Department of Computer Science
University of Innsbruck
Home Research Teaching Members Events News Jobs
Research
publications projects software

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

FWF Standalone Project, project number

P26201

Contact

cezary.kaliszyk at 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 Jakubův, 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.

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 Urban
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.