Hypertableau Reasoning for Description Logics
We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning c...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2014
|
| _version_ | 1797068945294884864 |
|---|---|
| author | Motik, B Shearer, R Horrocks, I |
| author_facet | Motik, B Shearer, R Horrocks, I |
| author_sort | Motik, B |
| collection | OXFORD |
| description | We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions---a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies. |
| first_indexed | 2024-03-06T22:17:19Z |
| format | Journal article |
| id | oxford-uuid:53cf1854-c675-4d7c-bdc1-a82e182a4309 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T22:17:19Z |
| publishDate | 2014 |
| record_format | dspace |
| spelling | oxford-uuid:53cf1854-c675-4d7c-bdc1-a82e182a43092022-03-26T16:34:05ZHypertableau Reasoning for Description LogicsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:53cf1854-c675-4d7c-bdc1-a82e182a4309EnglishSymplectic Elements at Oxford2014Motik, BShearer, RHorrocks, IWe present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions---a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies. |
| spellingShingle | Motik, B Shearer, R Horrocks, I Hypertableau Reasoning for Description Logics |
| title | Hypertableau Reasoning for Description Logics |
| title_full | Hypertableau Reasoning for Description Logics |
| title_fullStr | Hypertableau Reasoning for Description Logics |
| title_full_unstemmed | Hypertableau Reasoning for Description Logics |
| title_short | Hypertableau Reasoning for Description Logics |
| title_sort | hypertableau reasoning for description logics |
| work_keys_str_mv | AT motikb hypertableaureasoningfordescriptionlogics AT shearerr hypertableaureasoningfordescriptionlogics AT horrocksi hypertableaureasoningfordescriptionlogics |