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.
Send your questions and bug reports to christoph@sticksel.info
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)
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
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.
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.
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.
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.
Dr. Christoph Sticksel
Senior Team Leader and Principal Software Engineer in
Formal Methods/Program Analysis at
MathWorks
Natick, MA