2001
Aachen, Techn. Hochsch., Diss., 2001
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
Tag der mündlichen Prüfung/Habilitation
2001-05-31
Online
URN: urn:nbn:de:hbz:82-opus-1702
URL: https://publications.rwth-aachen.de/record/52234/files/Tobies_Stephan.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; Wissensrepräsentation (frei) ; Terminologische Logik (frei) ; Inferenz (frei) ; Erfüllbarkeitsproblem (frei) ; Tableau (frei) ; Berechnungskomplexität (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Beschreibungslogiken (BLen) werden in wissens-basierten Systemen eingesetzt, um terminologischen Anwendungswissen zu repräsentieren und semantisch wohldefinierte Schlußfolgerungen aus diesem Wissen zu ermöglichen. Diese Arbeit beschreibt eine Reihe neuer Komplexitätsresultate und praktische Algorithmen für ausdrucksstarke Beschreibungslogiken, die über verschiedene Formen von Zählquantoren verfügen. Wir zeigen, daß es in vielen Fällen möglich ist, lokale Anzahlaussagen in Form von qualifizierenden Zahlenrestriktionen zu Beschreibungslogiken hinzuzunehmen, ohne daß dies zu einem Anstieg in der Komplexität der Schlußfolgerungsprobleme führt. Dies ist sogar dann der Fall, wenn binäre Kodierung der Zahlen in der Eingabe zugelassen wird. Im Gegensatz dazu zeigen wir, daß die Hinzunahme verschiedener Formen von globalen Anzahlrestriktionen die Komplexität der Schlußfolgerungsprobleme zum Teil drastisch erhöhen kann. Wir zeigen exakte Komplexitätsresultate und beschreiben einen praktischen, Tableau-basierten Algorithmus für die Beschreibungslogik SHIQ, welche die Grundlage des hoch-optimierten BL-Systems iFaCT darstellt. Schließlich beschreiben wir einen Tableau-Algorithmus für das Clique Guarded Fragment (CGF), von dem wir hoffen, daß er als Basis einer effizienten Implementierung eines CGF Beweisers dienen kann.Description Logics (DLs) are used in knowledge-based systems to represent and reason about terminological knowledge of the application domain in a semantically well-defined manner. In this thesis, we establish a number of novel complexity results and give practical algorithms for expressive DLs that provide different forms of counting quantifiers. We show that, in many cases, adding local counting in the form of qualifying number restrictions to DLs does not increase the complexity of the inference problems, even if binary coding of numbers in the input is assumed. On the other hand, we show that adding different forms of global counting restrictions to a logic may increase the complexity of the inference problems dramatically. We provide exact complexity results and a practical, tableau based algorithm for the DL SHIQ, which forms the basis of the highly optimized DL system iFaCT. Finally, we describe a tableau algorithm for the clique guarded fragment (CGF), which we hope will serve as the basis for an efficient implementation of a CGF reasoner.
Fulltext:
PDF
Dokumenttyp
Dissertation / PhD Thesis
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT013114727
Interne Identnummern
RWTH-CONV-114471
Datensatz-ID: 52234
Beteiligte Länder
Germany
The record appears in these collections: |