@ARTICLE{SchmidtTishkovsky14,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2014},
TITLE = {Using Tableau to Decide Description Logics with Full Role Negation and Identity},
JOURNAL = {ACM Transactions on Computational Logic},
VOLUME = {15},
NUMBER = {1},
DOI = {10.1145/2559947},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/SchmidtTishkovsky13a.html},
ABSTRACT = {
This paper presents a tableau approach for deciding expressive
description logics with full role negation and role identity.
We consider the description logic ALBOid, which is ALC extended
with the Boolean role operators, inverse of roles, the identity
role, and includes full support for individuals and singleton
concepts.  ALBOid is expressively equivalent to the two-variable
fragment of first-order logic with equality and subsumes Boolean
modal logic.  In this paper we define a sound, complete and
terminating tableau calculus for ALBOid 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 property of ALBOid.
}
}