Proof Structures: Proofs as Formal Objects and as Data Structures

• Applicant: Dr. Christoph Wernhard
• Subject Area: Methods in Artificial Intelligence and Machine Learning
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 457292495

The field of the project is Automated Reasoning, a central subfield of AI, dedicated to the investigation of reasoning by means of the computer with a methodology that combines theoretical and experimental aspects. Typical systems of Automated Reasoning construct proof structures: representations of proofs, combined deduction steps. Proof structures can be understood on the one hand as formal objects, related in specific ways to logical formulas, and, on the other hand, as data objects that materialize the formal objects and be passed as inputs to practical applications. Examples are there query reformulation for knowledge integration, synthesis of logic programs, and organizing formalized mathematical knowledge. In the context of recent AI applications proof structures provide explanations in an ideal form that permits a formal access such that their investigation is expected to yield foundational and exemplary insights. The general objective of the project is the improvement of Automated Reasoning systems, in their capability to find proofs as well as by extending their range of applications. Given the results from the first funding period of the project, for the proposed renewal this splits into the following four specific objectives: (1) Improvements in finding proofs. The result so far is a framework that starts out from generating proof structures. Its novel methods result from the combination of features from different prover paradigms and the incorporation of proof compression. A hard problem was solved fully automatically for the first time. The project now aims at a thorough systematic understanding of the framework, new variations, and applicability to further problem classes. (2) Improvements and novel applications of proving systems in the context of a large library of formalized mathematical knowledge. Goals are improvements through proof analysis and machine learning, where previous project results will be scaled up, as well as generating alternate views on mathematical knowledge by restructuring, reducing and compressing proofs. (3) Improvements of query reformulation by interpolation for knowledge representation. The output query is there computed from a proof. The first method that uses there general automated provers results from the project. The goal is now to make relationships to special application formalisms precise. A further project result addresses nested relations. The goal is there transfer to practice via methods of automated theorem proving. (4) Improvements of program synthesis in answer set programming, an approach to declarative problem solving. Program synthesis, based on interpolation, is a recent project result. The goal is to put it into practice, taking account of ongoing developments in answer set programming.

• DFG Programme: Research Grants