19619

WiSe 13/14: V Logik erster Stufe in Theorie und Praxis

Christoph Benzmüller

Hinweise für Studierende

Übungen siehe 19619a

Kommentar

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] wird ebenfalls sehr empfohlen). Zu den Themen der Vorlesung zählen:

Syntax und Semantik von Aussagenlogik und Logik erster Stufe (mit und ohne Gleichheit),
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 2014 vertieft werden wird).
Es wird den Teilnehmern empfohlen, sich bereits im Vorfeld in [1] und [5] einzuarbeiten (auch [2] wird sehr empfohlen).

Weitere Angaben siehe (provisorische) Webseite Schließen

Literaturhinweise

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 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. (http://www.springerlink.com/content/2g263588337ku424/fulltext.pdf
[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.

Schließen