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

Schmidt, R. A. and Tishkovsky, D. (2014)

ACM Transactions on Computational Logic 15 (1). BiBTeX, PDF (DOI link to TOCL).

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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 16 Oct 14
Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk