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

Michael Schneider, Geoffrey Sutcliffe

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

10 Citations (Scopus)

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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages461-475
Number of pages15
Volume6803 LNAI
DOIs
StatePublished - 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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Automated Theorem Proving
Theorem proving
Semantic Web
Ontology
Reasoning
First-order
World Wide Web
Semantics
First-order Logic
Fragment
Language

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Schneider, M., & Sutcliffe, G. (2011). Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6803 LNAI, 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

Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. / Schneider, Michael; Sutcliffe, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI 2011. p. 461-475 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI).

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

Schneider, M & Sutcliffe, G 2011, Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 6803 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6803 LNAI, pp. 461-475, 23rd International Conference on Automated Deduction, CADE 23, Wroclaw, Poland, 7/31/11. https://doi.org/10.1007/978-3-642-22438-6_35
Schneider M, Sutcliffe G. Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI. 2011. p. 461-475. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-22438-6_35
Schneider, Michael ; Sutcliffe, Geoffrey. / Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6803 LNAI 2011. pp. 461-475 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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 Geoffrey Sutcliffe",
year = "2011",
doi = "10.1007/978-3-642-22438-6_35",
language = "English (US)",
isbn = "9783642224379",
volume = "6803 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "461--475",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

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

AU - Schneider, Michael

AU - Sutcliffe, Geoffrey

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

VL - 6803 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 461

EP - 475

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -