|
Logik in der Informatik
Prof. Dr. Martin Grohe |
 Institut für Informatik |
An dieser Stelle finden Sie im Laufe der Vorlesung aktuelle Mitteilungen
Automatische Theorembeweiser, also Programme, mit deren Hilfe man korrekte Folgerungen aus einer formalisierten Theorie ziehen kann, spielen eine wichtige Rolle als Werkzeuge in der Hard- und Softwareverifikation und der künstlichen Intelligenz.
In der Vorlesung sollen die grundlegenden Techniken vorgestellt werden, die in modernen Theorembeweisern verwendet werden. Im Projektteil erhalten die Studierenden die Möglichkeit, diese Techniken in eigenen, prototypischen Theorembeweisern umzusetzen und zu erproben.
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungen und gelegentlich ergänzende Bemerkungen.
Ergänzend zu den Vorlesungen findet ein Projekt statt.
Die ASCII-Syntax als Gerüst für Lex- und Yacc-artige Werkzeuge: syntax.lex syntax.yacc.
Für das bestandene Projekt gibt es einen Schein, der zur Zulassung zur Prüfung berechtigt. Zu Beginn der Semesterferien finden dann mündliche Prüfungen statt.
Melvin Fitting: First-Order Logic and Automated Theoren Proving, 2. Auflage, Springer, 1996
Reiner Hähnle und Bernhard Beckert: Vorlesungsskriptum Automatisches Beweisen, Universität Karlsruhe, 2001
Alan Robinson und Andrei Voronkov (Hrsg.): Handbook of Automated Reasoning, Elsevier, 2001. Darin vor allem Kapitel 3 (Reiner Hähnle: Tableaux and Related Methods) und Kapitel 28 (Reinhold Letz und Gernot Stenz: Model Elimination and Connection Tableau Procedures)
Außerdem sind hier die Folien der Wiederholung der Grundbegriffe der Logik der ersten Stufe.