Genetic Reasoning Evolving Proofs with Genetic Search

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. The proof is a program executing functions that correspond to rules of inference. It transforms a statement into an axiom. Genetic programming is the technique we use for automated programming. We show how such a system can be used to evolve mathematical proofs. The domain of application is arithmetics and register machine program verification. Keywords: Genetic Programming, Automated Reasoning, Theorem Proving 1 Introduction We present an approach to reasoning that uses a genetic search heuristics to navigate and search in the space of true statements. An algorithm inspired by natural selection is used to search for proofs. To use a genetic process as the architecture for m..