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

Members

Project Members

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

P26201

  Contact

cezary.kaliszyk@uibk.ac.at

Publications
  • Learning Proof Search in Proof Assistants
    Michael Färber
    PhD thesis, University of Innsbruck, 2018.
  • IMP with Exceptions over Decorated Logic
    Burak Ekici
    Discrete Mathematics and Theoretical Computer Science 20(2), pp. 1 – 43, 2018.
  • Concrete Semantics with Coq and CoqHammer
    Łukasz Czajka, Burak Ekici and Cezary Kaliszyk
    11th Conference on Intelligent Computer Mathematics (CICM 2018), Springer LNAI 11006, pp. 53 – 59, 2018.
  • Towards Mac Lane’s Comparison Theorem for the (co)Kleisli Construction in Coq
    Burak Ekici
    4th Workshop on Formal Mathematics for Mathematicians, CEUR Workshop Proceedings,  pp. 1 – 5, 2018.
  • Towards a Unified Ordering for Superposition-Based Automated Reasoning
    Jan Jakubuv, Cezary Kaliszyk
    6th International Conference on Mathematical Software, Lecture Notes in Computer Science 10931, pp. 245 – 254, 2018.
  • Towards Formal Foundations for Game Theory
    Julian Parsert, Cezary Kaliszyk
    Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 495 – 503, 2018.5.
  • Aligning Concepts across Proof Assistant Libraries
    Thibault Gauthier, Cezary Kaliszyk
    J. Symbolic Computation 90, pp. 89 – 123, 2018.
  • Learning-Assisted Reasoning within Proof Assistants
    Thibault Gauthier
    PhD thesis, University of Innsbruck,  2018.
  • Hammer for Coq: Automation for Dependent Type Theory
    Łukasz Czajka, Cezary Kaliszyk
    J. Autom. Reasoning 61, pp. 423 – 453, 2018.
  • Monte Carlo Tableau Proof Search
    Michael Färber, Cezary Kaliszyk, Josef Urban
    26th International Conference on Automated Deduction, LNCS 10395, pp. 563-579, 2017.
  • Classification of Alignments Between Concepts of Formal Mathematical Systems
    Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
    10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 83-98, 2017.
  • Wikis and Collaborative Systems for Large Formal Mathematics
    Cezary Kaliszy, Josef Urban
    Post proceedings of Semantic Web Collaborative Spaces, LNCS  pp. 35-52, 2016.
  • Towards Formal Proof Metrics
    David Aspinall, Cezary Kaliszyk
    19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.
  • Improving Statistical Linguistic Algorithms for Parsing Mathematics
    Cezary Kaliszyk, Josef Urban, Jiri Vyskočil
    11th International Workshop on the Implementation of Logics, EPiC 40, pp. 27-36, 2016.
  • What’s in a Theorem Name?
    David Aspinall and Cezary Kaliszyk
    Proceedings of the 7th Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 459 – 465, 2016.
  • No Choice: Reconstruction of First-order ATP Proofs without Skolem Function
    Michael Färber, Cezary Kaliszyk
    5th Workshop on Practical Aspects of Automated Reasoning, CEUR-WS 1635, pp. 24-31, 2016.
  • TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism
    Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
    5th Workshop on Practical Aspects of Automated Reasoning, CEUR-WS 1635, pp. 41-55, 2016.
  • Goal Translation for a Hammer for Coq
    Łukasz Czajka and Cezary Kaliszyk
    1st International Workshop on Hammers for Type Theories, EPTCS 210, pp. 13-20, 2016.
  • A Learning-Based Fact Selector for Isabelle/HOL
    Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
    Journal of Automated Reasoning Volume 53, Number 3, pp. 219 – 244, 2016.
  • Hammering towards QED
    Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
    Journal of Formalized Reasoning 9(1), pp. 101 – 148, 2016.
  • Towards a Mizar Environment for Isabelle: Foundations and Language
    Cezary Kaliszyk, Karol Pąk, and Josef Urban
    Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),   pp. 58 – 65, 2016.
  • Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions
    Łukasz Czajka
    Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016),   pp. 49 – 57, 2016.
  • Sharing HOL4 and HOL Light Proof Knowledge
    Thibault Gauthier and Cezary Kaliszyk
    Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 372 – 386, 2015.
  • FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
    Cezary Kaliszyk and Josef Urban
    Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 88 – 96, 2015.
  • Metis-based Paramodulation Tactic for HOL Light
    Michael Färber, Cezary Kaliszyk
    Proceedings of the 1st Global Conference on Artificial Intelligence (GCAI 2015), EPiC Series in Computing 36, pp. 127-136, 2015.
  • MizAR 40 for Mizar 40
    Cezary Kaliszyk and Josef Urbanth
    Journal of Automated Reasoning 55(3), pp. 245 – 256, 2015.
  • Lemmatization for Stronger Reasoning in Large Theories
    Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
    Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 341 – 356, 2015.
  • Random Forests for Premise Selection
    Michael Färber and Cezary Kaliszyk
    Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 325 – 340, 2015.
  • Efficient Low-Level Connection Tableaux
    Cezary Kaliszyk
    Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015), Lecture Notes in Artificial Intelligence 9323, pp. 102 – 111, 2015.
  • Learning to Parse on Aligned Corpora (Rough Diamond)
    Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
    Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science 9236, pp. 227 – 233, 2015.
  • Efficient Semantic Features for Automated Reasoning over Large Theories
    Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
    Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 3084 – 3090, 2015.
  • System Description: E.T. 0.1
    Cezary Kaliszyk, Stephan Schulz, Josef Urban, and Jiří Vyskočil
    Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 389 – 398, 2015.
  • Beagle as a HOL4 External ATP Method
    Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, and Michael Norrish
    Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), EasyChair Proceedings in Computer Science 31, pp. 50 – 59, 2015.
  • Formalizing Physics: Automation, Presentation and Foundation Issues
    Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, and Sofiène Tahar
    Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015), Lecture Notes in Computer Science 9150, pp. 288 – 295, 2015.
  • HOL(y)Hammer: Online ATP Service for HOL Light
    Cezary Kaliszyk and Josef Urban
    Mathematics in Computer Science 9(1), pp. 5 – 22, 2015.
  • Premise Selection and External Provers for HOL4
    Thibault Gauthier and Cezary Kaliszyk
    Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),   pp. 49 – 57, 2015.
  • Certified Connection Tableaux Proofs for HOL Light and TPTP
    Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
    Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),   pp. 59 – 66, 2015.
  • Learning-assisted Theorem Proving with Millions of Lemmas
    Cezary Kaliszyk and Josef Urban
    Journal of Symbolic Computation 69, pp. 109 – 128, 2015.
  • Machine Learning of Coq Proof Guidance: First Experiments
    Cezary Kaliszyk, Lionel Mamane, and Josef Urban
    Proceedings of the 6th International Symposium on Symbolic Computation in Software Science (SCSS 2014), EasyChair Proceedings in Computer Science 30, pp. 27 – 34, 2014.
  • Towards Knowledge Management for HOL Light
    Cezary Kaliszyk and Florian Rabe
    Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science 8543, pp. 357 – 372, 2014.
  • Matching Concepts across HOL Libraries
    Thibault Gauthier and Cezary Kaliszyk
    Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science 8543, pp. 267 – 281, 2014.
  • Learning-Assisted Automated Reasoning with Flyspeck
    Cezary Kaliszyk and Josef Urban
    Journal of Automated Reasoning 53(2), pp. 173 – 213, 2014.




Nach oben scrollen