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

mindestens eine Woche intensives Studium der angegebenen Literatur (siehe unten)
Sprechstundenangebot in der Woche vom 22.-28.9.2014: Arnimallee 7, Raum 115 (Benzmüller) bzw. Raum 113 (Wisniewski, Steen)

Veranstaltung

Zeitraum: 29.9.2014 - 10.10.2014 (Blockveranstaltung)
Vorlesung täglich, 9:30 Uhr - 12:30 Uhr (inkl. Pausen)
Übungen täglich, ca. 14:30 Uhr - 17:30 Uhr (inkl. Pausen)
Ort: SR 031 (Arnimallee 5/7, Erdgeschoss, Seminarraum im Verbindungsflur)

Nachbereitungsphase

eine Woche Nachbereitung bzw. Klausvorbereitung vom 13.-17.10.2014

Klausur

in der Woche vom 20.-24.10.2014, genaueres wird noch bekannt gegeben

Synopsis

Themen der Vorlesung und der Übungen:

Einfach getypter Lambda-Kalkül: wichtigste theoretische Eigenschaften, Church Numerals
Einführung in die Logik höherer Stufe (HOL): Historie und Abgrenzung, Syntax, Semantik, Kalküle, Korrektheit, Vollständigkeit, Cut-Elimination, Cut-Simulation, Unifikation, Pre-Unifikation, Skolemisierung, Transformationen in Logik erster Stufe
Automatische Beweiser (und Modellgenerierer) für HOL: LEO-III, LEO-II, Satallax, Isabelle/HOL, Nitpick
Interaktive Beweiser für HOL: Isabelle/HOL
TPTP Sprache(n), SZS Ontologie für Beweiserresultate, TPTP und TSTP Problem- und Beweis-Bibliotheken, weitere TPTP Werkzeuge und Systeme
Quantifizierte Modallogiken, Konditionallogiken, Hybride Logiken, Temporallogiken, Mehrwertige Logiken
HOL als Universelle Logik mithilfe semantischer Einbettungen
Anwendungen: Ontologieschliessen, Gödel's Gottesbeweis, andere Anwendungen

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)

The Lambda Calculus (Jesse Alama), Stanford Encyclopedia of Philosophy, 2013.
Lambda Calculi with Types (Henk Barendregt), 1993.
Henk: a typed intermediate language (Simon Peyton Jones, Erik Meijer), 1997.
Automation of Higher-Order Logic (Christoph Benzmüller, Dale Miller), Chapter in Handbook of the History of Logic, Volume 9 --- Logic and Computation (Jörg Siekmann, Dov Gabbay, John Woods, eds.), Elsevier, 2014 (to appear).
The Seven Virtues of Simple Type Theory (William M. Farmer), Journal of Applied Logic, 6:267-286.
Church's Type Theory (Peter Andrews), The Stanford Encyclopedia of Philosophy (Spring 2014 Edition), Edward N. Zalta (ed.)
Higher-Order Semantics and Extensionality, (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Journal of Symbolic Logic, 69(4):1027-1088, 2004.
Cut-Simulation and Impredicativity, (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Logical Methods in Computer Science, volume 5, number 1:6, pp. 1-21, 2009.
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure, (Christoph Benzmüller, Geoff Sutcliffe), Journal of Formalized Reasoning, volume 3, number 1, pp. 1-27, 2010.
Higher-Order Automated Theorem Provers, (Christoph Benzmüller), 2014 (to appear).
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In 21st European Conference on Artificial Intelligence (ECAI), 2014.

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