19324201

WiSe 16/17: Logik

Franz Kiràly

Information for students

Organisatorisches:

Erster Vorlesungstermin ist der 21.10.2016, erster Übungstermin der 28.10.2016. Während der Vorlesung werden 10-12 Übungsblätter bearbeitet.

Die Vorlesung wird durch einen elektronischen Online-Kurs unterstützt, der aufgrund technischer Beschränkungen der FU-seitigen e-Learning-Infrastruktur am University College London gehostet wird. Details hierzu und Zugangsdaten werden in der ersten Vorlesungswoche bekanntgegeben.

Comments

This lecture course combines

A) a compact introduction in the theory of first-order logic with
B) a hands-on tutorial on the development and eployment of first-order theorem proving systems.

Regarding A) the lecture focuses on the textbook of Fitting: First-Order Logic and Automated Theorem Proving, 1996. Harrison' Handbook of Practical Logic and Automated Reasoning, 2009, is also recommended. The topics of this part of the lecture include:

syntax and semantik of propositional logic and first-order logic (with and without equality);
Herbrand models;
Hintikka sets and abstract consistency;
soundness and completeness;
semantic tableaux and Resolution;
implementation

Regarding B) the lecture focuses on the TPTP infrastruktur (www.tptp.org). Addressed topics include:

TPTP Sprache(n)
SZS ontology of prover results
TPTP and TSTP libraries for problems and proofs
application and developement of TPTP compliant provers
further TPTP tools and systems
TPTP infrastructure for higher-order logic

Part B) of the lecture we will predominantly work practically. As far as time permits we will also address selected topics on the theory and practice of higher-order automated theorem proving. Students are advised to start reading the suggested literature before the lecture course starts.

16 Class schedule

Additional appointments

Fri, 2017-02-24 10:00 - 14:00

Prüfungen

Location:
T9/053 Seminarraum (Takustr. 9)

Regular appointments

Fri, 12:00 - 14:00 16 Class schedule

Fri, 2016-10-21 12:00 - 14:00