iProver-Eq

This is the version of the iProver-Eq system exactly as used for the evaluation of my PhD thesis.

A formal release of an improved and tuned system will follow right after CASC-23 in August 2011. The system to download here is licensed for use only to verify the contributions of my thesis, please do not distribute. Contact me if you want to use it for other purposes.

Download iProver-Eq (1.9MB)

top

Installation

For compilation, OCaml in version 3.12 is required together with the camlidl and ocamlfind tools. Perl, bison and flex are required for CVC3 that is used as the ground solver.

For clausification Vampire is used and a binary of the clausifier is shipped as vclausify_rel.

The executable should be able to be compiled with the Makefile, calling make in the directory. No call to a configure script is necessary.

Execute iProver-Eq by calling iprover-cvc-eq-nc --time_out_rel 60. problem.

To use a different clausifier or in a different location pass the appropriate values in the options --clausifier and --clausifier_option

Don't hesitate to contact me at csticksel@cs.man.ac.uk if I can be of any help. I know that gathering the correct libraries etc. can be a bit of a pain

top

System Description

Konstantin Korovin, Christoph Sticksel
The University of Manchester, United Kingdom

Architecture

iProver-Eq [KS10a] extends the iProver system [Kor08] with built-in equational reasoning, along the lines of [GK04]. As in the iProver system, first-order reasoning is combined with ground satisfiability checking where the latter is delegated to an off-the-shelf ground solver.

iProver-Eq consists of three core components: i) ground reasoning by an SMT solver, ii) first-order equational reasoning on literals in a candidate model by a labelled unit superposition calculus [KS10a,KS10b] and iii) instantiation of clauses with substitutions obtained by ii).

Given a set of first-order clauses, iProver-Eq first abstracts it to a set of ground clauses which are then passed to the ground solver. If the ground abstraction is unsatisfiable, then the set of first-order clauses is also unsatisfiable. Otherwise, literals are selected from the first-order clauses based on the model of the ground solver. The labelled unit superposition calculus checks whether selected literals are conflicting. If they are conflicting, then clauses are instantiated such that the ground solver has to refine its model in order to resolve the conflict. Otherwise, satisfiability of the initial first-order clause set is shown.

Clause selection and literal selection in the unit superposition calculus are implemented in separate given clause algorithms. Relevant substitutions are accumulated in labels during unit superposition inferences and then used to instantiate clauses. For redundancy elimination iProver-Eq uses demodulation, dismatching constraints and global subsumption. In order to efficiently propagate redundancy elimination from instantiation into unit superposition, we implemented different representations of labels based on sets, AND/OR-trees and OBDDs. Non-equational resolution and equational superposition inferences provide further simplifications.

For the LTB division, iProver-Eq-SInE runs iProver-Eq as the underlying inference engine of SInE [HV11], i.e., axiom selection is done by SInE, and proof attempts are done by iProver-Eq.

Strategies

Proof search options in iProver-Eq control clause and literal selection in the respective given clause algorithms. Equally important is the global distribution of time between the inference engines and the ground solver. At CASC, iProver-Eq will execute a fixed schedule of selected options.

If no equational literals occur in the input, iProver-Eq falls back to the inference rules of iProver, otherwise the latter are disabled and only unit superposition is used. If all clauses are unit equations, no instantiations need to be generated and the calculus is run without the otherwise necessary bookkeeping.

Implementation

iProver-Eq is implemented in OCaml and uses CVC3 [BT03] for the ground reasoning in the equational case and MiniSat [ES03] in the non-equational case. iProver-Eq accepts FOF and CNF formats, where Vampire [RV01] is used for clausification of FOF problems.

References

BT07
Barrett C., Tinelli C. (2007), CVC3, Damm W., Hermanns H., Proceedings of the 19th Conference on Computer Aided Verification (Bremen, Germany), pp. 298-302, Lecture Notes in Computer Science 4590, Springer.
ES03
Eén, N., Sörensson, N. (2003), An Extensible SAT-solver, Giunchiglia E., Tacchella A., Selected Revised Papers of the 6th International Conference Theory and Applications of Satisfiability Testing (SAT) (Santa Margherita Ligure, Italy) pp. 502-518, Lecture Notes in Computer Science 2919, Springer.
GK04
Ganzinger H., Korovin K. (2004), Integrating Equational Reasoning into Instantiation-Based Theorem Proving, Marcinkowski J., Tarlecki A., Proceedings of the 18th International Workshop on Computer Science Logic (CSL), 13th Annual Conference of the EACSL (Karpacz, Poland), pp.71-84, Lecture Notes in Computer Science 3210, Springer.
HV11
Hoder, K., Voronkov A. (2011), Sine Qua Non for Large Theory Reasoning, Proceedings of the 23rd Conference on Automated Deduction (CADE) (Wroclaw, Poland), Lecture Notes in Computer Science, Springer.
Kor08
Korovin K. (2008), iProver - An Instantiation-Based Theorem Prover for First-order Logic (System Description), Baumgartner P., Armando A., Gilles D., Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR) (Sydney, Australia), pp. 292-298, Lecture Notes in Artificial Intelligence, Springer.
KS10a
Korovin K., Sticksel C. (2010), iProver-Eq - An Instantiation-Based Theorem with Equality, Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR) (Edinburgh, United Kingdom), pp. 196-202, Lecture Notes in Computer Science 6173, Springer.
KS10b
Korovin K., Sticksel C. (2010), Labelled Unit Superposition Calculi for Instantiation-based Reasoning, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) (Yogyakarta, Indonesia), pp. 459-473, Lecture Notes in Computer Science 6397, Springer.
RV01
Riazanov A, Voronkov, A. (2001), Vampire 1.1 (System Description), Leitsch A., Nipkow T., Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR) (Siena, Italy), pp. 376-380, Lecture Notes in Computer Science 2083, Springer.