WS 2013/14: Logik erster Stufe --- Theorie und Praxis
Vorlesung und Übung (Nr. 19619) - 2+2-stündig, ECTS: 5
Dozent: Christoph Benzmüller
Übungen: Fritz Ulbrich
Termine: werden noch bekannt gegeben
Zielgruppe: Studenten mit Interesse an Logik, Automatischem
Theorembeweisen und Künstlicher Intelligenz
Voraussetzungen: Grundlagen der theoretischen Informatik
Maximale Anzahl von Teilnehmern: 35
Wiki: wird noch eingerichtet
Website: http://christoph-benzmueller.de/2013-FOL/
Klausur: Termine werden noch bekannt gegeben
Synopsis
Diese Vorlesung kombiniert
- A) eine kompakte Einführung in die Theorie von Logik erster Stufe mit
- B) einem praktischen Training zur Verwendung von Theorembeweisern für die Logik erster Stufe in Anwendungen.
Hinsichtlich A) orientiert sich die Vorlesung am Lehrbuch von
Fitting [1] (Harrison [2] ist ebenfalls empfohlen). Zu den Themen der Vorlesung zählen:
- Syntax und Semantik von Aussagenlogik und Logik erster Stufe,
- Herbrand Modelle,
- Hintikka Mengen und Abstrakte Konsistenz,
- Korrektheit und Vollständigkeit,
- Semantische Tableaux und Resolution,
- Implementierung.
Hinsichtlich B) konzentriert sich die Vorlesung auf eine Einführung in die TPTP Infrastruktur [4]. Angesprochene Themen sind:
- TPTP Sprache(n),SZS Ontologie für Beweiserresultate,
- TPTP und TSTP Problem- und Beweis-Bibliotheken,
- Anwendung von TPTP kompatiblen Beweisern,
- weitere TPTP Werkzeuge und Systeme,
- (TPTP für Logik höherer Stufe).
In Teil B) der Vorlesung werden praktische Übungen im Vordergrund stehen. Sofern Zeit bleibt, wird in der Vorlesung auch ein kurzer Ausblick auf Theorie und Praxis von Logik höherer Stufe geboten (ein Thema, das evtl. im Rahmen einer Vorlesung im SS 2013 vertieft werden wird).
Es wird den Teilnehmern empfohlen, sich bereits im Vorfeld in
[1] und [5] einzuarbeiten (auch [2] wird sehr empfohlen).
Literatur
- zu A):
[1] Melvin Fitting, First-Order Logic and Automated Theorem Proving. Springer-Verlag, New York, 1996
[2] John Harrison, Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009
[3] Uwe Schöning, Logik für Informatiker, Spektrum, 2000
- zu B):
[4] TPTP Infrastruktur: http://www.tptp.org
[5] G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure. Journal of Automated Reasoning (2009) 43(4): 337-362 (Download)
[6] G. Sutcliffe and C. Benzmüller, Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of
Formalized Reasoning, (2010) 3(1):1-27
Course Resources
Thanks to Geoff Sutcliffe for his support!
C. Benzmüller, 2013