Theorem proving, Winter 2000/01

Theorembeweisen

Wintersemester 2000/01

Veranst: 8745/8746?

Ort: Haus II, HO 2
Vorbesprechung: keine
Termin: Di, 11 - 13 & Do 11 - 13
Übung: Di, nach der Vorlesung

[Inhalt] [Organisatorisches] [Unterlagen] [Handouts] [Aufgaben] [Literatur] [Software] [Links]

Inhalt

Unter Theorembeweisen versteht man das maschinenunterstützte Finden logischer Beweise. Es verbindet die Gebiete der mathematischen Logik mit algorithmischen Fragen nach effizienten Suchstrategien, adäquater Maschinenrepräsentierung und Organisation von Beweisen und anderem mehr. Mit Anwendungen von Logikprogrammierung über die Programmverifikation und Hardwaresynthese bis hin zu Datenbanken, Expertensystemen und künstlicher Intelligenz stellt Theorembeweisen eine wichtige Disziplin der Informatik dar. Ziel der Vorlesung ist es, in die Prinzipien des automatischen Beweisen und ihre algorithmischen Umsetzungen einzuführen sowie einen Einblick in den aktuellen Stand moderner Werkzeuge auf dem Gebiet zu geben.

Von den Grundlagen der Aussagen- und Prädikatenlogik ausgehend wird die Vorlesung die wichtigsten für die Automatisierung geeigneten Beweissysteme behandeln, unter anderem Gentzensysteme und Systeme natürlichen Schließens sowie Resolutionsmethoden. Spätere Teile der Vorlesung behandeln die Umsetzung in verschiedene Klassen von Theorembeweisern. Ein Schwerpunkt der begleitenden Übungen wird der Umgang mit verschiedenen Beweiswerkzeugen sein.

Organisatorisches

Anmeldung:

Wir bitten um schriftliche (per email) Anmeldung für den Kurs und die Angabe folgender Daten:

Name,
Email-Adresse
Semesterzahl

Nachbereitung:

...

Aufgaben

Literatur

First-Order Logic and Automated Theorem Proving, Melvin Fitting, Springer-Verlag, 1996, zweite Ausgabe
Basic proof theory, Troelstra, Schwichtenberg, Cambridge University Press, 1990.
Principles of Automated Theorem Proving, David Duffy, Wiley, 1991