At CADE-10 Ross Overbeek proposed a two-part contest to stimulate and reward work in automated theorem proving. The first part consists of seven theorems to be proved with resolution, and the second part of equational theorems. Our theorem proversOtter and its parallel childRoo proved all of the resolution theorems and half of the equational theorems. This paper represents a family of entries in the contest.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Lusk, E., and McCune, W., ‘Experiments withRoo, a parallel automated deduction system’, in B. Fronhöfer and G. Wrightson (Eds.),Parallelization in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590, pp. 139–162, New York, Springer-Verlag (1992).
Lusk, E., McCune, W. and Slaney, J., ‘Roo — a parallel theorem prover’,Tech. Memo ANL/MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill. (1991).
Lusk, E. and Overbeek, R., ‘The automated reasoning system ITP’,Tech. Report ANL-84/27, Argonne National Laboratory, Argonne, Ill. (April 1984).
McCharen, J., Overbeek, R. and Wos, L., ‘Complexity and related enhancements for automated theorem-proving programs’,Computers and Mathematics with Applications,2 1–16 (1976).
McCharen, J., Overbeek, R. and Wos, L., ‘Problems and experiments for and with automated theorem-proving programs’,IEEE Transactions on Computers,C-25(8), 773–782 (August 1976).
McCune, W.,Otter 2.0 Users' Guide. Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, Ill. (March 1990).
McCune, W., ‘What's New inOtter 2.2’,Tech. Memo ANL/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill. (July 1991).
McCune, W. and Wos, L., ‘The absence and the presence of fixed point combinators’,Theoretical Computer Science,87 221–228 (1991).
McCune, W. and Wos, L., ‘Experiments in automated deduction with condensed detachment’, D. Kapur (Ed.),Proceedings 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 607, pp. 209–223. New York, Springer Verlag (June 1992).
Smith, B., ‘Reference manual for the environmental theorem prover: An incarnation ofAura’,Tech. Report ANL-88-2, Argonne National Laboratory, Argonne, Ill. (March 1988).
Hantao Zhang, ‘Automatic proofs of equality problems in Overbeek's competition’,Journal of Automated Reasoning,11 333–351 (1993).
About this article
Cite this article
Lusk, E.L., McCune, W.W. Uniform strategies: The CADE-11 theorem proving contest. J Autom Reasoning 11, 317–331 (1993). https://doi.org/10.1007/BF00881871
- Automated theorem proving
- Knuth-Bendix completion