iProver-Eq

This is the iProver-Eq system developed in my PhD thesis. It is identical to the version that was most recently entered into CASC 24. Unfortunately, I currently don't have the time to add new features to the system, so nothing has happened since then.

Download iProver-Eq (8.0MB)

Send your questions and bug reports to christoph@sticksel.info

Installation and Usage

For compilation, OCaml in version 4.00 is required together with the and ocamlfind tools.

The SMT solver CVC4 in the directory cvc4-1.2 has the following additional requirements (from cvc4-1.2/README)

  • GNU C and C++ (gcc and g++), reasonably recent versions
  • GNU Make
  • GNU Bash
  • GMP v4.2 (GNU Multi-Precision arithmetic library)
  • The Boost C++ base libraries

No call to a configure script is necessary.

If you have some of the libraries in a non-standard location, run make with the environment variables CFLAGS and LDFLAGS set to the required paths.

The default installation location is /usr/local/bin, set the environment variable BINDIR to override this.

To compile and install iProver-Eq just call make, if you want or need to adjust the default paths, call make as

BINDIR=$HOME/bin CFLAGS=-I/opt/local/include LDFLAGS=-L/opt/local/lib make

Execute iProver-Eq by calling

iprover-cvc4-eq-nc --time_out_virtual %d %s

where %d is the CPU time limit and %s is the problem file name.

The distinguished strings are as recommended by the TPTP library

  • % SZS status Theorem\n
  • % SZS status Unsatisfiable\n
  • % SZS status CounterSatisfiable\n
  • % SZS status Satisfiable\n

No proofs or solutions are output.

To read TPTP files in FOF format, iProver-Eq needs an external clausifier. Vampire and E are supported. Install the respective executable in the same location as iProver-Eq and it will detect and use it to preprocess TPTP FOF problems.

System Description

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.

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. By default, 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 instances need to be generated and the calculus is run without the otherwise necessary bookkeeping.

Implementation

iProver-Eq is implemented in OCaml and uses the CVC4 SMT solver [BCDHJKRT11] 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 [HKV11,HKKV12] or the E prover is used for clausification and preprocessing of FOF problems.

References

BCDHJKRT11
Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C. (2011), CVC4, Gopalakrishnan, G., Shaz, Q., Proceedings of the 23rd International Conference on Computer Aided Verification (Snowbird, Utah), pp. 171-177 Lecture Notes in Computer Science 6806, 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.
HKKV12
Hoder K., Khasidashvili Z, Korovin K., Voronkov A. Preprocessing Techniques for First-Order Clausification in preparation.
HKV11
Hoder K., Kovács L., Voronkov A. (2011) Invariant Generation in Vampire Proceeding of Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2011), pp. 60-64, LNCS 6605, 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.

Picture of me

Dr. Christoph Sticksel

Sr. Software Engineer in
Formal Methods/Program Analysis at
MathWorks
Natick, MA

Christoph.Sticksel@mathworks.com