Algorithmic Structuring and Compression of Proofs

Proofs are the most important carriers of mathematical knowledge. From the early days of automated deduction to the current state of the art in automated and interactive theorem proving we have witnessed a huge increase in the ability of computers to search for, formalise and work with proofs. Computer-generated proofs are typically analytic, i.e. they essentially consist only of formulas which are already present in the theorem that is shown. In contrast, mathematical proofs written by humans almost never are: they are highly structured due to the use of lemmas. Because of this reason, computer-generated proofs are typically very difficult if not impossible to understand for a human reader. This project aims at developing algorithms and software which structure and abbreviate analytic proofs by computing useful lemmas. Since the very beginning of structural proof theory it is well understood that arbitrary proofs can be transformed into analytic proofs and how to do it: by cut-elimination The approach we propose for this project is to reverse cut-elimination. Given an analytic proof (e.g. one that has been generated algorithmically) the task is to transform it into a shorter and more structured proof of the same theorem by the introduction of cuts which - at the mathematical level - represent lemmas. This approach is rendered possible by recent ground-breaking results which established a new connection between proof theory and formal language theory. These insights allow the application of efficient algorithms based on formal grammars to structure and compress proofs. This project will build on recent preliminary work on a proof-of-concept algorithm which uses this approach for the introduction of a single quantified cut. Its central theoretical aim is to extend the algorithm to cover stronger classes of cuts. The algorithms will also be implemented in order to apply them to actual proofs, e.g. as post- processing to automated theorem provers. The implementation will be based on the GAPT-project which is developed at the proposed host institution and provides a general framework for proof-theoretic algorithms The ultimate aim of this project is to provide a software system which is given an analytic first-order proof as input and computes formulas (from full first-order logic) as lemmas which optimally compress the input proof.

Proofs are the most important carriers of mathematical knowledge. From the early days of automated deduction to the current state of the art in automated and interactive theorem proving we have witnessed a huge increase in the ability of computers to search for, formalise and work with proofs. Computer-generated proofs are typically analytic, i.e. they essentially consist only of formulas which are already present in the theorem that is shown. In contrast, mathematical proofs written by humans almost never are: they are highly structured due to the use of lemmas. Because of this reason, computer-generated proofs are typically very difficult if not impossible to understand for a human reader. In this project we have developed algorithms and software which structure and abbreviate analytic proofs by computing useful lemmas. Since the very beginning of structural proof theory it is well understood that arbitrary proofs can be transformed into analytic proofs and how to do it: by cut-elimination. The approach we are following is to reverse cut-elimination. Given an analytic proof (e.g. one that has been generated algorithmically) the task is to transform it into a shorter and more structured proof of the same theorem by the introduction of cuts which at the mathematical level - represent lemmas. This approach is rendered possible by recent ground-breaking results which established a new connection between proof theory and formal language theory. These insights allow the application of efficient algorithms based on formal grammars to structure and compress proofs. The central theoretical result of this project was to extend this connection to cover stronger classes of cuts. The algorithms have also been implemented in order to apply them to actual proofs, e.g. as post-processing to automated theorem provers. The implementation is based on the GAPT-project which is developed at the host institution and provides a general framework for proof-theoretic algorithms.