19619
Lecture
WiSe 13/14: V Logik erster Stufe in Theorie und Praxis
Christoph Benzmüller
Information for students
Übungen siehe 19619a
Comments
Diese Vorlesung kombiniert
Hinsichtlich A) orientiert sich die Vorlesung am Lehrbuch von Fitting [1] (Harrison [2] wird ebenfalls sehr empfohlen). Zu den Themen der Vorlesung zählen:
Hinsichtlich B) konzentriert sich die Vorlesung auf eine Einführung in die TPTP Infrastruktur [4]. Angesprochene Themen sind:
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 close
- 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 close
Suggested reading
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.
- [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.
16 Class schedule
Regular appointments
Fri, 2013-10-18 12:00 - 14:00
Fri, 2013-10-25 12:00 - 14:00
Fri, 2013-11-01 12:00 - 14:00
Fri, 2013-11-08 12:00 - 14:00
Fri, 2013-11-15 12:00 - 14:00
Fri, 2013-11-22 12:00 - 14:00
Fri, 2013-11-29 12:00 - 14:00
Fri, 2013-12-06 12:00 - 14:00
Fri, 2013-12-13 12:00 - 14:00
Fri, 2013-12-20 12:00 - 14:00
Fri, 2014-01-10 12:00 - 14:00
Fri, 2014-01-17 12:00 - 14:00
Fri, 2014-01-24 12:00 - 14:00
Fri, 2014-01-31 12:00 - 14:00
Fri, 2014-02-07 12:00 - 14:00
Fri, 2014-02-14 12:00 - 14:00