Reasoning in the OWL 2 full ontology language using first-order automated theorem proving

Michael Schneider, Geoff Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings
Pages461-475
Number of pages15
DOIs
StatePublished - Aug 19 2011
Event23rd International Conference on Automated Deduction, CADE 23 - Wroclaw, Poland
Duration: Jul 31 2011Aug 5 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6803 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other23rd International Conference on Automated Deduction, CADE 23
CountryPoland
CityWroclaw
Period7/31/118/5/11

Keywords

  • ATP
  • First-order logic
  • OWL
  • Semantic Web

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reasoning in the OWL 2 full ontology language using first-order automated theorem proving'. Together they form a unique fingerprint.

  • Cite this

    Schneider, M., & Sutcliffe, G. (2011). Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings (pp. 461-475). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI). https://doi.org/10.1007/978-3-642-22438-6_35