Proof Structures: Proofs as Formal Objects and as Data Structures

• Applicant: Dr. Christoph Wernhard
• Subject Area: Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 457292495

The proposed 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: (1) 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. (2) 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. (3) 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. (4) 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.

• DFG Programme: Research Grants