19313901 Vorlesung

WiSe 14/15: Expressive Logiken - Theorie, Mechanisierung, Anwendungen

Christoph Benzmüller

Hinweise für Studierende

Klausur am 20.10.14, 18-20 Uhr, SR031, Arnimallee 7



Voraussetzungen:

Empfohlen (aber nicht zwingend erforderlich) sind Grundlagenkenntnisse in der Theoretischen Informatik, der Funktionalen Programmierung, der Logik erster Stufe und der Künstlichen Intelligenz.



Zielgruppe:

Masterstudiengang Informatik (alte und neue STO). Studenten mit Interesse an Logik, Automatischem und Interaktivem Theorembeweisen und künstlicher Intelligenz



Homepage:

http://page.mi.fu-berlin.de/cbenzmueller/papers/2014-EL/

Schließen

Kommentar

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.

Schließen

9 Termine

Regelmäßige Termine der Lehrveranstaltung

Mo, 29.09.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Di, 30.09.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Mi, 01.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Do, 02.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Mo, 06.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Di, 07.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Mi, 08.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Do, 09.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Fr, 10.10.2014 09:00 - 13:00

Dozenten:
PD Dr. Christoph Benzmüller

Räume:
SR 031/A7 (Arnimallee 7)

Studienfächer A-Z