### 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:

- proof translation between various logic and external first and higher order ATPs (automated theorem provers);
- providing stronger machine learning-based premise selection;
- 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 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 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.

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.