Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.


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.

share|improve this question
add comment

1 Answer

up vote 2 down vote accepted

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)

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.