TY - GEN

T1 - Deduction in ontologies via ASP

AU - Swift, Terrance

PY - 2004/1/1

Y1 - 2004/1/1

N2 - 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 1.

AB - 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 1.

UR - http://www.scopus.com/inward/record.url?scp=9644264057&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=9644264057&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:9644264057

T3 - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)

SP - 275

EP - 288

BT - Logic Programming and Nonmonotonic Reasoning

A2 - Niemela, Ilkka

A2 - Lifschitz, Vladimir

PB - Springer Verlag

T2 - 7th International Conference on Logic Programming and Nonmonotonic Reasoning , LPNMR 2004

Y2 - 6 January 2004 through 8 January 2004

ER -