Inhalt

In dieser Vorlesung werden wir uns mit dem Thema der formalen Wissenrepräsentation befassen. Insbesondere lernen wir Algorithmen kennen, die mit formalem Wissen umgehen können und durch automatisches Schlussfolgern auch implizit vorhandenes Wissen ableiten können. Dazu verwenden wir verschiedene logik-basierte Formalismen angefangen mit der Aussagenlogik über die Prädikatenlogik bis zu verschiedenen Fragmenten der Prädikatenlogik. Wir betrachten dabei die folgenden Punkte:

• Eigenschaften von Logiken (Finite Model Property, Kompaktheit, Baumeigenschaft, ...)
• Aufgaben des Automatischen Schlussfolgerns in der Wissenrepräsentation (Erfüllbarkeit, Klassifikation, Entailment, ...)
• Verfahren zum automatischen Schlussfolgern (Tableau, Hypertableau, Resolution, Consequence-Based Reasoning, Automaten)
• Beweisverfahren (Korrektheit und Terminierung der vorgestellten Algoritmen)
• Komplexität der Algorithmen

Veranstalter

Juniorprof. Dr. Birte Glimm

Termine

Vorlesung

Mittwoch: 16:00 — 17:30 in O27/3211
Donnerstag: 16:00 — 17:30 in O27/3211
Sprechstunde nach der VL oder nach Vereinbarung, nach Absprache können die VL auch 15 min früher beginnen

Klausur

Die Prüfung wird schriftlich durchgeführt. 

Übungen

Die Übungen finden im Rahmen der Vorlesung statt, ungefähr im 14-tägigem Rhythmus. Abgabe- und Besprechungstermine für Übungsblätter werden jeweils in der Vorlesung bekanntgegeben und stehen im Moodle e-Lerning System zur Verfügung.

Alle relevanten Vorlesungsunterlagen finden Sie in Moodle. Das benötigte Passwort wird in der Vorlesung bekanntgegeben oder kann per Email an die Dozentin erfragt werden. Handouts können über das Skriptdrucksystem der SGI ausgedruckt werden.

Bücher

Allgemeine Literatur zum Thema der Vorlesung:

• Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, Peter F. Patel-Schneider. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press. 2007. 2-te Auflage. ISBN 978-0521876254
• Uwe Schöning. Logik für Informatiker. 5. Auflage, Spektrum Akademischer Verlag, 2000 (ISBN 978-3827410054)
• Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer. ISBN 0-387-94593-8
• John Kelly. The Essence of Logic. Prentice Hall. ISBN 0-13-396375-6
• John Sowa. Knowledge Representation. Brooks/Cole 1999

Technisches

Typ:	Vorlesung im Master Studium (3V / 1Ü)
Leistungspunkte:	6
Zuordnung:	Theoretische und Mathematische Methoden der Informatik (Kernfach/Kernmodul) Theoretische Informatik (Vertiefungsfach/Vertiefungsmodul) Intelligente Systeme (Vertiefungsfach/Vertiefungsmodul)
Folgeveranstaltungen:	Intelligente Handlungsplanung Grundlagen des Semantic Web Multiagentensysteme