These web pages are a supplement to the following paper.
33 Basic Test Problems:
A Practical Evaluation of Some Paramodulation Strategies
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.
Abstract
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.