@MISC{SchmidtTishkovsky12a,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2012},
TITLE = {Using Tableau to Decide Description Logics with Full Role Negation and Identity},
URL = {http://arxiv.org/abs/1208.1476v1},
NOTE = {arXiv e-Print 1208.1476v1 [cs.LO]},
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 the 
extension of ALC 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 and complete tableau calculus for the ALBOid 
that provides a 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. Being 
based on a conceptually simple rule, unrestricted blocking 
performs case distinctions over whether two individuals are 
equal or not and equality reasoning to find finite models.
The blocking mechanism ties the proof of termination of 
tableau derivations to the finite model property of ALBOid.
}
}