Using Tableau to Decide Description Logics with Full Role Negation and Identity

摘要

This article presents a tableau approach for deciding expressive description logics with full role negation and role identity. We consider the description logic A(L)BO~(id), which is ACC extended with the Boolean role operators, inverse of roles, the identity role, and includes full support for individuals and singleton concepts. A(L)BO~id is expressively equivalent to the two-variable fragment of first-order logic with equality and subsumes Boolean modal logic. In this article, we define a sound, complete, and terminating tableau calculus for A(L)BO~（id） that provides the basis for decision procedures for this logic and all its sublogics. An important novelty of our approach is the use of a generic unrestricted blocking mechanism. Unrestricted blocking is based on equality reasoning and a conceptually simple rule, which performs case distinctions over the identity of individuals. The blocking mechanism ties the proof of termination of tableau derivations to the finite model DroDertv of A(L)BO~(id).