19619

WiSe 12/13: Logik erster Stufe in Theorie und Praxis

Christoph Benzmüller; Raul Rojas Gonzales

Additional information / Pre-requisites

1,2,4 Blockveranstaltung vor WS12/13 - Täglich von 9-18 Uhr in SR031, Arnimallee 5/7

Comments

Inhalt 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 an den Lehrbüchern von Fitting [1] und Harrison [2]. 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 2013 vertieft werden wird). Es wird den Teilnehmern empfohlen, sich bereits im Vorfeld in [1], [2] und [5] einzuarbeiten. Voraussetzungen Grundlagen der theoretischen Informatik 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 [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 close

9 Class schedule

Regular appointments

Mon, 09:00 - 18:00 9 Class schedule

Mon, 2012-10-01 09:00 - 18:00

Lecturers:
PD Dr. Christoph Benzmüller