19324201 Lecture

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.

close

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.

close

Suggested reading

Literatur:

Für die theoretischen Teile orientiert sich die Vorlesung an

Ebbinghaus (2007) – Einführung in die mathematische Logik

Schöning (2000) – Logik für Informatiker

close

16 Class schedule

Additional appointments

Fri, 2017-02-24 10:00 - 14:00
Prüfungen

Location:
T9/053 Seminarraum (Takustr. 9)

Regular appointments

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

Location:
A7/SR 031 (Arnimallee 7)

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

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-11-04 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-11-11 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-11-18 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-11-25 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-12-02 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-12-09 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2016-12-16 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-01-06 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-01-13 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-01-20 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-01-27 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-02-03 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

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

Location:
A7/SR 031 (Arnimallee 7)

Fri, 2017-02-17 12:00 - 14:00

Location:
A7/SR 031 (Arnimallee 7)

Subjects A - Z