关于Bernays-Schönfinkel-Ramsey分离逻辑的表达完备性
计算机科学中的逻辑
2018-02-19 v2
摘要
本文研究了分离逻辑的可满足性问题，该逻辑具有无限制嵌套的分离合取与分离蕴涵，针对量词前缀在语言中的前束公式，且可能位置的全域为可数无穷或有限。类比于带未解释谓词和等式的一阶逻辑，我们称此片段为Bernays-Schönfinkel-Ramsey分离逻辑[BSR(SLk)]。我们表明，与一阶逻辑不同，BSR(SLk)的（有）限可满足性问题是不可判定的，并且我们定义了其两个非平凡子集，通过控制全称量化变量在分离蕴涵作用域内的出现以及后者出现的极性，分别可判定有限与无限可满足性。可判定性结果通过受控消除分离连接词获得，描述为：(i) 将前束形分离逻辑公式有效翻译为仅使用一阶连接词的一小组\emph{测试公式}的组合，随后(ii) 将后者翻译为等可满足的一阶公式。
引用
@article{arxiv.1802.00195,
title = {On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic},
author = {Mnacho Echenim and Radu Iosif and Nicolas Peltier},
journal= {arXiv preprint arXiv:1802.00195},
year = {2018}
}