带简单界限的 Bernays-Schoenfinkel-Ramsey 片段是 NEXPTIME-完全的
计算机科学中的逻辑
2020-01-07 v2 计算复杂性
摘要
一般而言，扩展了线性算术的一阶谓词逻辑是不可判定的。我们表明，扩展了仅限于简单界限（SB）的线性算术的 Bernays-Schönfinkel-Ramsey (BSR) 片段可通过有限基例实例化进行判定。所识别的基例可用于限制现有 BSR(SB) 自动推理过程的搜索空间。与 BSR 相比，BSR(SB) 的可满足性仍然是 NEXPTIME-完全的。该可判定性结果几乎是紧的，因为若将 BSR 扩展以包含线性差分不等式、简单加法不等式、商不等式和乘法不等式，则其变为不可判定。
引用
@article{arxiv.1501.07209,
title = {Bernays-Schoenfinkel-Ramsey with Simple Bounds is NEXPTIME-complete},
author = {Marco Voigt and Christoph Weidenbach},
journal= {arXiv preprint arXiv:1501.07209},
year = {2020}
}
备注
This is a revised version of the initial arXiv submission. Although submitted in 2020, the last update of its contents dates back to June 2015