Introduction

The Conference on Automated Deduction (CADE) has been for nearly twenty years a meeting where both theoreticians and system implementors present their work. Feeling perhaps that the conference was becoming dominated by the theoreticians, Ross Overbeek proposed at CADE-10 in 1990 a contest to stimulate work on the implementation and use of theorem-proving systems. The challenge was to prove a set of theorems, and do so with a uniform approach. That is, it was not allowed to set parameters in the system to specialize it for individual problems. There were actually two separate contests, one represented by a set of seven problems designed to test basic inference components, and the other represented by a set of ten problems designed to test equality-based systems.

This paper describes our experiences in preparing to enter the contest with Otter[5,6] and ROO[1,2], two systems developed at Argonne National Laboratory. ROO is a parallel version of Otter, but has such different behavior in some cases that we treat them a separate entries. We entered each of them in both contests.

Some of the problems are difficult ones, and although many of the problems had been done before with Otter, in each case we had set Otter's many input parameters in a way customized to the problem at hand, and chosen a set of support that appeared to us to be most natural. It was a challenge to come up with a uniform set of parameter settings and a uniform algorithm for picking the set of support that would allow Otter to prove each of the theorems.