Representing heuristic-relevant information for an automated theorem prover

  • Christian B. Suttner
Part III Communications
Part of the Lecture Notes in Computer Science book series (LNCS, volume 464)


A promising approach to attack the problem of combinatorial explosion faced in automated theorem proving is to employ search guiding heuristics. Our system, which is able to learn such heuristics automatically, uses evaluation functions to rate different choices for continuation during a proof. In this paper, we will focus on the content and representation of the input to these evaluation functions.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BES+81]
    [BES+81] K. Bläsius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, and C. Walther. The Markgraf Karl Refutation Proof Procedure. In Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, 1981.Google Scholar
  2. [CL73]
    C.-L. Chang and R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
  3. [ESS89]
    W. Ertel, J. Schumann, and C.B. Suttner. Learning Heuristics for a Theorem Prover using Back Propagation. In Proceedings of the 5. ÖGAI-Conference, Igls, Austria, 1989. Springer.Google Scholar
  4. [LBSB]
    R. Letz, S. Bayerl, J. Schumann, and W. Bibel. SETHEO: A High-Performance Theorem Prover. to appear in: Journal of Automated Reasoning.Google Scholar
  5. [Lov68]
    D.W. Loveland. Mechanical Theorem-Proving by Model Elimination. Journal of the ACM, 15(2), 1968.Google Scholar
  6. [OMW76]
    R. Overbeek, J. McCharen, and L. Wos. Complexity and Related Enhancements for Automated Theorem-Proving Programs. Comp. & Maths. with Appls., 2(1-A), 1976.Google Scholar
  7. [RHW86]
    D.E. Rumelhart, G.E. Hinton, and R.J. Williams. Learning Internal Representations by Error Propagation. In Parallel Distributed Processing, 1986.Google Scholar
  8. [Sam59]
    A.L. Samuel. Some Studies in Machine Learning Using the Game of Checkers. IBM Journal, 1(3), 1959.Google Scholar
  9. [Sam67]
    A.L. Samuel. Some Studies in Machine Learning Using the Game of Checkers, II. IBM Journal, 11(6), 1967.Google Scholar
  10. [SE90]
    C.B. Suttner and W. Ertel. Automatic Acquisition of Search Guiding Heuristics. In Proceedings of the 10. International Conference on Automated Deduction (CADE). Springer, 1990.Google Scholar
  11. [SF71]
    J.R. Slagle and C.D. Farrell. Experiments in Automatic Learning for a Multipurpose Heuristic Program. Comm. of the ACM, 14(2), 1971.Google Scholar
  12. [Sti86]
    M.E. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89–101, 1986.Google Scholar
  13. [Sut89]
    C.B. Suttner. Learning Heuristics for Automated Theorem Proving. Diploma Thesis, Technical University Munich, May 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Christian B. Suttner
    • 1
  1. 1.Forschungsgruppe Künstliche IntelligenzTechnische Universität MünchenMünchen 2

Personalised recommendations