iProver --- a theorem prover for first-order logic with support for arithmetic reasoning.
iProver supports all combinations of quantifiers, uninterpreted functions, data types, linear and non-linear arithmetic.
iPorver is implemented in OCaml.
iProver v3.5 (SMT-COMP-2021/CASC-28)
For quantified reasoning iProver interleaves instantiation calculus Inst-Gen with ordered resolution and superposition calculi.
iProver integrates Z3 and MiniSAT for ground reasoning during the reasoning phase and uses Vampire for clausification and axiomatisations of theories which is done as the initial problem transformation.
The reasoning method behind iProver is refutationally complete for pure first-order logic with equality. iProver supports arbitrary precision arithmetic.
A very brief overview of iProver: iprover-smt-comp-2021.pdf.
Features and supported input formats:
- SMT2: combinations of quantifiers, uninterpreted functions, data types, linear and non-linear arithmetic.
- TPTP CNF/TF0/TCF/FOF (TFF/FOF with external clausifiers)
- Finite model finding: TPTP
- QBF/DQBF: QDIMACS
- Hardware verification: AIGER
- First-order verification:
an extension of TPTP for specifying first-order transition systems and verification conditions
- Planning: PDDL (in progress )
Major contributors:
Project leader: Konstantin Korovin (konstantin.korovin[@]manchester.ac.uk), The University of Manchester, UK
- Konstantin Korovin: core, instantiation, resolution, finite model finding, preprocessing, indexing, QBF
- Andre Duarte: superposition, AC reasoning, simplifications, SMT/Z3:
- Edvard K. Holden: HOS-ML, parameter tuning, machine learning
- Julio Cesar Lopez Hernandez: abstraction refinement
- Dmitry Tsarkov: bounded model checking, k-induction, AIG
- Christoph Sticksel: proofs/unsat cores, bounded model checking
- Martin Suda: planning
Please email (konstantin.korovin[@]manchester.ac.uk) for comments, 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
CASC competitions.
|
|
References:
- Implementing Superposition in iProver (System Description)
[pdf, bib]
- Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning
[pdf, bib]
- iProver - An Instantiation-Based Theorem Prover for First-Order Logic
[pdf,
bib]
- for specific features please refer to corresponding papers
Mac version
External libraries:
- Vampire used for clausification and theory axioms:
Andrei Voronkov, Giles Reger, Laura Kovac, Ahmed Bhayat, Martin Suda, Krystof Hoder, Alexander Riazanov ...
- MiniSat (ground reasoning) Niklas Een and Niklas Sorensson
- Z3 (ground reasoning) Nikolaj Bjorner, Leonardo de Moura, ..
- AIG parser: Armin Biere
- OCamlgraph: Sylvain Conchon, Jean-Christophe Filliātre, Julien Signoles
- Zarith: Antoine Miné, Xavier Leroy, Pascal Cuoq, Christophe Troestler
iProver is currently distributed under GNU GPL if you require a different license please contact:
konstantin.korovin
manchester.ac.uk
maintained by Konstantin Korovin, this research is supported by The Royal Society and the University of Manchester