Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 

Foto: Matthias Friel

Proofs by Automated Systems: Applications and Desirable Features - Einzelansicht

  • Funktionen:
Veranstaltungsart Seminar Veranstaltungsnummer 555611
SWS 2 Semester WiSe 2022/23
Einrichtung Institut für Informatik und Computational Science  
Gruppe 1:
    Tag Zeit Rhythmus Dauer Raum Lehrperson Ausfall-/Ausweichtermine Max. Teilnehmer/-innen
Seminar Do  bis  wöchentlich am   Dr. Wernhard fällt aus

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

Short Propositional Proofs

Background: Interpolation and Definability

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

Background: Clausal Tableaux

Interpolation with Clausal Tableaux

Short Propositional Proofs and Interpolation

Background: Condensed Detachment


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.

Keine Einordnung ins Vorlesungsverzeichnis vorhanden. Veranstaltung ist aus dem Semester WiSe 2022/23 , Aktuelles Semester: SoSe 2024