Logik in der Informatik
Prof. Dr. Martin Grohe

Institut für Informatik

Projektvorlesung Theorie und Anwendung von Theorembeweisern

Aktuelles  Einführung  Inhalt  Logbuch  Vorlesung  Projekt  Literatur

Aktuelles

An dieser Stelle finden Sie im Laufe der Vorlesung aktuelle Mitteilungen

Einführung

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.

Logbuch

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungen und gelegentlich ergänzende Bemerkungen.

Informationen zum Vorlesungsbetrieb

Zeiten und Raum
Dienstags 13-15 Uhr im Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'306
 
Dozenten
Prof. Dr. Martin Grohe
Sprechstunde: Freitags 10:00 - 11:00
Dipl. Math. Mark Weyer
Sprechstunde: Mittwochs 14:00 - 15:00

Projekt

Ergänzend zu den Vorlesungen findet ein Projekt statt.

Zeit und Raum
Donnerstags 13-15 Uhr im Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'306
 
Projektbetreuer
Dipl. Math. Mark Weyer
Sprechstunde: Mittwochs 14:00 - 15:00

Ressourcen:

Die ASCII-Syntax als Gerüst für Lex- und Yacc-artige Werkzeuge: syntax.lex syntax.yacc.

Prüfung

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.

Literatur

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.

Last modified: Tue Apr 18 13:01:50 CEST 2006
Martin Grohe