- AutorIn
- Jan Hladik
- Titel
- To and Fro Between Tableaus and Automata for Description Logics
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-ds-1201792812059-19082
- Quellenangabe
- Jan Hladik and Ulrike Sattler. A Translation of Looping Alternating Automata into Description Logics. Proceedings of CADE-19, volume 2741 of LNAI. Springer-Verlag.
- Datum der Einreichung
- 14.09.2007
- Datum der Verteidigung
- 14.11.2007
- Abstract (DE)
- Beschreibungslogiken (Description logics, DLs) sind eine Klasse von Wissensrepraesentationsformalismen mit wohldefinierter, logik-basierter Semantik und entscheidbaren Schlussfolgerungsproblemen, wie z.B. dem Erfuellbarkeitsproblem. Zwei wichtige Entscheidungsverfahren fuer das Erfuellbarkeitsproblem von DL-Ausdruecken sind Tableau- und Automaten-basierte Algorithmen. Diese haben aufgrund ihrer unterschiedlichen Arbeitsweise komplementaere Eigenschaften: Tableau-Algorithmen eignen sich fuer Implementierungen und fuer den Nachweis von PSPACE- und NEXPTIME-Resultaten, waehrend Automaten sich besonders fuer EXPTIME-Resultate anbieten. Zudem ermoeglichen sie eine vom Standpunkt der Theorie aus elegantere Handhabung von unendlichen Strukturen, eignen sich aber wesentlich schlechter fuer eine Implementierung. Ziel der Dissertation ist es, die Gruende fuer diese Unterschiede zu analysieren und Moeglichkeiten aufzuzeigen, wie Eigenschaften von einem Ansatz auf den anderen uebertragen werden koennen, um so die positiven Eigenschaften von beiden Ansaetzen miteinander zu verbinden. Unter Anderem werden Methoden entwickelt, mit Hilfe von Automaten PSPACE-Resultate zu zeigen, und von einem Tableau-Algorithmus automatisch ein EXPTIME-Resultat abzuleiten.
- Abstract (EN)
- Description Logics (DLs) are a family of knowledge representation languages with well-defined logic-based semantics and decidable inference problems, e.g. satisfiability. Two of the most widely used decision procedures for the satisfiability problem are tableau- and automata-based algorithms. Due to their different operation, these two classes have complementary properties: tableau algorithms are well-suited for implementation and for showing PSPACE and NEXPTIME complexity results, whereas automata algorithms are particularly useful for showing EXPTIME results. Additionally, they allow for an elegant handling of infinite structures, but they are not suited for implementation. The aim of this thesis is to analyse the reasons for these differences and to find ways of transferring properties between the two approaches in order to reconcile the positive properties of both. For this purpose, we develop methods that enable us to show PSPACE results with the help of automata and to automatically derive an EXPTIME result from a tableau algorithm.
- Freie Schlagwörter (DE)
- Beschreibungslogiken, Wissensrepraesentation, Automatisches Schliessen, Tableau-Algorithmen, Automatentheorie, Komplexitaet
- Freie Schlagwörter (EN)
- Description Logics, Knowledge Representation, Automated Reasoning, Tableau Algorithms, Automata Theory, Complexity
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 304, ST 130
- GutachterIn
- Prof. Dr.-Ing Franz Baader
- Prof. Dr. rer. nat. habil Ulrike Sattler
- Prof. Dr. rer. nat. habil Michael Thielscher
- BetreuerIn
- Prof. Dr.-Ing Franz Baader
- Verlag
- Technische Universität Dresden, Dresden
- URN Qucosa
- urn:nbn:de:bsz:14-ds-1201792812059-19082
- Veröffentlichungsdatum Qucosa
- 31.01.2008
- Dokumenttyp
- Dissertation
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis