Universität Karlsruhe
Institut für Logik, Komplexität und Deduktionssysteme
Dr. Bernhard Beckert
Automatisches Beweisen
Vorlesung im Sommersemester 2002
Achtung: Neuer Termin
Der Donnerstag-Termin ist auf Mittwochs, 14 Uhr, verlegt (Ort: SR236).
Semesterwochenstunden:
Die Vorlesung hat 3 (drei) SWS.
Vertiefungsfächer:
Die Vorlesung gehört zu den beiden Vertiefungsfächern "Logik und theoretische
Grundlagen" und "Deduktionssysteme".
Inhalt
Automatische Beweisverfahren werden in der einen oder anderen Weise vielerorts
verwendet, zum Beispiel im logischen Programmieren, in deduktiven Datenbanken,
in der Hard- und Softwareverifikation, in der Computerlinguistik... Die
Vorlesung gibt einen Überblick über das Gebiet "Automatisches Beweisen":
-
Vorstellung und Diskussion aller wichtigen verwendeten Kalkülklassen und
Inferenzprozeduren im Automatischen Beweisen.
-
Eingehen auf Zusammenhänge zwischen Kalkülen und deren Grenzen.
-
Einordnung der besprochenen Kalküle und Prozeduren bezüglich Anwendungen
und möglicher Erweiterungen.
Der Besuch der Vorlesung "Formale Systeme" wird vorausgesetzt; dennoch
werden die für das automatische Beweisen relevanten Inhalte von "Formale
Systeme" am Anfang der Vorlesung noch einmal kurz rekapituliert.
Zeiteinteilung
Die Vorlesung hat drei Semesterwochenstunden; sie wird aber dennoch zum
Ausgleich während des Semesters ausfallender Vorlesungen regelmäßig
vierstündig gehalten.
Zeit: Dienstags 11:30 Uhr und Donnerstags 14:00 Uhr (erstmals am 16.04.2002).
Ort: Seminarraum 301, Informatik-Hauptgebäude.
Vorläufiger Zeitplan (Vorlesungstermine)
| Dienstag | Donnerstag |
| 16.04. | 18.04. |
| 23.04. | 25.04. |
| 30.04. | - |
| Dienstag | Mittwoch |
| - | Tag der Arbeit |
| 07.05. | 08.05. |
| 14.05. | 15.05. |
| 21.05. | 22.05. |
| 28.05. | 29.05. |
| 04.06. | - |
| Konferenz | Konferenz |
| 18.06. | 19.06. |
| 25.06. | 26.06. |
| 02.07. (Ausweichtermin) | Sportfest |
Folien
Jeweils nach der Vorlesung werden die Folien hier zur Verfügung gestellt.
- Vorlesung vom 16.04.02
- Vorlesung vom 18.04.02
- Vorlesung vom 23.04.02
- Vorlesung vom 25.04.02
- Vorlesung vom 30.04.02
- Vorlesung vom 07.05.02
- Vorlesung vom 08.05.02
- Vorlesung vom 14.05.02
- Vorlesung vom 15.05.02
- Vorlesung vom 22.05.02
- Vorlesung vom 23.05.02
- Vorlesung vom 28.05.02
- Vorlesung vom 29.05.02
- Vorlesung vom 04.06.02
- Vorlesung vom 18.06.02
- Vorlesung vom 19.06.02
- Vorlesung vom 25.06.02
- Vorlesung vom 26.06.02
Automatische Beweiser (Implementierungen)
Eine kleine Auswahl automatischer Beweissysteme:
Skriptum
Das Skriptums zur Vorlesung steht als PostScript-Datei zur Verfügung:
skriptum.ps.gz (577K). Dies ist die Version vom letzten Jahr, die neue wird rechtzeitig hier zur Verfügung stehen.
Das Skriptum wurde von Reiner Hähnle erstellt, der die Vorlesung bis 1998 las. Ich habe es überarbeitet, aktualisiert und an den Stoff der Vorlesung, wie ich sie
seit 1999 regelmäßig halte, angepaßt.
beckert@kit.edu
$Id: index.html,v 1.22 2002/05/15 16:41:34 beckert Exp beckert $