Scaling Up Description Logic Reasoning by Distributed Resolution

Schlicht, Anne

Preview

PDF (Dissertation )
dissertation_schlicht.pdf - Published
Download (1MB)

URL:	https://ub-madoc.bib.uni-mannheim.de/31365
URN:	urn:nbn:de:bsz:180-madoc-313655
Document Type:	Doctoral dissertation
Year of publication:	2012
Place of publication:	Mannheim
Publishing house:	Universität Mannheim
University:	Universität Mannheim
Evaluator:	Stuckenschmidt, Heiner
Date of oral examination:	29 March 2012
Publication language:	English
Institution:	School of Business Informatics and Mathematics > Praktische Informatik II (Stuckenschmidt 2009-)
Subject:	004 Computer science, internet
Subject headings (SWD):	Automatisches Beweisverfahren , Paralleler Algorithmus , Wissensverarbeitung
Keywords (English):	Theorem Proving , Parallel Computation , Knowledge Management
Abstract:	Benefits from structured knowledge representation have motivated the creation of large description logic ontologies. For accessing implicit information and avoiding errors in ontologies, reasoning services are necessary. However, the available reasoning methods suffer from scalability problems as the size of ontologies keeps growing. This thesis investigates a distributed reasoning method that improves scalability by splitting a reasoning process into a set of largely independent subprocesses. In contrast to most description logic reasoners, the proposed approach is based on resolution calculi. We prove that the method is sound and complete for first order logic and different description logic subsets. Evaluation of the implementation shows a heavy decrease of runtime compared to reasoning on a single machine. Hence, the increased computation power pays off the overhead caused by distribution. Dependencies between subprocesses can be kept low enough to allow efficient distribution. Furthermore, we investigate and compare different algorithms for computing the distribution of axioms and provide an optimization of the distributed reasoning method that improves workload balance in a dynamic setting.
Translation of the abstract:	Der Zugang zu gespeichertem Wissen wird durch den Einsatz formaler Sprachen erheblich erleichtert. Besonders in Medizin und Biologie wird Fachwissen in Form von großen Ontologien dargestellt, um Forschung und Entwicklung zu unterstützen. Mit Methoden der Wissensrepräsentation ist es möglich, Anfragen zu komplexen Zusammenhängen automatisch zu beantworten. Allerdings stoßen bestehende Methoden bei der Bearbeitung von Anfragen schnell an die Grenzen der verfügbaren Ressourcen, wenn die verwendete Ontologie komplex und umfangreich ist. Die vorliegende Arbeit stellt einen Ansatz zur Lösung des Problems vor, der die Skalierbarkeit durch Parallelisierung der Berechnung verbessert. Durch die Aufteilung auf mehrere Prozesse wird die Rechenzeit erheblich reduziert. Die Grundidee besteht darin, die Berechnung so aufzuteilen, dass zwischen den Teilprozessen wenig Abhängigkeiten bestehen und der Kommunikationsaufwand gering ist. Das vorgeschlagene Verfahren ist auf Basis eines existierenden Prädikatenlogik Beweisers implementiert, und die Effizienz des Ansatzes wurde experimentell nachgewiesen. Zusätzlich wurden verschiedene Strategien zur Verteilung untersucht und deren Auswirkungen auf die Effizienz des Verfahrens. Des Weiteren wurde die Methode so generalisiert, dass die Verteilung zur Laufzeit auf eine veränderliche Anzahl Rechner angepasst werden kann. (German)