WS 2014/2015: Expressive Logiken -- Theorie, Mechanisierung, Anwendungen

Vorlesung und Übung (Blockkurs) -- 2+2-stündig, ECTS: 5
Dozent (Vorlesung): Christoph Benzmüller
Dozenten (Übungen): Alexander Steen, Max Wisniewski
Zielgruppe:
Masterstudiengang Informatik (alte und neue STO)
Studenten mit Interesse an Logik, Automatischem und Interaktivem Theorembeweisen und Künstlicher Intelligenz
Modul: Künstliche Intelligenz
Voraussetzungen: empfohlen (aber nicht zwingend erforderlich) sind Grundlagenkenntnisse in der Theoretischen Informatik, der Funktionalen Programmierung, der Logik erster Stufe, und der KI
Mailinglist: ExpressiveLogiken@lists.fu-berlin.de, Registrierung über diese Seite
Wiki: wird noch bekanntgegeben

Organisatorisches

Vorbereitungsphase

Veranstaltung

Nachbereitungsphase

Klausur

Synopsis

Themen der Vorlesung und der Übungen:
Die Vorlesung wird sich auf die theoretischen Aspekte konzentrieren. In den Übungen werden sowohl theoretische als auch praktische Aufgaben bearbeitet. Eine Auswahl der erwähnten Systeme werden in der Praxis angewendet werden. Zur erfolgreichen Teilnahme ist eine intensive Einarbeitung in die Literatur, sowie Nachbereitung der Vorlesung unbedingt erforderlich.

Folien

Folien zur Vorlesung gibt es hier. TPTP THF0 Beispiele gibt es hier.

Termine

Erste Woche

Montag (29.9)
Thematische Einführung, Formalitäten
Lambda-Kalkül (ungetypt, einfach getypt, verschiedene Erweiterungen), evtl. auch de-Bruijn-Indizes, Typrekonstruktion
Einführung HOL (Syntax), Expressivität
Dienstag (30.9)
Überblick zur Semantik von HOL, abstrakte Konsistenz
ND-Kalküle, Korrektheit und Vollständigkeit
Mittwoch (1.10)
Fortsetzung Semantik / abstrakte Konsistenz / ND-Kalküle
Vollständigkeit
Donnerstag (2.10)
Einführung TPTP (Bibliothek, Eingabesprachen, Ausgabe)
Übersicht Beweiser (Automatische Theorembeweiser, Interaktive Theorembeweiser)
Formulierung von Problemen in THF, Benutzung von ATPs
Freitag (3.10)
entfällt

Zweite Woche

Montag (4.10)
Resolution (LEO-II), (Prä-)Unifikation
Dienstag (5.10)
ggf. Fortsetzung Resolution/Unifikation
Einfürung Modallogik (QML) (Syntax, Kripke-Semantik, Korrenpondenzresultate)
Mittwoch (6.10)
Einbettungsansatz (Einbettung von QML in HOL), Variationen (constant vs. varying domain, etc.)
Anwendung am Beispiel von Gödels Gottesbeweis
Weitere Einbettungen (z.B. Konditionallogik, Temporallogik, Hybride Logiken)
Donnerstag (7.10)
Praktische (technische) Aspekte von HOL-Beweisern (Termdarstellungen, Architekturen, ...)
ggf. Übersetzung nach FOL
Leo-III Projekt
Freitag (8.10)
Gastvortrag von Chad Brown (Instanzierungsbasierter Kalkül für HOL, Satallax)
Rekapitulation, Fragestunde, Übungsklausur

Literaturempfehlung zur Vorlesung (siehe auch weitere Literaturangaben in diesen Werken)


C. Benzmüller, A. Steen, M. Wisniewski, 2014