Siehe TUMonline

Eine anwendungsorientierte Einführung in das automatische und interaktive Beweisen, aufgebaut als Aufstieg durch zunehmend ausdrucksstärkere Logiken und die Beweissuchverfahren, die sie jeweils erfordern. Der Schwerpunkt liegt darauf, wie moderne Beweissysteme funktionieren und wie man sie einsetzt; Grundlagenresultate werden präzise formuliert, die Beweise auf der Ebene der Beweisidee skizziert. Vier Blöcke zu je fünf Vorlesungen und einer Übung.

**Block 1: SAT.** Erfüllbarkeit, konjunktive Normalform, NP-Vollständigkeit. DPLL und Conflict-Driven Clause Learning (CDCL). Implementierungstechniken. Beweiszertifikate: DRAT, LRAT und die Prüfung durch einen kleinen vertrauenswürdigen Checker. Kodierungen und Anwendungen.

**Block 2: SMT.** SMT-LIB und die gängigen Theorien. Der Eager-Ansatz (Reduktion auf SAT) und seine Grenzen. DPLL(T). Theorie-Solver: inkrementelles Simplex-Verfahren mit Farkas-Zertifikaten, Congruence Closure, Arrays. Theoriekombination nach Nelson-Oppen. Z3 und cvc5.

**Block 3: Automatisches Beweisen in der Prädikatenlogik erster Stufe.** Semi-Entscheidbarkeit und entscheidbare Fragmente. Unifikation und Resolution. Reduktionsordnungen, LPO und KBO, und das Problem der Gleichheit. Superposition, Redundanz, Saturation. Architektur eines Beweisers; TPTP; E und Vampire.

**Block 4: Interaktives Beweisen in Lean.** Abhängige Typen, Curry-Howard, vertrauenswürdiger Kern und de-Bruijn-Kriterium. Beweisterme und Taktiken. Automatisierung über Mathlib, zurückgeführt auf die Verfahren der vorangegangenen Blöcke. Formalisierung großer Entwicklungen; Hammers, Premise Selection, Autoformalization.

Grundlagen der mathematischen Logik oder der diskreten Mathematik: Aussagen- und Prädikatenlogik, Induktionsbeweise. Für die praktischen Übungsaufgaben sichere Programmierkenntnisse in einer gängigen Programmiersprache: die Studierenden vervollständigen ein vorgegebenes Beweiser-Grundgerüst und schreiben Skripte gegen die Schnittstellen der eingesetzten Werkzeuge.

Vorkenntnisse zu Beweisassistenten oder Werkzeugen des automatischen Beweisens werden nicht vorausgesetzt. Das Modul Logik (IN2049) ist eine sinnvolle, aber keine notwendige Vorbereitung.

**Vorlesungen** stellen die Algorithmen, die Resultate und die Implementierungstechniken dar, mit kurzen Werkzeugdemonstrationen dort, wo ein System behandelt wird.

**Übungen**, eine je Block, dienen dem angeleiteten Problemlösen und der Besprechung der eingereichten Lösungen.

**Übungsaufgaben**, eine je Block, bilden den wesentlichen Teil des Selbststudiums und erstrecken sich über den gesamten Block. Jede verbindet leichtere theoretische mit umfangreicheren praktischen Aufgaben, die die eigenständige Arbeit mit einem aktuellen System erfordern.