Using Tableau to Decide Description Logics with Full Role Negation and Identity
Renate A. Schmidt, Dmitry Tishkovsky

TL;DR
This paper introduces a tableau-based decision procedure for the expressive description logic ALBOid, incorporating full role negation and identity, using an innovative unrestricted blocking mechanism to ensure termination.
Contribution
It develops a sound and complete tableau calculus for ALBOid with a novel unrestricted blocking rule, advancing decision procedures for highly expressive description logics.
Findings
Provides a decision procedure for ALBOid and its sublogics
Uses a generic unrestricted blocking mechanism for termination
Links proof termination to the finite model property of ALBOid
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
