以表格为基础的关于非弗吉亚机密身份逻辑的决定程序 (Tableau-based decision procedure for non-Fregean logic of sentential identity)

from arxiv, This is a full version of a conference paper that will appear in the proceedings of the 28th International Conference on Automated Deduction (CADE)

Sentential Calculus with Identity (SCI) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of SCI-formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

翻译：具有身份的感官计算( SCI) 是传统理论逻辑的延伸, 体现了公式之间特性的新联系。在 SCI 中, 两种公式如果具有相同的批注, 可以说是相同的。在逻辑的语义中, 真理价值被区别于分解, 因此, 特征连接比古典等同性。在本文中, 我们展示了一种根据标签表来决定 SCI 公式的相对性的合理性的合理、完整和终止算法。据我们所知, 这是 SCI 的第一个实施的决定程序, 它在NP 中运行, 也就是说, 复杂性- 最佳性。获得的复杂性约束是将算法的衍生规则分为两组的结果: 分解和平等性规则, 其相互作用产生与所调查公式的多面长度分支的衍生树。我们描述程序的执行情况, 并将其与 SCI 的另一种计算方法( 但是没有确定终止结果 ) 的执行情况进行比较。我们展示了可能的逻辑改进, 并讨论其他算法的可能性。

相关内容