Komplexpraktikum Theoretische Informatik
Beschreibung
Im Master-Praktikum (Modul INF-MA-PR) sowie im Profilprojekt (Modul INF-PM-FPG) wird eine wissenschaftliche Aufgabenstellung unter Anleitung eines Mitarbeiters des Lehrstuhls für Automatentheorie bearbeitet. Das Ziel ist es, mit den Grundlagen des wissenschaftlichen Arbeitens vertraut zu werden. Dazu gehören, je nach Thema, die Literaturrecherche, Erarbeitung eigenständiger Forschungsergebnisse, sowie Implementierungsarbeiten. Falls das Thema eine Implementierung beinhaltet, soll diese gut strukturiert und dokumentiert werden. Zum erfolgreichen Abschluss des Praktikums gehört eine schriftliche Dokumentation (ca. 15 Seiten) sowie eine mündliche Präsentation (30 Minuten) vor Mitarbeitern des Lehrstuhls.
SWS/Module
Das Praktikum wird für folgende Module angeboten:
- INF-PM-FPG (Profilprojekt Grundlagenforschung) in den Studiengängen Master Informatik und Diplom Informatik
Im Rahmen dieses Moduls umfasst das Praktikum -/-/8 SWS.
Koordination: Prof. Franz Baader - INF-MA-PR (Forschung und Entwicklung in der Informatik) im Studiengang Master Informatik
In diesem Fall kann die Bearbeitung des Praktikums im Umfang von -/-/4 SWS oder -/-/8 SWS erfolgen. Es muss im Vorfeld mit dem Betreuer abgesprochen werden, welche Option gewählt wird.
Koordination: Dr. Stefan Borgwardt
Themen
Die folgenden Themen werden am 18.04.2018 um 11:10 im Raum APB/3027 genauer vorgestellt (auf Englisch).
It is well-known that regular languages are recognised by finite automata and are closed under union, intersection, complement, and also language operations, such as concatenation and quotient. However, some operations, like complement or intersection of linearly many automata, require exponentially larger automata.
Tree-like automata were considered in [1] in order to represent languages of the form \(K\cup L \Sigma^*\) for finite languages \(K,L\) and they demonstrate better closure properties. The aim of this project is to develop the theory of tree-like automata: after formally introduce them, prove their closure properties (or, rather, of the languages they accept) providing suitable constructions, and compute the complexity of such constructions. Furthermore, the study can consider extensions and limitations of tree-like automata.
This project requires basic knowledge of automata theory.
Literature:
- F Baader, R Küsters, A Borgida, DL McGuinness; Matching in description logics, Journal of Logic and Computation, Volume 9, Issue 3, 1 June 1999, Pages 411–447, https://doi.org/10.1093/logcom/9.3.411
Tutor: Pavlos Marantidis
Für ausdrucksschwache Beschreibungslogiken wie die Logik \(\mathcal{EL}\), in der häufig medizinische Ontologien beschrieben werden, berechnen die Subsumtionsalgorithmen zusätzlich ein sogenanntes kanonisches Modell, in dem genau die Subsumtionsbeziehungen gelten, die aus der Ontologie folgen. Ein solches Modell kann als Graph, bei dem sowohl die Knoten als auch die Kanten mit Markierungen versehen sind, dargestellt werden. Ziel ist es, Eigenschaften dieses Modells zu visualisieren. Dazu muss 1) die interne Darstellung des kanonischen Modells aus \(\mathcal{EL}\)-Systemen (wie z.B. ELK https://www.cs.ox.ac.uk/isg/tools/ELK/) in eine für die Visualisierung geeignete Form transformiert werden; 2) das kanonische Modell geeignet angezeigt werden; 3) Unterstützung zur Visualisierung von Eigenschaften des Modells (z.B. färbe alle Elemente, die zum Konzept \(C\) gehören) bereitgestellt werden.
Dieses Projekt wird von der Professur für Multimedia-Technologie mitbetreut.
Tutor: Stefan Borgwardt
Für Ontologien ist die Berechnung der Subsumtionshierarchie, d.h. die Unterkonzept-Oberkonzept-Beziehungen zwischen den in der Ontologie definierten Konzepten, eine wichtige Basisoperation. Ziel ist es, geeignete Visualisierungsansätze für diese Hierarchie zu entwickeln. Dazu muss 1) die interne Repräsentation der Hierarchie (http://owlcs.github.io/owlapi/) in eine für die Visualisierung geeignete Form transformiert werden; 2) der Hierarchiegraph geeignet angezeigt werden, auch bei sehr großen Ontologien mit 300.000 Konzepten; 3) Unterstützung zum Zoomen auf Konzepte und ihre direkte Umgebung sowie Markierung aller Unter- oder Oberkonzepte bereitgestellt werden.
Dieses Projekt wird von der Professur für Multimedia-Technologie mitbetreut.
Tutor: Stefan Borgwardt
Um Anfragen zu beantworten, ist es oft nötig, auf mehrere verschiedenartige Datenquellen zurückzugreifen, z.B. Datenbanken oder Sammlungen von RDF-Tripeln. Ontologien ermöglichen es, diese Quellen mittels eines gemeinsamen Vokabulars zu verknüpfen. Das Ziel des Praktikums ist es, einen existierenden Algorithmus zur Anfragebeantwortung über Datalog+/- Ontologien [1] für sogenannte multi-lineare Datalog+/- Regeln anzupassen. Es soll die Korrektheit des Algorithmus bewiesen werden, und bekannte Optimierungen für diesen Algorithmus untersucht werden.
Das Praktikum erfordert grundlegendes Wissen über Prädikatenlogik und Beweistechniken.
Literatur:
- Georg Gottlob, Giorgio Orsi, and Andreas Pieris. Query rewriting and optimization for ontological databases. ACM Transactions on Database Systems, 39(3), pp. 25:1–25:46, 2014.
Tutor: Stefan Borgwardt
Ontologien werden in vielen Bereichen benutzt, um Fachterminologien zu formalisieren, zum Beispiel in der Medizin, der Biologie, im Semantic Web, und anderen Gebieten. Moderne Ontologien umfassen oft ein grosses Vokabular. So definiert z.B. die Ontologie SNOMED CT, welche in vielen Ländern im Gesundheitssektor eingesetzt wird, über 300.000 Konzepte.
Die Entwicklung, Wartung und Benutzung solcher Ontologien wird durch ihre Komplexität erschwert, vor allem da Ontologien eine Menge implizites Wissen beinhalten. Eine Methode, die hierbei helfen kann, ist die uniforme Interpolation [2]. Ausgehend von einer vom Benutzer spezifizierten Menge von Konzepten und Relationen, berechnet sie eine fokussierte Sicht auf die Ontologie, den uniformen Interpolanten, welcher alle Informationen widerspiegelt, die mit diesen Konzepten und Relationen ausgedrückt werden können. Dies erlaubt es zum Beispiel, versteckte Beziehungen zwischen ausgewählten Konzepten aufzudecken, was dabei helfen kann, Ontologie-Inhalte besser zu verstehen und Modellierungsfehler zu entdecken.
Obwohl Algorithmen für uniforme Interpolation bereits implementiert wurden, sind diese bisher noch nicht in gängige Ontologie-Editoren eingebunden. Das Ziel des Praktikums ist es, ein Plugin für den populären Ontologie-Editor Protégé zu entwickeln, welches die Bibliothek LETHE [1] benutzt, um uniforme Interpolanten zu berechnen. Das Plugin soll es dem Benutzer erlauben, Konzepte und Relationen auszuwählen, um anschließend den uniformen Interpolanten zu berechnen und in benutzerfreundlicher Weise anzuzeigen.
Das Praktikum setzt Java-Kenntnisse voraus, sowie grundlegendes Wissen über Beschreibungslogiken.
Literatur:
- Patrick Koopmann, Renate A. Schmidt. LETHE: Saturation-based reasoning for non-standard reasoning tasks. In Proceedings of the 4th OWL Reasoner Evaluation Workshop (ORE), volume 1387 of CEUR Workshop Proceedings, pp. 23–30, 2015.
- Patrick Koopmann, Renate A. Schmidt: Forgetting concept and role symbols in \(\mathcal{ALCH}\)-ontolgoies. In Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 8312 of Lecture Notes in Computer Science, pp. 552–567, 2013. Springer-Verlag.
Tutor: Patrick Koopmann
Die Beschreibungslogik \(\mathcal{EL}\) ist die Grundlage großer biomedizinischer Ontologien, wie zum Beispiel von SNOMED CT oder der Gene Ontology. Unterschiedliche Schlussfolgerungsmethoden helfen dabei, solche Ontologien zu erstellen, zu reparieren, und aktuell zu halten. Zum Beispiel kann die Differenz zwischen zwei Begriffen benutzt werden, um die Konzepthierarchie der Ontologie zu erklären ("Warum ist A ein Unterkonzept von B?") oder Benutzeranfragen zu verfeinern ("Unter welchen Bedingungen sind die Instanzen von B auch Instanzen von A?"). Leider können existierende Definition von Konzept-Differenz [1] nicht angemessen mit der Struktur von \(\mathcal{EL}\)-Konzepten umgehen.
Das Ziel des Praktikums ist es, eine neue Definition für die Differenz von \(\mathcal{EL}\)-Konzepten auf ihre Eigenschaften, wie Existenz, Eindeutigkeit, und Komplexität, hin zu untersuchen.
Das Praktikum erfordert grundlegendes Wissen über logikbasierte Wissensrepräsentation.
Literatur:
- Gunnar Teege. Making the difference: A subtraction operation for description logics. In Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 540–550, 1994.
Tutor: Oliver Fernández Gil (auf Englisch)
Die einfache Beschreibungslogik \(\mathcal{EL}\) wird inzwischen oft für Aufgaben der Wissensrepräsentation und -ableitung verwendet, hauptsächlich wegen ihrer praktisch schnell lösbaren Inferenzprobleme und ihrer guten Lesbarkeit. Zum Beispiel besitzt die Web Ontology Language (OWL) ein Profil "EL", das auf \(\mathcal{EL}\) basiert. In dieser Logik haben die gebräuchlichen Inferenzprobleme weiterhin eine polynomielle Zeitkomplexität, wie zum Beispiel das Problem der Subsumption zwischen zwei Konzeptbeschreibungen bezüglich einer TBox.
In der Vergangenheit wurden einige speziellere Inferenzprobleme in \(\mathcal{EL}\) definiert und ihre Komplexitäten wurden untersucht. Das Ziel dieses Projekts ist es, das neue Inferenzproblem der Nachbarschaft zwischen \(\mathcal{EL}\)-Konzeptbeschreibungen zu betrachten. Insbesondere nennen wir eine \(\mathcal{EL}\)-Konzeptbeschreibung \(C\) einen unteren Nachbarn einer \(\mathcal{EL}\)-Konzeptbeschreibung \(D\) bezüglich einer \(\mathcal{EL}\)-TBox \(\mathcal{T}\) falls \(C\) von \(D\) bzgl. \(\mathcal{T}\) strikt subsumiert wird und es außerdem "keine \(\mathcal{EL}\)-Konzeptbeschreibung dazwischen" gibt, also falls jede \(\mathcal{EL}\)-Konzeptbeschreibung \(E\) mit \(\mathcal{T}\models C\sqsubseteq E\sqsubseteq D\) entweder äquivalent zu \(C\) oder äquivalent zu \(D\) ist. Die Betrachtung dieses Themas kann in verschiedenen Richtungen geschehen:
- \(\mathcal{T}\) kann leer sein.
- Bestimmung der Komplexität des Nachbarschaftsproblems.
- Entwurf und Implementierung eines effizienten Algorithmus, der das Nachbarschaftsproblem entscheidet.
- Entwurf und Implementierung eines effizienten Algorithmus, der alle oberen/unteren Nachbarn einer Konzeptbeschreibung berechnet.
- Ausdrucksstärkere Beschreibungslogiken, z.B. \(\mathcal{ALC}\), oder \(\mathcal{EL}\) mit größter Fixpunkt Semantik.
-
etc.
Das Praktikum setzt grundlegendes Wissen über Beschreibungslogiken voraus.
Literatur:
- Franz Baader, Ian Horrocks, Carsten Lutz, Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017.
- Francesco M. Donini, Simona Colucci, Tommaso Di Noia, Eugenio Di Sciascio: A Tableaux-Based Method for Computing Least Common Subsumers for Expressive Description Logics. In Proceedings of the 21st International Joint Conferences on Artificial Intelligence (IJCAI), pp. 739-745, 2009.
Tutor: Francesco Kriegel
Die formale Begriffsanalyse (FBA) entstand aus dem Versuch, die philosophische Vorstellung eines „Begriffs“ zu formalisieren. Insbesondere hat die FBA eine starke Verbindung zur Aussagenlogik, und bietet verschiedene Methoden für den Umgang mit Wissen in Form von Regeln bzw. Implikationen. Ein prominentes Beispiel ist die kanonische Basis eines gegebenen formalen Kontexts \(\mathbb{K}\), die eine kleinstmögliche Menge von Implikationen darstellt, die einerseits in \(\mathbb{K}\) gültig ist, und aus der sich alle in \(\mathbb{K}\) gültigen Implikationen ableiten lassen. Für die Ableitungsrelation zwischen Implikationsmengen gibt es sowohl semantische als auch syntaktische Charakterisierungen.
Vor Kurzem wurde in [2] eine probabilistische Erweiterung der FBA untersucht, und eine Methode zur Axiomatisierung von Implikationen über probabilistischen Merkmalen wurde entwickelt. Die Ableitungsrelation zwischen Mengen von probabilistischen Implikationen ist dort jedoch nur semantisch beschrieben, und bisher existiert keine korrekte und vollständige syntaktische Beschreibung der Ableitungsrelation. Das Ziel dieses Praktikums ist es, eine solche syntaktische Charakterisierung zu finden, und ggf. eine Implementierung zur Verfügung zu stellen. Weil die in [2] verwendete Logik in die Logik aus [1] eingebettet werden kann, kann es hilfreich sein, für diese Aufgabe [1] zu lesen.
Literatur:
- Ronald Fagin, Joseph Y. Halpern, Nimrod Megiddo. A logic for reasoning about probabilities. Information and Computation 87(1/2), pp. 78–128, 1990.
- Francesco Kriegel. Implications over probabilistic attributes. In Proceedings of the 14th International Conference on Formal Concept Analysis (ICFCA), pp. 168–183, 2017.
Tutor: Francesco Kriegel
Die einfache Beschreibungslogik \(\mathcal{EL}\) wird inzwischen oft für Aufgaben der Wissensrepräsentation und -ableitung verwendet, hauptsächlich wegen ihrer praktisch schnell lösbaren Inferenzprobleme und ihrer guten Lesbarkeit. Zum Beispiel besitzt die Web Ontology Language (OWL) ein Profil "EL", das auf \(\mathcal{EL}\) basiert. In dieser Logik haben die gebräuchlichen Inferenzprobleme weiterhin eine polynomielle Zeitkomplexität, wie zum Beispiel das Problem der Subsumption zwischen zwei Konzeptbeschreibungen bezüglich einer TBox.
Wissensbasen können nicht nur von Hand aufgebaut werden, sondern es gibt hierfür auch automatische Konstruktionsverfahren. Insbesondere wurde in [1] gezeigt, wie die Theorie der in einer Interpretation gültigen Konzeptinklusionen automatisch axiomatisiert werden kann — und zwar korrekt und vollständig. Leider kann dieser Ansatz kein bereits vorhandenes Wissen in Form einer TBox berücksichtigen. Später lieferte [2] eine entsprechende Erweiterung des Axiomatisierungsverfahrens, welches sowohl eine Interpretation als auch eine TBox als Eingabe erlaubt. Diese Prozedur verwendet exzessiv sogenannte modellbasierte speziellste Konzeptbeschreibungen relativ zu einer TBox. Bisher wurde jedoch noch nicht untersucht, wie man deren Existenz überprüfen kann, bzw. wie man diese effizient berechnen kann; beide Fragen sollen in diesem Projekt angegangen werden. Ideen aus [3] können helfen, diese Fragen zu beantworten.
Das Praktikum setzt grundlegendes Wissen über Beschreibungslogiken voraus.
Literatur:
- Pages 60–68 in: Felix Distel. Learning description logic knowledge bases from data using methods from formal concept analysis. PhD thesis, Technische Universität Dresden, 2011.
- Francesco Kriegel. Incremental learning of TBoxes from interpretation sequences with methods of Formal Concept Analysis. In Proceedings of the 28th International Workshop on Description Logics (DL), pp. 452–464, 2015.
- Benjamin Zarrieß, Anni-Yasmin Turhan. Most specific generalizations w.r.t. general \(\mathcal{EL}\)-TBoxes. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI), pp. 1191–1197, 2013.
Tutor: Francesco Kriegel
Die formale Begriffsanalyse (FBA) entstand aus dem Versuch, die philosophische Vorstellung eines „Begriffs“ zu formalisieren. Insbesondere hat die FBA eine starke Verbindung zur Aussagenlogik, und bietet verschiedene Methoden für den Umgang mit Wissen in Form von Regeln bzw. Implikationen. Ein prominentes Beispiel ist die kanonische Basis eines gegebenen formalen Kontexts \(\mathbb{K}\), die eine kleinstmögliche Menge von Implikationen darstellt, die einerseits in \(\mathbb{K}\) gültig ist, und aus der sich alle in \(\mathbb{K}\) gültigen Implikationen ableiten lassen. Falls der die betrachtete Domäne beschreibende Kontext nicht vollständig ist, aber Experten in dieser Domäne verfügbar sind, dann kann ein Verfahren namens „Merkmalsexploration“ [1] genutzt werden, um in Interaktion mit den Experten eine minimale Menge von Implikationen zu finden, die die betrachtete Domäne korrekt und vollständig beschreibt.
Ein Nachteil der existierenden Varianten der Merkmalsexploration ist jedoch, dass stets nur eine Frage an die Experten gestellt werden kann, woraufhin die Antwort abgewartet werden muss, bevor der Algorithmus fortfahren kann; für große Domänen ist dieses Verfahren also bisher nicht praktikabel. Kürzlich wurde in [2] eine Abwandlung eingeführt, die eine parallele Interaktion mit den Experten erlaubt. Das Ziel dieses Praktikums ist der Entwurf und die Implementierung einer Plattform für eine kollaborative Wissenserschließung, die die parallele Merkmalsexploration als Kernkomponente benutzt. Die Implementierung soll eine Client-Server-Architektur verwenden, und ein geeigneter Anwendungsfall soll gesucht und umgesetzt werden.
Literatur:
- Bernhard Ganter. Two basic algorithms in concept analysis. In Proceedings of the 8th International Conference on Formal Concept Analysis (ICFCA), pp. 312–340, 2010.
- Francesco Kriegel. Parallel attribute exploration. In Proceedings of the 22nd International Conference on Conceptual Structures (ICCS), pp. 91–106, 2016.
Tutor: Francesco Kriegel
In Beschreibungslogiken reicht die klassische monotone Semantik oft nicht aus, um bestimmte Aspekte des menschlichen Denkens zu modellieren, wie z.B. die Änderung der eigenen Meinung im Angesicht neuer Information. Ein neuer Ansatz, Beschreibungslogiken mit nichtmonotoner Semantik zu versehen, sind die sogenannten „Typicality Models“ [1]. Diese erweitern die klassischen kanonischen Modelle der Beschreibungslogik \(\mathcal{EL}_{\bot}\). Das Ziel dieses Praktikums ist es, den normalen Klassifikationsalgorithmus zur Konstruktion kanonischer Modelle in \(\mathcal{EL}_{\bot}\) [2] so anzupassen, dass er minimale und maximale Typicality Models für nichtmonotone Wissensbasen konstruieren kann.
Das Praktikum setzt grundlegendes Wissen über Beschreibungslogiken voraus.
Literatur:
- Maximilian Pensel, Anni-Yasmin Turhan. Including quantification in defeasible reasoning for the description logic \(\mathcal{EL}_{\bot}\). In Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 78–84, 2017.
- Franz Baader, Sebastian Brandt, Carsten Lutz. Pushing the \(\mathcal{EL}\) envelope. In Proceedings of the 19th International Joint Conferences on Artificial Intelligence (IJCAI), pp. 364–369, 2005.
Tutor: Maximilian Pensel
In Fällen wo Wissensbasen aus verrauschten Daten generiert werden, können Wissensbasen leicht inkonsistent werden. In solchen Fällen werden Schussfolgerungen unter inkonsistenz-toleranter Semantik gezogen. Wenn die Daten in der Wissenbasis zu verschiedenen Zeitpunkten eingelesen werden, ist es üblich die Daten mit einem Zeitstempel zu versehen und so temporale Wissenbasen zu generieren.
In diesem Projekt sollen temporale Instanzanfragen (Anfragen nach den Instanzen eines Konzeptes) in Hinblick auf verschiedene inkonsistenz-tolerante Semantiken untersucht und Algorithmen zur Beantwortung von temporalen Instanzanfragen angegeben (und ggf. auch implementiert) werden.
Das Praktikum setzt grundlegendes Wissen über Beschreibungslogiken voraus.
Literatur:
- Rafael Penaloza. Inconsistency-Tolerant Instance Checking in Tractable Description Logics. International Joint Conference on Rules and Reasoning, 2017.
- Camille Bourgaux and Anni-Yasmin Turhan: Temporal Query Answering in DL-Lite over Inconsistent Data. In Proceedings of the 16th International Semantic Web Conference (ISWC 2017), LNCS 2017.
Tutor: Anni-Yasmin Turhan
Eigene Themenvorschläge sind auch sehr willkommen.
Organisation
Interessierte Studierende nehmen bitte bis zum 31.04.2018 Kontakt zu Prof. Franz Baader, Dr. Stefan Borgwardt, oder direkt zum jeweiligen Betreuer auf (siehe Themenliste).
Falls das Praktikum bis zum Ende des Semesters (30.09.2018) nicht abgeschlossen ist, kann die Leistung nicht anerkannt werden. Es liegt in der Verantwortung des Studierenden, die Arbeit rechtzeitig zu beginnen, und regelmäßige Treffen mit dem Betreuer zu vereinbaren.