j'Imp Theorem Prover

>> >>

Overview

j'Imp (alias jImp) is an automatic theorem prover based on set of support and ordered resolution for first-order logic. It supports clause indexing techniques, subsumption, and tautology elimination. For propositional inference, j'Imp provides the special Davis-Putnam-Loveland-Logemann (DPLL) inference procedure, which is very similar to tableaux proving. j'Imp has been implemented in Java and is available along with its reusable components as a part of the Orbital library.

Usage

The easiest way to use the j'Imp theorem prover is to download the Orbital library and start one of the following scripts

bin/jimp on linux/windows/mac

Then type the following first-order formula as an input to show that all transitive irreflexive relations are asymmetric:

  (all a all b all c (r(a,b)&r(b,c)=>r(a,c))) && (all a ~r(a,a)) |= all a all b (r(a,b)=>~r(b,a))

You can also just tell j'Imp to prove or disprove a couple of test cases by calling

bin/jimp all none properties fol

Call bin/jimp --help to see further options and to get more information on the available configuration options and prover profiles of j'Imp.

usage: [options] [all|none|properties|fol|<filename>|table]
      all             prove important semantic-equivalence expressions
      none            try to prove some semantic-garbage expressions
      properties      prove some properties of classical logic inference relation
      fol             prove important equivalences of first-order logic

      <filename>      try to prove all expressions in the given file
      table           print a function table of the expression instead
      -               Use no arguments at all to be asked for expressions to prove.
options:
      -inference=<inference_mechanism>  use the specified prover
                      for choices of <inference_mechanism>, see list below
      -normalForm     check conjunctive and disjunctive forms of formulas
      -closure        print universal/existential closures of formulas
      -verbose        be more verbose (f.ex. print normal forms if -normalForm)
      -charset=<encoding>     the character set or encoding to use for reading files
      -problem        parse a problem file, i.e. combine all lines into a single problem,
                      instead of assuming single-line conjectures.

To check whether A and B are equivalent, enter '|= A<->B' or 'A == B'.
Use -verbose --help to get more help.
Available theorem provers:
  -inference=RESOLUTION_INFERENCE
      RESOLUTION: First-order resolution prover with set of support and clausal indexing
  -inference=RESOLUTION_HEURISTIC_INFERENCE
      RESOLUTION_HEURISTIC: First-order resolution prover based on heuristic search
      with set of support and clausal indexing
  -inference=RESOLUTION_SATURATION_INFERENCE
      RESOLUTION_SATURATION: Naive first-order resolution prover based on saturation
  -inference=PROPOSITIONAL_INFERENCE
      PROPOSITIONAL: Propositional DPLL procedure
  -inference=SEMANTIC_INFERENCE
      SEMANTIC_INFERENCE: Propositional inference using simple semantic truth-tables

Components

In addition to the standalone theorem prover application, j'Imp provides components reusable in more general settings. j'Imp include facilities for unified formula representation, flexible type-systems, formal language definition, logical inference systems, term rewrite systems, unification, term and formula parsing, formula evaluation, clause representation, classical logic, modal logic, fuzzy logic, and utilities for formula manipulation like conjunctive normal form or formatting.

Download

The theorem prover j'Imp and its reusable components are written in Java and part of the

Orbital library
See program bin/jimp
See packages orbital.logic.sign, orbital.logic.imp, orbital.moon.logic, orbital.logic.trs