@inproceedings{694245c753454e9090f81aeb9a0c7a88,
title = "Reasoning in the OWL 2 full ontology language using first-order automated theorem proving",
abstract = "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.",
keywords = "ATP, First-order logic, OWL, Semantic Web",
author = "Michael Schneider and Geoff Sutcliffe",
year = "2011",
doi = "10.1007/978-3-642-22438-6_35",
language = "English (US)",
isbn = "9783642224379",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "461--475",
booktitle = "Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings",
note = "23rd International Conference on Automated Deduction, CADE 23 ; Conference date: 31-07-2011 Through 05-08-2011",
}