Proofs as Formal Objects and as Data Structures

– Project Page –

- Principal researcher: Christoph Wernhard
- Funding by DFG starting in August 2021
- Hosted by University of Potsdam, Chair of Theoretical Computer Science

The project is in the area of automated reasoning, a central subfield of Artificial Intelligence, whose topic is the investigation of reasoning by means of the computer. Typical automated reasoning systems create proof structures: representations of proofs, combined deduction steps, as data structures. Proof structures can be understood on the one hand as formal objects that are related in specific ways to logical formulas, and, on the other hand, as data objects that materialize these formal objects and can be used for practical applications. Starting out from the investigation of proof structures in this sense, the project aims at both, improving the capability of automated reasoning systems to find proofs, and extending the range of tasks that can be solved by them, beyond theorem proving in the strict sense.

Aside of the interplay of theoretical and experimental methods that characterizes the field of automated reasoning, a specific methodical aspect of the project is the analysis of given proofs. Of particular relevance is there an extensive corpus of advanced formal proofs from the literature before the broad availability of computers, which still can not be found in a satisfactory way by automated methods.

The specific objectives of the project are:

- Improving the capability of first-order theorem provers to find proofs, in particular through novel calculi, guided by abstractions emerging from the orientation at proof structures and by observations made in the analysis of proofs.
- Theoretically well-understood and implemented proof transformations for various practical applications, such as shortening or simplification of proofs, discovery and abstraction of repetitions and regularities in proofs, or mappings between calculi to enable the combination of different systems.
- Applicability of automated reasoning to query reformulation for integrating data and knowledge bases as well as query optimization. It is planned to refine and extend an approach to query reformulation that is based on Craig interpolation, a fundamental relationship in first-order logic between proof structures and associated formulas.
- Progress in certain advanced issues of theoretical and practical interest that are related to the core techniques considered in the project, Craig interpolation and condensed detachment. The latter is the primary proof representation in the analyzed literature. Goals are in particular the overcoming of known limitations, insights into relationships to further techniques, and availability of further application possibilities.

In André Platzer and Geoff Sutcliffe,
editors, *Automated Deduction: CADE 2021*, volume 12699 of *LNCS
(LNAI)*, pages 58-75. Springer, 2021.

[ Preprint
(extended version):
https://arxiv.org/abs/2104.13645
| Presentation slides
]

[
Preprint: https://arxiv.org/abs/2008.03489 ]

Contact: info@christophwernhard.com