iProver --- an instantiation-based theorem prover for first-order logic


iProver is currently distributed under GNU GPL and under GNU Lesser General Public License (LGPL).

iProver is easy to use, just run "iproveropt problem.p" where problem.p is a cnf problem in the TPTP format. You can have more fun with around 40 options available. You can download the sources and build iProver by simply running "./configure" and then "./make". Alternatively you can download an executable compiled for Linux.

The current version of iProver is available to download: iProver at Google Code. New version iProver v0.7 is released!!!

For a general architecture of iProver please see the system description and for more details: An Invitation to Instantiation-Based Reasoning: From Theory to Practice. Let us only mention here that one of the distinctive features of iProver is a modular combination of first-order reasoning with ground reasoning. In particular, iProver currently integrates MiniSat for reasoning with ground abstractions of first-order clauses.

Performance: iProver performs well over all TPTP library and especially strong on the EPR (function-free/effectively propositional/Bernays-Schönfinkel) class.

iProver won the EPR division at recent CASC-J4 (2008) and CASC-22 (2009) competitions.

Please, send your comments, suggestions and bug reports to korovincs.man.ac.uk

A highly experimental version of iProver-Eq where equational reasoning is built-in via a superposition calculus and the ground reasoning uses CVC3 is available here: iprover-eq.tar.gz (developed together with Christoph Sticksel)
Konstantin Korovin, this research is supported by The Royal Society and The University of Manchester