In diesem Seminar werden sowohl theoretische Grundlagen als auch aktuelle Techniken zur Realisation von interaktiven und automatischen Theorembeweisern für klassische Logik höherer Stufe (HOL) diskutiert. Theorembeweiser sind Programme, die eine Menge von Annahmen ("Axiome") und eine Behauptung annehmen und dann versuchen zu beweisen (oder zu widerlegen), dass die Behauptung eine logische Konsequenz der Annahmen ist. Theorembeweiser können z.B. zur Programmverfikation (beweise, dass bestimmte Zusicherungen gelten), zur Beweisassistenz (bestötige dass meine Beweisführung korrekt ist) und in weiteren Einsatzgebieten formaler Methoden verwendet werden. Ebenso ist durch jüngere Forschungsresultate bestätigt, dass insbesondere Theorembeweiser für Prädikatenlogik höherer Stufe für die Verfikation/Analyse von Argumenten aus der theoretischen Philosophie/Metaphysik eingesetzt werden können.

Was sind die mathematischen Grundlagen für solche Programme? Wie implementiert man diese (effizient)? Viele der Themen sind aktuelle Forschungsgegenstände und können in ambitionierte Bachelor- und Masterarbeiten münden. Die Veranstaltung ist für 15 Studierende ausgelegt.

Vortragsthemen können umfassen:

• Einfach getypter Lambda-Kalkül: wichtigste theoretische Eigenschaften, sowie Beispiele (z.B. Church Numerals, ...);
• Einführung in die Logik höherer Stufe (HOL): Historie und Abgrenzung, Syntax, Semantik;
• Kalküle, Korrektheit, Vollständigkeit;
• Cut-Elimination, Cut-Simulation;
• Unifikation, Pre-Unifikation;
• Skolemisierung, Normalformen;
• Transformationen in Logik erster Stufe;
• Implementierungstechniken (Indexing, Selektionsheuristiken, ...);

und weiteres