Consequence-based reasoning for SRIQ ontologies
<p><em>Description logics</em> (DLs) are knowledge representation formalisms with numerous applications and well-understood model-theoretic semantics and computational properties. <em>SRIQ</em> is a DL that provides the logical underpinning for the semantic web language...
| Egile nagusia: | |
|---|---|
| Beste egile batzuk: | |
| Formatua: | Thesis |
| Hizkuntza: | English |
| Argitaratua: |
2016
|
| Gaiak: |
| _version_ | 1826277408117882880 |
|---|---|
| author | Bate, A |
| author2 | Horrocks, I |
| author_facet | Horrocks, I Bate, A |
| author_sort | Bate, A |
| collection | OXFORD |
| description | <p><em>Description logics</em> (DLs) are knowledge representation formalisms with numerous applications and well-understood model-theoretic semantics and computational properties. <em>SRIQ</em> is a DL that provides the logical underpinning for the semantic web language OWL 2, which is the W3C standard for knowledge representation on the web.</p> <p>A central component of most DL applications is an efficient and scalable reasoner, which provides services such as consistency testing and classification. Despite major advances in DL reasoning algorithms over the last decade, however, ontologies are still encountered in practice that cannot be handled by existing DL reasoners.</p> <p><em>Consequence-based calculi</em> are a family of reasoning techniques for DLs. Such calculi have proved very effective in practice and enjoy a number of desirable theoretical properties. Up to now, however, they were proposed for either Horn DLs (which do not support disjunctive reasoning), or for DLs without cardinality constraints. In this thesis we present a novel consequence-based algorithm for TBox reasoning in <em>SRIQ</em>—a DL that supports both disjunctions and cardinality constraints. Combining the two features is non-trivial since the intermediate consequences that need to be derived during reasoning cannot be captured using DLs themselves. Furthermore, cardinality constraints require reasoning over equality, which we handle using the framework of <em>ordered paramodulation</em>—a state-of-the-art method for equational theorem proving. We thus obtain a calculus that can handle an expressive DL, while still enjoying all the favourable properties of existing consequence-based algorithms, namely optimal worst-case complexity, one-pass classification, and pay-as-you-go behaviour.</p> <p>To evaluate the practicability of our calculus, we implemented it in <em>Sequoia</em>—a new DL reasoning system. Empirical results show substantial robustness improvements over well-established algorithms and implementations, and performance competitive with closely related work.</p> |
| first_indexed | 2024-03-06T23:28:27Z |
| format | Thesis |
| id | oxford-uuid:6b35e7d0-199c-4db9-ac8a-7f78256e5fb8 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:28:27Z |
| publishDate | 2016 |
| record_format | dspace |
| spelling | oxford-uuid:6b35e7d0-199c-4db9-ac8a-7f78256e5fb82022-03-26T19:02:21ZConsequence-based reasoning for SRIQ ontologiesThesishttp://purl.org/coar/resource_type/c_db06uuid:6b35e7d0-199c-4db9-ac8a-7f78256e5fb8Knowledge RepresentationLogicAutomated ReasoningArtificial IntelligenceComputer ScienceEnglishORA Deposit2016Bate, AHorrocks, IGrau, BMotik, B<p><em>Description logics</em> (DLs) are knowledge representation formalisms with numerous applications and well-understood model-theoretic semantics and computational properties. <em>SRIQ</em> is a DL that provides the logical underpinning for the semantic web language OWL 2, which is the W3C standard for knowledge representation on the web.</p> <p>A central component of most DL applications is an efficient and scalable reasoner, which provides services such as consistency testing and classification. Despite major advances in DL reasoning algorithms over the last decade, however, ontologies are still encountered in practice that cannot be handled by existing DL reasoners.</p> <p><em>Consequence-based calculi</em> are a family of reasoning techniques for DLs. Such calculi have proved very effective in practice and enjoy a number of desirable theoretical properties. Up to now, however, they were proposed for either Horn DLs (which do not support disjunctive reasoning), or for DLs without cardinality constraints. In this thesis we present a novel consequence-based algorithm for TBox reasoning in <em>SRIQ</em>—a DL that supports both disjunctions and cardinality constraints. Combining the two features is non-trivial since the intermediate consequences that need to be derived during reasoning cannot be captured using DLs themselves. Furthermore, cardinality constraints require reasoning over equality, which we handle using the framework of <em>ordered paramodulation</em>—a state-of-the-art method for equational theorem proving. We thus obtain a calculus that can handle an expressive DL, while still enjoying all the favourable properties of existing consequence-based algorithms, namely optimal worst-case complexity, one-pass classification, and pay-as-you-go behaviour.</p> <p>To evaluate the practicability of our calculus, we implemented it in <em>Sequoia</em>—a new DL reasoning system. Empirical results show substantial robustness improvements over well-established algorithms and implementations, and performance competitive with closely related work.</p> |
| spellingShingle | Knowledge Representation Logic Automated Reasoning Artificial Intelligence Computer Science Bate, A Consequence-based reasoning for SRIQ ontologies |
| title | Consequence-based reasoning for SRIQ ontologies |
| title_full | Consequence-based reasoning for SRIQ ontologies |
| title_fullStr | Consequence-based reasoning for SRIQ ontologies |
| title_full_unstemmed | Consequence-based reasoning for SRIQ ontologies |
| title_short | Consequence-based reasoning for SRIQ ontologies |
| title_sort | consequence based reasoning for sriq ontologies |
| topic | Knowledge Representation Logic Automated Reasoning Artificial Intelligence Computer Science |
| work_keys_str_mv | AT batea consequencebasedreasoningforsriqontologies |