Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Uniform strategies: The CADE-11 theorem proving contest

  • 25 Accesses

  • 2 Citations

Abstract

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.

References

  1. 1.

    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).

  2. 2.

    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).

  3. 3.

    Lusk, E. and Overbeek, R., ‘The automated reasoning system ITP’,Tech. Report ANL-84/27, Argonne National Laboratory, Argonne, Ill. (April 1984).

  4. 4.

    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).

  5. 5.

    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).

  6. 6.

    McCune, W.,Otter 2.0 Users' Guide. Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, Ill. (March 1990).

  7. 7.

    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).

  8. 8.

    McCune, W. and Wos, L., ‘The absence and the presence of fixed point combinators’,Theoretical Computer Science,87 221–228 (1991).

  9. 9.

    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).

  10. 10.

    Smith, B., ‘Reference manual for the environmental theorem prover: An incarnation ofAura’,Tech. Report ANL-88-2, Argonne National Laboratory, Argonne, Ill. (March 1988).

  11. 11.

    Hantao Zhang, ‘Automatic proofs of equality problems in Overbeek's competition’,Journal of Automated Reasoning,11 333–351 (1993).

Download references

Author information

Rights and permissions

Reprints and Permissions

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

Download citation

Key words

  • Automated theorem proving
  • resolution
  • paramodulation
  • Knuth-Bendix completion
  • strategy