Seminar Theoretische Informatik - Methoden des automatischen Theorembeweisens
- Seminar, Frank, Mi. 12:00-14:00, 3.04.2.01
In diesem Seminar werden vertiefende Themen der theoretischen Informatik und angrenzender Bereiche der Mathematik anhand von ausgewählter Literatur besprochen.
Das Thema des WS 2014 ist "Methoden des automatischen Theorembeweisens"
Im Seminar werden Konzepte und Algorithmen für das automatische
Theorembeweisen durch die Studierenden vorgestellt. Dabei werden sowohl
Beweissuch-Algorithmen, als auch Entscheidungsprozeduren für spezielle
Probleme behandelt. Ziel des Seminars ist, dass die Studierenden sich
das Verständnis für diverse Lösungsstrategien für das automatische
Theorembeweisen aneignen und Implementationen anfertigen können.
Das automatische Theorembeweisen lässt sich beispielsweise dafür nutzen, Software und Hardware formal zu verifizieren oder sogar zu synthetisieren. Dabei gibt es Schnittmengen zu SAT-Solvern, die jedoch im allgemeinen nicht über Aussagenlogik hinausgehen. SMT-Solver gehen noch ein wenig weiter als SAT-Solver und unterstützen beispielsweise Aussagenlogik in Kombination mit Gleichheiten. Automatische Theorembeweiser unterstützen beispielsweise Prädikatenlogik erster oder sogar höherer Ordnung und zumeist auch Gleichheiten. Seit mehr als 10 Jahren gibt es sogar Weltmeisterschaften für Theorembeweiser und SAT-Solver in denen auch Probleme aus der Praxis, beispielsweise aus der automotiven Industrie bewiesen werden.
Moodle-Kurs: Der Kurs heißt im Moodle "ATP-Seminar". Link : https://moodle2.uni-potsdam.de/course/view.php?id=6088
Die Vortragsthemen werden nach Präferenzen vergeben.
Vortragsthemen (Weitere auf Wunsch möglich):
- Logiken - Syntax, Semantik und Normalformen
- Entscheidungsprozeduren für Wortprobleme - Unifikation
- Unifikation nach Robinson
- Unifikation nach Martelli-Montanari
- Unifikation nach Escalada-Ghallab
- Kalküle
- Resolution
- DPLL
- Semantisches Tableau
- Konnektions-Methode
- Inst-Gen-Kalkül
- Paramodulation
- Superposition
- Entscheidungsprozeduren für Theorien
- Kongruenz-Hüllen-Algorithmus
- Knuth-Bendix-Ordering
- Recursive Path Ordering
- Sup-Inf Methode
Während Teil 1 durch den Dozenten in den ersten Wochen vorgestellt wird, werden die Themen der Teile 2, 3 und 4 durch
Studierende vorgestellt.
Für die Vorträge müssen keine Folien angefertigt werden. Statt dessen werden die Themen in einem Wiki aufgearbeitet,
damit Studierende, die Konzepte anderer Studierenden verwenden, auf diese verweisen können.
Leistungserfassung:
- Vortrag (Dauer: 25 Minuten) + Diskussion
- Naive aber korrekte Implementierung des vorgestellten Konzeptes
Literatur
Leittext:
Leittexte sind überwiegend spezifische Fachartikel zu einzelnen Themen.
Diese werden im Moodle zur Verfügung gestellt.
Interessante/Relevante Literatur:
- J. Robinson & A. Voronkov eds., Handbook of Automated Reasoning, Elsevier and MIT Press, 2001.
- W. Bibel, Deduktion: Automatisierung der Logik, Oldenbourg Wissenschaftsverlag, 1992
- R. M. Smullyan, First-Order Logic, Dover Pubn Inc, 1995
