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.

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.

share|improve this question

1 Answer 1

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
    
This answer has some good links, but it does contain some errors. The idea of automated theorem proving lies in starting off with some assumptions (the assumptions might have variables in which case they could be axioms, they might also only have constants in which case they might not be axioms) and then getting the program to derive the goal. Combining all of the assumptions in all possible ways only describes a level saturation or breadth-first search strategy. Automated theorem provers often use different strategies, or use a level saturation approach in concert with something else. –  Doug Spoonwood Jul 2 at 3:12
    
Also, from what I can tell OTTER first got developed in 1988. McCune's/EQP's result about Robbins' algebras appeared in 1996. From what I can tell, EQP has more specially strategies available than OTTER, it didn't make OTTER obsolete. I can say with more certainty that Prover9, so far as I can tell, didn't make OTTER obsolete since OTTER has a passive list option, a hot list option, and there exists a way to weight the head and tail of a function in OTTER which I don't believe you can do in Prover9. Also, Larry Wos, McCune's longtime colleague at Argonne still uses OTTER. –  Doug Spoonwood Jul 2 at 3:17

Your Answer

 
discard

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.