iProver --- an instantiation-based theorem prover for first-order logic
iProver v2.5 (CASC-J8, 2016)
iProver is implemented in OCaml.
Features and supported input formats:
- First-order theorem proving: TPTP CNF/TCF (sorted first-order CNF)/FOF (with external clausifiers)
- Finite model finding: TPTP
- QBF: QDIMACS
- Hardware verification: AIGER
- First-order verification:
an extension of TPTP for specifying first-order transition systems and verification conditions
- Planning: PDDL (in progress )
Easy to install and use:
- install OCaml v4.02 or later
- iproveropt problem.p
Project manager: Konstantin Korovin (korovin[@]cs.man.ac.uk), the University of Manchester, UK.
- core, instantiaiton, resolution, finite model finding, preprocessing: Konstantin Korovin
- proofs/unsat cores: Christoph Sticksel
- bounded model checking, k-induction, AIG: Dmitry Tsarkov, Christoph Sticksel
- planning: Martin Suda
Please email us for comments, questions, suggestions, bug reports, or if you would like to join the project.
We are keen to hear about your experience with iProver, so please drop us a line.
iProver won the EPR and first-order satisfiability (FNT) divisions at several recent
- Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning
- iProver - An Instantiation-Based Theorem Prover for First-Order Logic
- for specific features please refer to corresponding papers
- MiniSAT: Niklas Een and Niklas Sorensson; (default)
- PicoSAT: Armin Biere (make PicoSAT=true)
- AIG parser: Armin Biere
- OCamlgraph: Sylvain Conchon, Jean-Christophe Filliātre, Julien Signoles
- For first-order clausifiaction iProver can be bundled with:
- Vampire - Andrei Voronkov, Giles Reger, Martin Suda, Krystof Hoder, Laura Kovacs...
- E prover - Stephan Schulz
iProver is currently distributed under GNU GPL if you require a different license please contact:
maintained by Konstantin Korovin, this research is supported by the Royal Society and the University of Manchester