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

Michael Schneider; Geoff Sutcliffe

doi:10.1007/978-3-642-22438-6_35

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

Michael Schneider, Geoff Sutcliffe

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

11 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 language	English (US)
Title of host publication	Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings
Pages	461-475
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-22438-6_35
State	Published - 2011
Event	23rd International Conference on Automated Deduction, CADE 23 - Wroclaw, Poland Duration: Jul 31 2011 → Aug 5 2011

Publication series

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

Other

Other	23rd International Conference on Automated Deduction, CADE 23
Country	Poland
City	Wroclaw
Period	7/31/11 → 8/5/11

Keywords

ATP
First-order logic
OWL
Semantic Web

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-22438-6_35

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

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

Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 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 proceeding › Conference contribution

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. 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 Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 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, Geoff. / Reasoning in the OWL 2 full ontology language using first-order automated theorem proving. Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 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 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",

}

TY - GEN

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

AU - Schneider, Michael

AU - Sutcliffe, Geoff

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 -