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.
will produce executable: iproveropt
Alternatively you can download an executable compiled for Linux.
Easy to use:
where problem.p is a cnf problem in the TPTP format.
You can have more fun with more than 50 options available.
For a general architecture of iProver please see the
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:
Please, send your comments, suggestions and bug reports to
A highly experimental version of iProver-Eq
where equational reasoning is built-in via
a superposition calculus and the ground reasoning uses
is available here:
(developed together with Christoph Sticksel)
Konstantin Korovin, this research is supported by the Royal Society and the University of Manchester