Tableaubasierte Ableitung und Erklärung von Subsumtionsbeziehungen

Durch die Vision des Semantic Web haben Wissensrepräsentationssysteme in den letzten Jahren an Bedeutung gewonnen und verstärkte Forschungs- und Entwicklungsaktivitäten in diesem Gebiet nach sich gezogen. Dies hat zur Entwicklung der Web Ontology Language (OWL) geführt, einer Sprache zur Repräsentation von Wissen, die auf dem logikbasierten Formalismus der Beschreibungslogiken fußt. Die Erfahrungen von Ontolgie-Entwicklern zeigen, dass nicht nur Neueinsteiger Probleme haben, Auswirkungen von Modellierungsentscheidungen nachzuvollziehen. Ein besseres Verständnis kann durch einen ad-hoc Erklärungsdienst für Subsumtion, einen Standardinferenzdienst ontologiebasierter Schlussfolgerungssysteme erreicht werden.

In dieser Masterarbeit wird eine Methode für die natürlichsprachliche Erklärung von Subsumtionsbeweisen in der Beschreibungslogik SHIN dargestellt, dabei wurde ein beweistheoretischer Ansatz auf der Basis des Tableaukalküls verfolgt. Die Erklärung erfolgt im Anschluss an den Beweis und verwendet die mit Informationen angereicherte Struktur eines Tableaubeweises zur Erzeugung textueller Erläuterungen. Anhand annotierbarer Terme werden die für einen Widerspruch relevanten Terme identifiziert und irrelevante Konstrukte in der Erklärung ausgeblendet. Des Weiteren wird beschrieben, wie zu verfahren ist, wenn ein Tableau verschiedene Erklärungsalternativen enthält und wie die Alternativen qualitativ differenziert werden können. Zusätzlich werden einige Optimierungstechniken vorgestellt, die einerseits eine Steigerung der Erklärungsqualität und andererseits der Effizienz des Tableau-Algorithmus zulassen.

Im Rahmen der Arbeit wurde eine prototypische Implementierung für die Beschreibungslogik SHF entwickelt. Die Implementierung diente der Evaluierung des Ansatzes und dessen Eignung für praktische Anwendungsszenarien sowie der Gewinnung neuer Erkenntnisse bzgl. betrachteter Optimierungsverfahren.