In the focus of the seminar are proofs as emitted by automated systems. We will consider issues such as:

• Approaches to short proofs related to modern SAT pre- and inprocessing techniques
• Short proofs through structure compression
• Computations on the basis of proofs, for example Craig interpolation, which can be used for query reformulation and verification
• Criteria for "good" proofs that are suited as explanations
• Formal proofs by humans and AI perspectives

The seminar is based on literature that presents background material and recent research papers.

Literature Suggestions

Background: Propositional Proofs

• Marijn J.H. Heule:
  "Proofs of Unsatisfiability"
  (in particular sections 15.1-15.2)
  Chapter 15 of Armin Biere et al. (eds.) "Handbook of
  Satisfiability", 2. ed., IOS Press, 2021,
  pp 635-668
  https://www.cs.cmu.edu/~mheule/publications/p01c15-prf.pdf

Short Propositional Proofs

• Wolfgang Bibel:
  "Short Proofs of the Pigeonhole Formulas Based on the Connection Method"
  Journal of Automated Reasoning 6, pp 287-297, 1990
  https://doi.org/10.1007/BF00244489
  
  
• Marijn J.H. Heule, Benjamin Kiesl, Armin Biere:
  "H2 Extension-Free Proofs"
  Journal of Automated Reasoning 64, pp 533–554, 2020
  https://doi.org/10.1007/s10817-019-09516-0
  
  
• A related talk by Marijn Heule on YouTube:
  https://www.youtube.com/watch?v=TRZ0LIifhi4

Background: Interpolation and Definability

• Melvin Fitting:
  "First-Order Logic and Automated Theorem Proving",
  2nd Edition
  (in particular Sect. 8.11-8.13)
  Springer,
  1996

Background: Clausal Tableaux

• Reiner Hähnle:
  "Tableaux and Related Methods"
  (in particular Sect. 4)
  In: Alan Robinson and Andrei Voronkov (eds.) "Handbook
  of Automated Reasoning", pp 100-178
  https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.132.9224

Interpolation with Clausal Tableaux

• Christoph Wernhard:
  "Craig Interpolation with Clausal First-Order Tableaux"
  Journal of Automated Reasoning 65, pp 647-690, 2021
  https://doi.org/10.1007/s10817-021-09590-3

Short Propositional Proofs and Interpolation

• Adrian Rebola Pardo:
  "Interpolation and Interference"
  iPRA 2022 – the 4th Workshopp on Interpolation:
  From Proofs to Applications, Book of Abstracts,
  pp 27-35, 2021
  https://ipra-2022.bitbucket.io/iPRA2022.pdf

Background: Condensed Detachment

• Dolph Ulrich:
  "A Legacy Recalled and a Tradition Continued"
  Journal of Automated Reasoning 27, pp 92-122, 2001
  https://doi.org/10.1023/A:1010683508225
  
  
• Christoph Wernhard, Wolfgang Bibel:
  "Learning from Lukasiewicz and Meredith:
  Investigations into Proof Structures"
  In "Automated Deduction - CADE 2021", pp 58-75,
  Springer LNCS(LNAI), Vol 12699, 2021
  https://doi.org/10.1007/978-3-030-79876-5_4

The course language is English or German, depending on the participants.

The schedule is planned as follows: A regular weekly introductory part at the beginning, some intermediate meetings, and a final part in blocked form with the main student presentations.

Basic knowledge of propositional logic and predicate logic is presupposed.

Helpful is some knowledge of processing methods for logics and practical systems that realize these. For example, Prolog, first-order theorem provers, proof assistants, SAT solvers, Answer Set Programming systems or Description Logic reasoners.