Study of an Epistemic Description Logic with Transitive Roles

Description logic is the logical foundation of the semantic Web. It is a tool for formally expressing domain knowledge. Description logic is the decidable fragment of the first order logic and suitable for modeling the concept terminology of domain knowledge. Because some application requirements and people can not describe all of the domain knowledge, there is lots of incomplete knowledge on the Web. Description logic is based on the open world assumption. It can only express the monotonic reasoning and can not solve the incomplete knowledge. By adding the epistemic operator “K” to the description logic, the epistemic description logic can be obtained. It has the advantage of dealing with the incomplete knowledge because of the non-monotonic features and the good computational complexity. The authors present a new epistemic description logic ALCKR\-+ based on the epistemic description logic ALCK, preserve the primary advantage of the description logic, add transitive roles for improving the expressivity, express the non-monotonic reasoning ability through the epistemic query, and design the syntax and semantic of ALCKR\-+. The corresponding tableau algorithm is also provided. The soundness and decidability of the tableau algorithm are proved. It is shown that the complexity of tableau algorithm is PSPACE-complete.