MiG

Logik erster Stufe: Theorie und Praxis

(19324201/19324202)

Typ

VL/Ü

Dozent/in

C. Benzmüller

Zeit

Vorlesung:  Freitags, 12-14 Uhr, SR031 der Arnimallee 7

Übung: Freitags 8-10 Uhr, SR049 der Takustr. 9

Beginn

21.10.2016 — 17.02.2017

Links auf Kursbeschreibung

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: First-Order Logic and Automated Theorem Proving, 1996. Harrison's Handbook of Practical Logic and Automated Reasoning, 2009, 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
  • Grenzen der Logik erster Stufe

Hinsichtlich B) konzentriert sich die Vorlesung auf eine Einführung in die TPTP Infrastruktur (www.tptp.org). Angesprochene Themen sind:

 

  • TPTP Sprache(n),SZS Ontologie für Beweiserresultate;
  • TPTP und TSTP Problem-und Beweis-Bibliotheken;
  • Anwendung und Entwicklung von TPTP kompatiblen Beweisern;
  • weitere TPTP Werkzeuge und Systeme
  • TPTP Infrastruktur 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. Es wird den Teilnehmern empfohlen, sich bereits im Vorfeld in die Literatur einzuarbeiten.