Abstract
An essential heuristic in the SHUNYATA program is the composition heuristic which produces predicates and formulas forming the central “ideas” of proofs. In the proof of a rather simple theorem in mathematical logic, it generates a predicate. In the proof of Gödel's incompleteness theorem, it generates an undecidable formula. The construction of the above predicate and the undecidable formula ordinarily requires the application of Cantor's famous diagonal method. The composition heuristic was originally developed as a learning procedure which generates theorem provers automatically.
This work, in whole or in part, describes components of machines, processes, and programs protected by patents, patent applications, and copyright laws. Further information is available from the author. Copyright © 1997 by Kurt Ammon. All rights reserved.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ammon, K., The Automatic Development of Concepts and Methods. Doctoral dissertation, Department of Computer Science, University of Hamburg, 1988.
Ammon, K., The automatic acquisition of proof methods, Seventh National Conference on Artificial Intelligence, Saint Paul, Minnesota, 1988.
Ammon, K., Automatic proofs in mathematical logic and analysis. 11th International Conference on Automated Deduction, Saratoga Springs, NY, 1992.
Ammon, K., The SHUNYATA system. 11th International Conference on Automated Deduction, Saratoga Springs, NY, 1992.
Ammon, K., An automatic proof of Gödel's incompleteness theorem. Artificial Intelligence 61, 1993, pp. 291–306.
Bibel, W., Automated Theorem Proving. Vieweg, Braunschweig, 1982.
Brüning, S., Thielscher, M., and Bibel, W., Letter to the Editor, Artificial Intelligence 64, 1993, pp. 353–354.
Gödel, K., über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, Vol. 38, pp. 173–198.
Kleene, S. C., Introduction to Metamathematics. North-Holland, Amsterdam, 1952.
Letz, R., Schuhmann, J., Bayerl, S., and Bibel, W., SETHEO: A high-performance prover. Journal of Automated Reasoning 8, 1992, pp. 182–212.
Loveland, D. W., Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978.
Mendelson, E., Introduction to Mathematical Logic. Van Nostrand Reinhold, New York, 1964.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ammon, K. (1997). The composition heuristic. In: Freksa, C., Jantzen, M., Valk, R. (eds) Foundations of Computer Science. Lecture Notes in Computer Science, vol 1337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052112
Download citation
DOI: https://doi.org/10.1007/BFb0052112
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63746-2
Online ISBN: 978-3-540-69640-7
eBook Packages: Springer Book Archive