Tableau calculi for CSL over minspaces
Tableau calculi for CSL over minspaces
复制标题
最小空间上的 CSL 的 Tableau 演算
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
D. Tishkovsky
中科院分区：
文献类型：
--
作者：
R. Alenda;N. Olivetti;C. Schwind;D. Tishkovsky
Shemeret、Tishkovsky、Zakharyashev和Wolter于2005年提出了比较概念相似性CSL逻辑，以表达一种关于本体中概念的定性相似性推理。逻辑的语义是根据距离空间定义的；然而，它可以等价地用优先结构重新表述，类似于条件逻辑的那些。本文考虑在满足极限假设的对称和非对称距离模型上解释的CSL，即所谓的最小空间距离模型。我们通过两种方式为CSL的自动扣除做出贡献。首先用有限过滤法证明了该逻辑对于其优先语义具有有效的有限模型性质。然后，我们给出了在对称和非对称最小空间距离模型上解释CSL的两种情况的标记表演算的决策过程。通过施加适当的阻塞条件，可以得到微积分的终止。
The logic of comparative concept similarity CSL has been introduced in 2005 by Shemeret, Tishkovsky, Zakharyashev and Wolter in order to express a kind of qualitative similarity reasoning about concepts in ontologies. The semantics of the logic is defined in terms of distance spaces; however it can be equivalently reformulated in terms of preferential structures, similar to those ones of conditional logics. In this paper we consider CSL interpreted over symmetric and nonsymmetric distance models satisfying the limit assumption, the so-called minspace distance models. We contribute to automated deduction for CSL in two ways. First we prove by the finite filtration method that the logic has the effective finite model property with respect to its preferential semantics. Then we present a decision procedure in the form of a labeled tableau calculus for both cases of CSL interpreted over symmetric and non-symmetric minspace distance models. The termination of the calculus is obtained by imposing suitable blocking conditions.