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

Download the current version from: iProver at Google Code.
New version iProver v0.8.1 (Post CASC-J5, 2010) is released!!!
Easy to install: We assume OCaml v3.10 >= is installed.
1) ./configure
2) make will produce executable: iproveropt
Alternatively you can download an executable compiled for Linux.
Easy to use: iproveropt problem.p
where problem.p is a cnf problem in the TPTP format. You can have more fun with more than 50 options available.
iProver won the EPR division at recent CASC-J5 (2010), CASC-22 (2009) and CASC-J4 (2008) competitions.
Performance: iProver performs well over whole TPTP library, see recent CASC results.
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.

iProver is currently distributed under GNU GPL and under GNU Lesser General Public License (LGPL), if you require a different license please contact: korovincs.man.ac.uk

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