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
(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 folCall 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