Genetic Reasoning: Evolutionary Induction of Mathematical Proofs

Abstract. Most automated reasoning systems rely on human knowl-edge 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 ecient and stable C-language system in contrast to earlier work in Prolog.