Using tableau to decide description logics with full role negation and identity
Using tableau to decide description logics with full role negation and identity
复制标题
DOI：
10.1145/2559947
复制
发表时间：
2012-08
期刊：
影响因子：
--
通讯作者：
R. Schmidt;D. Tishkovsky
中科院分区：
文献类型：
--
作者：
R. Schmidt;D. Tishkovsky
本文提出了一种用完全角色否定和角色同一性来决定表达性描述逻辑的表格方法。我们考虑描述逻辑ALBOid，它是ALC扩展的布尔角色操作符，角色的逆，身份角色，并包括对个体和单例概念的完全支持。ALBOid在表达式上等价于一阶逻辑的两个变量片段，并包含布尔模态逻辑。在本文中，我们为ALBOid定义了一个健全、完整和终止的表演算，它为这个逻辑和它的所有子逻辑的决策过程提供了基础。我们的方法的一个重要新颖之处在于使用了通用的不受限制的阻塞机制。无限制阻塞基于平等推理和一个概念上简单的规则，它在个体的身份上执行案例区分。阻塞机制将表导数的终止证明与ALBOid的有限模型性质联系起来。
This article 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 article, 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.