Project Group

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Prof. Dr.-Ing. Franz Baader

Die Project Group ist ein Angebot für Studierende im Studiengang Master Computational Logic (Modul MCL-P).

Organisation

Die Einführungsveranstaltung findet am 24. April um 15:15 im Raum APB/3027 statt. Falls Ihnen eine Teilnahme nicht möglich ist, nehmen Sie bitte bis zum 23. April Kontakt mit Francesco Kriegel auf.
Die Teilnehmer sollten die relevante Literatur lesen und diese mit ihrem Tutor diskutieren, um mit dem gewählten Thema vertraut zu werden. Die nötige Implementierungsarbeit (falls vorhanden) sollte in einer strukturierten Weise ausgeführt werden, und muss ordentlich dokumentiert werden. Falls ein Thema von zwei oder mehr Studenten bearbeitet wird, dann ist das Aneignen von Fähigkeiten zur Gruppenarbeit ein weiteres Ziel des Praktikums. Die Ergebnisse des Projekts müssen in einem Praktikumsbericht (~15 Seiten) beschrieben und in einem Vortrag (~30 Minuten) am Semesterende präsentiert werden.
Weiterhin sind die Teilnehmer verpflichtet, genügend Zeit für die Durchführung des Praktikums zu reservieren. Die unbedingte Frist zur Beendigung des Praktikums ist das Ende des Semesters (Prüfungszeitraum), d.h. die Bearbeitungszeit für das Praktikums beträgt ein Semester inklusive der vorlesungsfreien Zeit. Wenn das Praktikum nicht rechtzeitig abgeschlossen werden kann, dann können keine Credits vergeben werden. Es obliegt dem teilnehmenden Studenten, das Praktikum rechtzeitig zu beginnen und Termine mit dem Tutor für regelmäßige Besprechungen während des Semesters zu vereinbaren.
Es ist hilfreich, wenn Sie die Lehrveranstaltungen Formale Systeme, Theoretische Informatik und Logik und Description Logics absolviert haben.

Themen

(1) Endliche Herbrand-Modelle für Hornklauseln

Man kann die Existenz eines endlichen Herbrand-Modells für bestimmte Mengen von prädikatenlogischen Anti-Hornklauseln in exponentieller Zeit entscheiden. Dieses Entscheidungsproblem ist außerdem ExpTime-hart. Das Ziel dieses Praktikums ist es, die Komplexität des analogen Problems für Mengen von Hornklauseln zu bestimmen. Dazu soll ein Algorithmus entwickelt und/oder untere Schranken mittels eines Härtebeweises gefunden werden.

Es werden grundlegende Kenntnisse über Prädikatenlogik sowie Komplexitätstheorie vorausgesetzt.

Literatur
[1] Report: http://lat.inf.tu-dresden.de/research/papers/2012/BoMo-LPAR-12.pdf

Tutor: Stefan Borgwardt

(2) Endliche Herbrand-Modelle für Anti-Hornklauseln

Das Ziel dieses Praktikums ist es, einen Algorithmus zu implementieren, der die Existenz endlicher Herbrand-Modelle für bestimmte Mengen von prädikatenlogischen Anti-Hornklauseln entscheidet. Das Programm soll an vielfältigen Eingabeproblemen getestet werden. Die Programmiersprache kann frei gewählt werden.

Es werden grundlegende Kenntnisse über Prädikatenlogik sowie gute Programmierfähigkeiten vorausgesetzt.

Literatur
[1] Report: http://lat.inf.tu-dresden.de/research/papers/2012/BoMo-LPAR-12.pdf

Tutor: Stefan Borgwardt

(3) Most Specific Generalizations w.r.t. General TBoxes in ELgfp

Dieses Thema zielt auf die Implementierung und Evaluierung von Methoden zur Berechnung des kleinsten gemeinsamen Oberbegriff (least common subsumer) und speziellster Begriff (most specific concept) in der leicht-gewichtigen Beschreibungslogik ELgfp, d.h. EL interpretiert mit größter Fixpunkt Semantik. Im Unterschied zu Standard-EL mit deskriptiver Semantik existieren diese speziellsten Verallgemeinerungen stets in ELgfp und können in polynomieller Zeit berechnet werden. Weiterhin sollte der Student einen Vergleich mit speziellsten Generalisierungen bezüglich deskriptiver Semantik und mit Rollentiefe-beschränkten speziellsten Generalisierungen bezüglich deskriptiver Semantik machen.

Grundlegende Kenntnisse von Beschreibungslogiken und gute Programmierfähigkeiten werden erwartet. Für eine einfachere Verwendung und Integration mit existierenden Programmen (z.B. Elk, Protégé usw.) sollte das Programm auf der OWL API aufbauen.

Literatur
[1] Franz Baader: Least Common Subsumers and Most Specific Concepts in a Description Logic with Existential Restrictions and Terminological Cycles
[2] OWL API

Tutor: Francesco Kriegel

(4) Formale Begriffsanalyse & Aussagenlogik: Von Pseudo-Inhalten zu Implikations-Basen

Ziel dieses Themas ist die Formulierung einer minimalen Theorie von Implikationen, die in einer gegebenen Menge von aussagenlogischen Modellen gelten, und aus der alle anderen Implikationen folgen, die in der gegebenen Modellmenge gelten. Hierfür ist ein Isomorphismus zwischen aussagenlogischen Modellmengen und formalen Kontexten nötig, um bestehende Ergebnisse aus der formalen Begriffsanalyse zu verwenden. Weiterhin sollte der Student einen Algorithmus zur Berechnung der Implikations-Basis angeben. Die Resultate können auf aussagenlogische Basen erweitert werden.

Grundlegende Kenntnisse in Aussagenlogik und Mengenlehre werden erwartet. Weitere Kenntnisse in Logik oder Ordnungstheorie können hilfreich sein.

Literatur
[1] Bernhard Ganter und Rudolf Wille: Formale Begriffsanalyse - Mathematische Grundlagen, Springer Verlag, Heidelberg 1996
[2] Bernhard Ganter: Attribute Exploration with Background Knowledge

Tutor: Francesco Kriegel

(5) Unifikation in Beschreibungslogiken

Das System UEL kann benutzt werden, um Redundanzen in Ontologien zu finden, indem Konzepte der Beschreibungslogik EL unifiziert werden. Es soll um einen neu entwickelten regelbasierten Algorithmus erweitert werden, der es erlaubt, negative Nebenbedingungen bei der Unifikation zu berücksichtigen.

Es werden grundlegende Kenntnisse von Beschreibungslogiken sowie gute Programmierfähigkeiten vorausgesetzt.

Literatur
[1] UEL: http://uel.sourceforge.net/
[2] Report: http://lat.inf.tu-dresden.de/research/reports/2015/BaBM-LTCS-15-03.pdf

Tutor: Stefan Borgwardt

(6) Erweiterung eines Systems für die Berechnung von Logischen Unterschieden

Das Ziel dieses Projektes ist die Erweiterung eines neues System zur Erkennung von logischen Unterschieden zwischen Ontologien basierend auf einer Hypergraph-Darstellung von Ontologien [2]. Die Erweiterung des Systems besteht darin, dass nicht nur Unterschiede bezüglich Subsumptionsanfragen zwischen Konzepten erkannt werden sollen, sondern auch bezüglich Instanz- und konjunktiver Anfragen. Zusätzlich sollen Ontologien, welche in der Beschreibungslogik EL erweitert mit Rolleninklusionen, und Einschränkungen auf den Definition-/Wertebereich von Rollen formuliert sind, vom System verarbeitet werden können. Eine Beschreibung der erweiterten Algorithmen ist verfügbar in [1].

Es werden grundlegende Kenntnisse von Beschreibungslogiken sowie gute Programmierfähigkeiten, inbesondere in Java, vorausgesetzt.

Literatur
[1] http://dx.doi.org/10.3233/978-1-61499-419-0-555
[2] http://lat.inf.tu-dresden.de/research/papers/2013/EcLuWa-DChanges2013.pdf

Tutor: Michel Ludwig

Weitere Themen werden noch hinzugefügt.