Interactive Proof: Proof Translation, Premise Selection, Rewriting

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 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 the major ones is HOLyHammer developed in collaboration between the University of Innsbruck and Radboud University Nijmegen. It is currently able to find 40% of the formal Flyspeck proofs completely automatically. 

The main goal of the project is to create and further develop techniques and tools for using automated approaches in interactive proof systems in order to allow the mechanical construction of proofs that can be computer-verified.
The tools and techniques that the project intends to develop include: 

  1. proof translation between various logic and external first and higher order ATPs (automated theorem provers);
  2. providing stronger machine learning-based premise selection;
  3. automatically deriving and simplifying terminating and confluent rewrite databases for the interactive proof systems. 

We anticipate that the 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. The project will increase the power of the HOLyHammer tool, linking proof assistants with automated tools developed in Innsbruck. Furthermore, we expect that the research will make proof assistants more user friendly and, in the long term, contribute to bringing formal proof development to mainstream mathematics and computer science.

Duration: February 1, 2014, extended until beginning of 2019


Project Members

  • Cezary Kaliszyk
  • Łukasz Czajka
  • Thibault Gauthier
  • Michael Färber
  • Julian Parsert
  • Sebastian Waldhart
FWF Standalone Project, project number




Nach oben scrollen