These web pages are a supplement to the following paper.

33 Basic Test Problems:
A Practical Evaluation of Some Paramodulation Strategies

W. McCune

The paper appears as Chapter 5 (pp. 71-114) in Automated Reasoning and its Applications: Essays in Honor of Larry Wos, edited by Robert Veroff, MIT Press, 1997. Here is a preprint.
NOTE: The paper states that the Robbins problem is still open, but the problem has now been solved. Look here for details.


We present a new theorem prover for equational logic, a set of 33 equational theorems for evaluating paramodulation strategies, a large set of experiments with several paramodulation strategies, and two equational proofs in Robbins algebra. The new theorem prover, EQP, includes associative-commutative unification, but in many other ways it is similar to our production theorem prover Otter. The 33 equational theorems are taken from a recent collaboration between the author and R. Padmanabhan and are mostly about lattice-like and group-like structures. The experiments are with basic paramodulation, blocked paramodulation, ordered paramodulation, functional subsumption, a heuristic for eliminating associative-commutative unifiers, and methods for directing the search. The two Robbins algebra lemmas were previously known, but we believe our proofs are the first equational proofs and the first ones found by computer.

Available by FTP:

Make sure to vist the EQP home page.