实数上带界差约束的 Bernays-Schönfinkel-Ramsey 片段是可判定的
计算机科学中的逻辑
2017-06-27 v1
摘要
一阶线性实数算术加上未解释谓词符号构成了一种有趣的建模语言。然而，这类公式的可满足性是不可判定的，即使将未解释谓词符号限制为一元。为了找到该语言的可判定片段，必须限制算术部分的表达能力。一种可能的途径是将算术表达式限制为形如 x - y # c 的差约束，其中 # 取标准关系 <, ≤, =, ≠, ≥, >，且 x, y 是全称量化的。但已知将差约束与未解释谓词符号结合会再次导致不可判定的可满足性问题。本文证明，如果额外限制全称量化变量的取值范围，则可满足性变为可判定。由于实数上的有界区间仍包含无穷多个值，简单的实例化过程不足以解决该问题。
引用
@article{arxiv.1706.08504,
title = {The Bernays-Sch\"onfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable},
author = {Marco Voigt},
journal= {arXiv preprint arXiv:1706.08504},
year = {2017}
}
备注
27 pages