Entwicklung und Evaluierung eines parallelen Tableau-Reasoners für Beschreibungslogiken

Schlussfolgern mit ausdrucksmächtigen Beschreibungslogiken ist ein, in komplexitätstheoretischen Sinn, sehr schwieriges Problem. Zur Zeit bekannte, hochoptimierte Tableauverfahren z.B. für die Beschreibungslogik SHIF befinden sich in der Komplexitätsklasse 2EXPTIME. Quellen für inhärente Komplexität sind zum Beispiel Disjunktionen und Maximumkardinalitätsrestriktionen.

Parallelverarbeitung ist eine bisher wenig betrachtete Möglichkeit zur Beschleunigung des Tableau-Algorithmus. Der in dieser Arbeit verfolgte Ansatz bearbeitet den durch Disjunktion und Maximumkardinalität erzeugten Nichtdeterminismus parallel, da sich dieser leicht auf eine nebenläufige Verarbeitungsweise abbilden lässt.

Parallelität in einem ansonsten naiven Tableau-Algorithmus jedoch ist wenig vielversprechend. Eine Reihe effektiver und allgemein verwendeter Optimierungen des Verfahrens wurde in der Arbeit deshalb auf ihre Realisierbarkeit in einem parallelen Reasoner untersucht.

Basierend auf den angestellten Überlegungen wurde eine prototypische Implementierung erstellt. Dafür wurde die Architektur eines Parallelrechners mit gemeinsamem Speicher gewählt, auf deren Basis der Tableau-Algorithmus mittels des Workpool-Modells realisiert wurde. Die Implementierung unterstützt TBox- und ABox-Reasoning in der Beschreibungslogik SHN und erlaubt die Verwendung von GCI-Axiomen.

Die Ergebnisse einer durchgeführten Evaluierung zeigen, dass sich mit dieser Methode signifikante Performancesteigerungen erzielen lassen. Im Vortrag werden Möglichkeiten und Ideen zur weitere Verbesserung des Ansatzes aufgezeigt. Diese zielen auf eine bessere Ausnutzung des vorhandenen Rechenkraftpotentials, Anwendung weiterer Optimierungen und die Erweiterung auf ausdrucksmächtigere Beschreibungslogiken ab.