What does Equational Theorem Prover do?

Question

http://www.cs.unm.edu/~mccune/eqp/

What does EQP do? Is there any paper that explains what it does?

README and other read files do not provide such information - it only talks of how to use it and not what theoretical background of it is.

Answer 1

It seems to do exactly what it says on the tin, that is, automatically prove theorems in equational logic. Judging from it's age, it's more-or-less obsolete. It is a precursor to Otter, which is the precursor to Prover9 (both by William McCune); you will find documentation at the linked site. Prover9 has a counterpart, Mace4, which can find counterexamples to "conjectures".

The general idea with automated theorem provers is starting off with a list of axioms, then "combine" them in all possible ways to obtain a list of results that follow from those axioms. We then take those results, and combine them together, to get new results, and so on recursively, until we (hopefully) prove our goal.

Two methods are particularly helpful in reducing the search space and run time:

• Pruning duplicate (or trivial) intermediate results.
• Working backwards from the specified goal.

Unfortunately, automated theorem provers are largely limited to first order logic (for the time being).

For further reading, see e.g.

R Nieuwenhuis, A. Rubio, Paramodulation-based theorem proving, in Handbook of Automated Reasoning, 2001. (pdf)