如果一个理论在存在片段中是可判定的，这是否意味着有一个（终止）方法来获得满意的证人？

Question

我担心是否有算法（例如，在 SMT 求解器中实现）保证终止给出存在公式模型的任务；他们以同样的方式保证可满足性问题的终止。让我试着解释一下。

---

如果一阶理论

T

在其存在片段上是可判定的，这意味着存在一种方法（保证终止）可以解决

T

的所有存在公式的可满足性问题。我说得对吗？

我的问题是：

T

是否存在可判定意味着我们有一种方法（保证终止）来获得

T

内的存在公式模型？换句话说，如果我们有一种方法来解决

T

的存在公式的可满足性，这是否意味着我们也有一种方法来获得此类公式的模型（在可满足的实例中）？

例如，考虑线性整数算术理论。我们知道有一个终止算法（即 Cooper 方法）执行量词消除 (QE)，如果所有变量都受量词限制，则产生一个决策过程。这意味着 Cooper 可以解决具有终止保证的线性算术的可满足性问题。这也意味着，如果 SMT 求解器（比如 Z3）针对可满足性问题实施 Cooper，那么它（理论上）会提供终止。对吧？

但是，如果我们要求模型怎么办？很明显，对于这个理论，没有必要计算满意度见证（已经使用 QE 完成），所以可能没有办法获得这个见证。换句话说，例如，我们可以使用 Cooper 来决定

∃x,y. (x<y)

的可满足性，但不需要见证人！

那么，是否有类似的方法可以保证终止并提供模型？ 也许对QE方法进行一些修改？我认为可能是这种情况，因为 QE 方法以某种方式计算测试点，也许我们可以提取这些点的见证......

此外，考虑有限理论（例如，自然数达到

100

）。那么，很明显，通过枚举，我们都可以有一个方法来决定可满足性并返回一个见证。我关心的是无限理论。正如我们所看到的，QE 并不意味着 witness obtention，但也许有一些结果可以保证，如果一个理论被证明可以用 QE 方法确定，那么还有另一种方法可以计算 witnesses。

在肯定回答的情况下，SMT 求解器（其中任何一个）是否实施这些保证模型提供？如果不是，为什么会这样？ SMT 求解器的文献中是否有关于此的任何信息？