Bernays-Schönfinkel-Ramsey 片段与简单线性整数算术的结合

通常，扩展了线性整数算术的一阶谓词逻辑是不可判定的。我们证明了扩展了受限形式线性整数算术的 Bernays-Schönfinkel-Ramsey 片段（$\exists^* \forall^*$ 句子）可通过有限基实例化判定。所识别出的基实例可用于大幅限制现有自动推理程序的搜索空间，例如，在对 Bradley、Manna 和 Sipma 的数组性质片段中形式化的数组数据结构的量化性质进行推理时。通常，数组性质片段的判定过程基于将全称量化的数组索引与当前公式中出现的所有基索引项进行穷举实例化。我们的结果表明，可以使用显著更少的实例来完成。