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:
Major contributors:

Project leader: Konstantin Korovin (konstantin.korovin[@]manchester.ac.uk), The University of Manchester, UK
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.

Mac version
External libraries:
iProver is currently distributed under GNU GPL if you require a different license please contact: konstantin.korovinmanchester.ac.uk
maintained by Konstantin Korovin, this research is supported by The Royal Society and the University of Manchester