基于表决的语句同一非弗赖格逻辑判定过程
计算机科学中的逻辑
2021-07-16 v1
摘要
带同一的语句演算（SCI）是经典命题逻辑的扩展，具有一个新的公式间同一连接词。在 SCI 中，若两个公式具有相同的指称，则称它们同一。在该逻辑的语义中，真值与指称相区分，因此同一连接词严格强于经典等价。本文提出一种基于标记表决（labelled tableaux）的、判定 SCI 公式可满足性的可靠、完备且终止的算法。据我们所知，这是首个实现的 SCI 判定过程，其运行时间为 NP，即复杂度最优。所获得的复杂度界源于将算法中的推导规则分为两组：分解规则与相等规则，二者的相互作用产生关于所考察公式规模具有多项式长度分支的推导树。我们描述了该过程的实现，并将其性能与其他 SCI 演算的实现（然而这些演算的终止性结果尚未确立）进行比较。我们展示了算法可能的精炼，并讨论了将其扩展到其他非弗赖格逻辑的可能性。
引用
@article{arxiv.2104.14697,
title = {Tableau-based decision procedure for non-Fregean logic of sentential identity},
author = {Joanna Golińska Pilarek and Taneli Huuskonen and Michał Zawidzki},
journal= {arXiv preprint arXiv:2104.14697},
year = {2021}
}
备注
This is a full version of a conference paper that will appear in the proceedings of the 28th International Conference on Automated Deduction (CADE)