Proof Structures:
Proofs as Formal Objects and as Data Structures
– Project Page –

About the Project Related Systems Related Events Related Publications

About the Project

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:

  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.

Related Systems

Related Events

Related Publications

Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Jan Heuer and Christoph Wernhard
In Chris Benzmüller, Marjin Heule, and Renate Schmidt, editors, International Joint Conference on Automated Reasoning, IJCAR 2024, LNCS (LNAI). Springer, 2024.
To appear, preprint: https://arxiv.org/abs/2402.07696.
[ bib | Abstract ]
Synthesizing Nested Relational Queries from Implicit Specifications: Via Model Theory and via Proof Theory
Michael Benedikt, Cécilia Pradic, and Christoph Wernhard
Logical Methods in Computer Science, 2024.
To appear, preprint: http://arxiv.org/abs/2212.03085.
[ bib | Abstract ]
Structure-Generating First-Order Theorem Proving
Christoph Wernhard
In Jens Otten and Wolfgang Bibel, editors, AReCCa 2023 - Automated Reasoning with Connection Calculi, International Workshop, volume 3613 of CEUR Workshop Proceedings, pages 64-83. CEUR-WS.org, 2024.
[ Presentation slides ].
[ bib | .pdf | Abstract ]
Range-Restricted and Horn Interpolation through Clausal Tableaux
Christoph Wernhard
In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, LNCS (LNAI). Springer, 2023.
[ Preprint (extended version): https://arxiv.org/abs/2306.03572 ].
[ bib | DOI | Abstract ]
Lemmas: Generation, Selection, Application
Michael Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang Bibel
In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, LNCS (LNAI). Springer, 2023.
[ Preprint (extended version): https://arxiv.org/abs/2303.05854 ].
[ bib | DOI | Abstract ]
Automated Verification of Equivalence Properties in Advanced Logic Programs
Jan Heuer
In Sibylle Schwarz and Mario Wenzel, editors, Workshop on (Constraint and Functional) Logic Programming, WLP 2023, 2023.
[ Online ]
Learning to Identify Useful Lemmas from Failure
Michael Rawson, Christoph Wernhard, and Zsolt Zombori
In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 8th Conference on Artificial Intelligence and Theorem Proving, AITP 2023 (Informal Book of Abstracts), 2023.
[ Extended abstract | Presentation slides ].
[ bib ]
Investigations into Proof Structures
Christoph Wernhard and Wolfgang Bibel
2023.
[ Preprint (submitted): https://arxiv.org/abs/2304.12827 ].
[ bib | Abstract ]
Synthesizing Nested Relational Queries from Implicit Specifications
Michael Benedikt, Cécilia Pradic, and Christoph Wernhard
In Principles of Database Systems, PODS 23, pages 33-45, 2023.
[ bib | DOI | Abstract ]
Compressed Combinatory Proof Structures and Blending Goal- with Axiom-Driven Reasoning: Perspectives for First-Order ATP with Condensed Detachment and Clausal Tableaux
Christoph Wernhard
In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 7th Conference on Artificial Intelligence and Theorem Proving, AITP 2022 (Informal Book of Abstracts), 2022.
[ Extended abstract | Presentation slides ].
[ bib ]
Generating Compressed Combinatory Proof Structures - An Approach to Automated First-Order Theorem Proving
Christoph Wernhard
In Boris Konev, Claudia Schon, and Alexander Steen, editors, 8th Workshop on Practical Aspects of Automated Reasoning, PAAR 2022, volume 3201 of CEUR Workshop Proceedings. CEUR-WS.org, 2022.
[ Preprint: http://cs.christophwernhard.com/papers/css.pdf ].
[ bib | Abstract ]
CD Tools - Condensed Detachment and Structure Generating Theorem Proving (System Description)
Christoph Wernhard
Technical report, 2022.
https://arxiv.org/abs/2207.08453.
[ bib | DOI | Abstract ]
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
Christoph Wernhard
In Renate A. Schmidt, Christoph Wernhard, and Yizheng Zhao, editors, Proceedings of the Second Workshop on Second-Order Elimination and Related Topics (SOQE 2021), volume 3009 of CEUR Workshop Proceedings, pages 98-111, 2021.
[ Preprint (extended version): https://arxiv.org/abs/2110.11108 ].
[ bib | .pdf | Abstract ]
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures
Christoph Wernhard and Wolfgang Bibel
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 ]
[ DOI | bib ]
Craig Interpolation with Clausal First-Order Tableaux
Christoph Wernhard
Journal of Automated Reasoning, 65(5):647-690, 2021.
[ Preprint: https://arxiv.org/abs/2008.03489 ]
[ DOI | bib ]

Contact: info@christophwernhard.com