Reasoning with Individuals for the Description Logic SHIQ

Abstract

While there has been a great deal of work on the development of reasoning algorithms for expressive description logics, in most cases only Tbox reasoning is considered. In this paper we present an algorithm for combined Tbox and Abox reasoning in the SHIQ description logic. This algorithm is of particular interest as it can be used to decide the problem of (database) conjunctive query containment w.r.t. a schema. Moreover, the realisation of an efficient implementation should be relatively straightforward as it can be based on an existing highly optimised implementation of the Tbox algorithm in the FaCT system.

To appear at CADE-17

Cited by in corpus (10)

• Complexity Results and Practical Algorithms for Logics in Knowledge Representation
• Conjunctive Query Answering for the Description Logic SHIQ
• Reasoning with Very Expressive Fuzzy Description Logics
• Data complexity of answering conjunctive queries over SHIQ knowledge bases
• ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
• Redundancy-free Verbalization of Individuals for Ontology Validation
• Ontology Verbalization using Semantic-Refinement
• Conjunctive Query Answering via a Fragment of Set Theory (Extended Version)
• A Paraconsistent Tableau Algorithm Based on Sign Transformation in Semantic Web
• An ExpTime Procedure for Description Logic $\mathcal{A}\mathcal{LC}\mathcal{Q}\mathcal{I}$ (Draft)