TY - GEN
T1 - Deduction in ontologies via ASP
AU - Swift, Terrance
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2004.
PY - 2004
Y1 - 2004
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 -