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


Download the current version from: iProver at Google Code.
New version: iProver v0.99 (CASC-J6, 2012) to be released in a few days!!!
Easy to install: We assume OCaml v3.12 >= 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 (effectively propositional) EPR division at recent: CASC-J6 @ IJCAR (2012), CASC-23 (2011), CASC-J5 (2010), CASC-22 (2009) and CASC-J4 (2008) competitions. EPR fragment can be used to encode a wide range of problems; in particular we are collaborating with Intel on hardware verification using EPR methods (see references in our recent publications).
iProver won the first-order satisfiability (non-theorems) division (FNT) at CASC@Turing (2012) part of the Turing Centenary Conference.
Performance: iProver performs well over the 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