Deduction in ontologies via ASP

Ontologies have become an important methodology for representing knowledge, particularly for allowing agents to interchange knowledge over the world-wide-web. From an abstract point of view, an ontology can be seen as a theory about a set of classes. The language underlying the ontology may or may not be decidable; if it is, it is often called a description logic, and the problem of determining whether one description logic formula implies (or subsumes) another is fundamental to deduction in ontologies. This paper models description logics as first-order theories, and employs model-theoretic techniques to determine properties of various description logics. These properties are used to design efficient engines to generate Answer Set Programs that perform deduction in ontologies. This approach contrasts to tableaux theorem proving techniques that are more commonly used. The resulting system serves as an experimental platform to explore the combination of logic-programming based techniques for non-monotonic reasoning and constraint handling with description-logic based deduction. Specifically, we use ASP to create a small but powerful theorem prover for the description logic ALCQI. While ALCQI is P-space complete, our deduction engine requires exponential space in the worst case. However experiments show that its time is roughly comparable to the one of the best tableaux-based engined, DLP [1], even though DLP is written for a simpler description logic, ALCN ¹.