An entry in the 1992 Overbeek theorem-proving contest [electronic resource].
- Washington, D.C. : United States. Dept. of Energy, 1992. and Oak Ridge, Tenn. : Distributed by the Office of Scientific and Technical Information, U.S. Dept. of Energy.
- Physical Description:
- 42 pages : digital, PDF file
- Additional Creators:
- Argonne National Laboratory, United States. Department of Energy, and United States. Department of Energy. Office of Scientific and Technical Information
- Restrictions on Access:
- Free-to-read Unrestricted online access
- 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 and Roo, 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 as 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 information algorithm for picking the set of support that would allow OTTER to prove each of the theorems.
- Published through SciTech Connect., 11/01/1992., "anl/mcs-tm--172", "DE93004735", and McCune, W.W.; Lusk, E.L.
- Type of Report and Period Covered Note:
- Topical; 11/01/1992 - 11/01/1992
- Funding Information:
View MARC record | catkey: 14355309