Equational Prover

EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search. It seems to perform well on many problems about lattice-like structures.

EQP is not as stable and polished as our main production theorem prover Otter. But it has obtained several interesting results, and we have decided to make it available (including the source code) to everyone, with no restrictions (and of course no warranty). EQP's documentation is not good, but if you already know Otter, you might not have great difficulty in learning to use EQP.

Download

The whole package, including the source code, users' guide, and example input files:

eqp-09d (April 1998)
eqp-09e (May 2009)

For a quick preview, see the README file, the users' guide, and the ChangeLog file.

EQP's Solution of the Robbins Problem
EQP's results on some problems in quantum logic
33 Basic Test Problems: A Practical Evaluation of Some Paramodulation Strategies, a paper on experiments with EQP
Otter, a theorem prover for full first-order logic with equality
Mace2, a program that looks for models (e.g., counterexamples) of first-order statements

Equational Prover

Download

Related Pages