TY - GEN
T1 - Reasoning in the OWL 2 full ontology language using first-order automated theorem proving
AU - Schneider, Michael
AU - Sutcliffe, Geoff
N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.
PY - 2011
Y1 - 2011
N2 - OWL 2 has been standardized by the World Wide Web Consortium (W3C) as a family of ontology languages for the Semantic Web. The most expressive of these languages is OWL 2 Full, but to date no reasoner has been implemented for this language. Consistency and entailment checking are known to be undecidable for OWL 2 Full. We have translated a large fragment of the OWL 2 Full semantics into first-order logic, and used automated theorem proving systems to do reasoning based on this theory. The results are promising, and indicate that this approach can be applied in practice for effective OWL reasoning, beyond the capabilities of current Semantic Web reasoners.
AB - OWL 2 has been standardized by the World Wide Web Consortium (W3C) as a family of ontology languages for the Semantic Web. The most expressive of these languages is OWL 2 Full, but to date no reasoner has been implemented for this language. Consistency and entailment checking are known to be undecidable for OWL 2 Full. We have translated a large fragment of the OWL 2 Full semantics into first-order logic, and used automated theorem proving systems to do reasoning based on this theory. The results are promising, and indicate that this approach can be applied in practice for effective OWL reasoning, beyond the capabilities of current Semantic Web reasoners.
KW - ATP
KW - First-order logic
KW - OWL
KW - Semantic Web
UR - http://www.scopus.com/inward/record.url?scp=80051678132&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80051678132&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22438-6_35
DO - 10.1007/978-3-642-22438-6_35
M3 - Conference contribution
AN - SCOPUS:80051678132
SN - 9783642224379
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 461
EP - 475
BT - Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings
T2 - 23rd International Conference on Automated Deduction, CADE 23
Y2 - 31 July 2011 through 5 August 2011
ER -