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))

See Full syntax of formulas.

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=<prover>  use the specified prover
            for choices of <prover>, 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=<enc>  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
   First-order resolution prover with set of support and clausal indexing
-inference=RESOLUTION_HEURISTIC_INFERENCE
   First-order resolution prover based on heuristic search
   with set of support and clausal indexing
-inference=RESOLUTION_SATURATION_INFERENCE
   Naive first-order resolution prover based on saturation
-inference=PROPOSITIONAL_INFERENCE
   Propositional DPLL procedure
-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