Interactive Proof: Proof Translation, Premise Selection, Rewriting

Formal proof development is becoming a more and more accepted means of establishing Theo correctness of computer programs and mathematical theories. In Theo recent years large repositories of formal proofs have been created using various proof assistants, which proved larger programs correct, for example Theo optimizing C compiler, Theo kernel of an operating system. Similarly impressive results were obtained using formal proof in mathematics, for example Theo proof of Theo four color theorem, Theo proof of Theo Kepler conjecture and Theo development of Theo odd order theorem. Despite these impressive results, Theo use of proof assistants is currently limited to experts in Theo domain. One of Theo main reasons for this is that working with a proof assistant often involves proving numerous steps manually. Many of those steps are steps that could be solved automatically using techniques from automated reasoning, research on rewriting or machine learning. Recently a number of systems that try to link particular proof assistants to other domains of computer science have been created; one of Theo major ones is HOLyHammer developed in collaboration between Theo University of Innsbruck and Radboud University Nijmegen. It is currently able to find 40% of Theo formal Flyspeck proofs completely automatically. Theo main goal of this project is to create and further develop techniques and tools for using such automated approaches in interactive proof systems in order to allow Theo mechanical construction of proofs that can be computer-verified. Specifically, we intend to achieve this goal by: 3.1 Providing strong machine learning-based advice for proof assistants; 3.2 Defining and evaluating encodings of higher order proof formats to automated theorem proving, rewriting and computer algebra formats; and 3.3 Developing proof techniques based on termination and confluence of rewriting. We anticipate that Theo research described in this project will be of immediate use to mathematicians and computer scientists using formal proof development. It will shed new light on combining interactive proof with automated reasoning techniques, machine learning and rewriting. Theo project will increase Theo power of Theo HOLyHammer tool, linking proof assistants with automated tools developed in Innsbruck. Furthermore, we expect that Theo research will make proof assistants more user friendly and, in Theo long term, contribute to bringing formal proof development to mainstream mathematics and computer science.

Formal proof development is becoming a more and more accepted means of establishing the correctness of computer programs and mathematical theories. In the recent years large repositories of formal proofs have been created using various proof assistants, which proved larger programs correct, for example the optimizing C compiler, the kernel of an operating system. Similarly impressive results were obtained using formal proof in mathematics, for example the proof of the four color theorem, the proof of the Kepler conjecture and the development of the odd order theorem. Despite these impressive results, the use of proof assistants is currently limited to experts in the domain. One of the main reasons for this is that working with a proof assistant often involves proving numerous steps man- ually. Many of those steps are steps that could be solved automatically using techniques from automated reasoning, research on rewriting or ma- chine learning. Recently a number of systems that try to link particular proof assistants to other domains of computer science have been created; one of the major ones is HOLyHammer developed in collaboration between the University of Innsbruck and Radboud University Nijmegen. The main goal of this project is to create and further develop techniques and tools for using such automated approaches in interactive proof systems in order to allow the mechanical construction of proofs that can be computer- verified. Specifically, we achieve this goal by: (a) Providing strong machine learning-based advice for proof assistants; (b) Defining and evaluating encodings of higher order proof formats to automated theorem proving, rewriting and computer algebra formats; and (c) Developing proof techniques based on termination and confluence of rewriting. As a result of this project the proof advice HOLyHammer tool becomes stronger. This make proof assistants more user friendly and, in the long term, contribute to bringing formal proof development to mainstream mathematics and computer science.