Abstract
Most automated reasoning systems rely on human knowledge or heuristics to guide the reasoning or search for proofs. We have evaluated the use of a powerful general search algorithm to search in the space of mathematical proofs. In our approach, automated reasoning is seen as an instance of automated programming where the proof is seen as a program (of functions corresponding to rules of inference) which transforms a statement into an axiom. We use genetic programming as the general technique for automated programming. We show that such a system can be used to evolve mathematical proofs in complex domains, i.e. arithmetics. We extend our previous research by the implementation of an efficient and stable C-language system in contrast to earlier work in Prolog.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Banzhaf, W., Nordin, P., Keller R.E., Francone, F.D. (1998) Genetic Programming-An Introduction. Morgan Kauffmann, San Fransisco, and d-punkt, Heidelberg, Germany.
Bledsoe W. W., (1977) Non-Resolution Theorem Proving, In Artificial Intelligence, Vol. 9, pp 2–3.
Boyer R.S., Moore J.S. (1979) Proving Teorems about LISP-Functions, In J.ACM, Vol. 22, pp 129–144.
Boyer R.S., Yu Y. (1992) Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor, In Automated Deduction-CADE-11 Kapur D. (Ed), pp. 416–430.
Bundy A., (1983) The Computer Modeling of Mathematical Reasoning, Academic Press, London, pp. 74–77.
James W. (1890) The principles of psychology Vol.1. Originally published: Henry Holt, New York 1890.
Koza, J. (1992) Genetic Programming, MIT Press, Cambridge, MA
Lowerre, B.T., Reddy, R.D. (1980) The Harpy Speech Understanding System. In Trends in Speech Recognition. Lea, W.A. (Ed.) Englewood Cliffs, Prentice-Hall, New York.
McCune W.W. (1994) Otter 3.0 Reference Manual and Guide. Argonne National Laboratory, Argonne, USA.
Newell, A., Shaw J.C., and Simon H. (1957) Empirical Explorations of the Logic Theorem Machine: A case study in Heuristic, in Proceedings of Western Joint Computer Conference Vol. 15.
Nordin J.P., Banzhaf W. (1995a) Complexity Compression and Evolution, in Proceedings of Sixth International Conference of Genetic Algorithms, Pittsburgh, 995, L. Eshelman (ed.), Morgan Kaufmann, San Mateo, CA
Nordin, J.P.,F. Francone, Banzhaf W. (1995b) Explicitly Defined Introns in Genetic Programming. In Advances in Genetic Programming II, (In press) Kim Kinnear, Peter Angeline (Eds.), MIT Press USA.
Nordin, J.P., Banzhaf W.(1995c) Controlling an Autonomous Robot with Genetic Programming. In proceedings of: 1996 AAAI fall symposium on Genetic Programming, Cambridge, USA.
Robinson J.A., (1965) A Machine Oriented Logic Based on the Resolution Principle, In J.ACM, Vol. 12, No. 1, pp. 23–41.
Rosenblom, P. (1987) Best First Search. In Encyclopedia of Artificial Intelligence, Shapiro, S. (Ed) Vol. 2, Wiley, New York.
Russel S., Norvig P. (1995) Artificial Intelligence: A modern approach. Prentice-Hall, Inc.
Winker S., Wos L., (1978) Automated Generation of Models and Counterexamples and its application to Open Questions in Ternary Boolean Algebra, In Proceedings of 8th international symposium Multiple-Valued Logic, Rosemont, Ill., IEEE and ACM, pp. 251–256, New York
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nordin, P., Eriksson, A., Nordahl, M. (1999). Genetic Reasoning: Evolutionary Induction of Mathematical Proofs. In: Poli, R., Nordin, P., Langdon, W.B., Fogarty, T.C. (eds) Genetic Programming. EuroGP 1999. Lecture Notes in Computer Science, vol 1598. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48885-5_19
Download citation
DOI: https://doi.org/10.1007/3-540-48885-5_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65899-3
Online ISBN: 978-3-540-48885-9
eBook Packages: Springer Book Archive