Z3：是非线性整数算术不可判定或半可判定的

Question

在 Z3 (Python) 中，我解决了以下问题：

y1,y2,x = Ints('y1 y2 x')
univ = ForAll([x], (y1<y2+x*x))
phi = Exists([y1,y2], univ)

solve(phi)

注意编码没有意义，随便玩玩

关键是结果完全出乎我的意料，因为它返回了一个结果！这是令人惊讶的，因为我一直在研究一阶理论，据我所知，LIA 是可判定的，而 NIA 不是（有理数也是如此）。顺便说一下，结果是 []：即有效。

所以我在这边搜索了这个问题，找到了（How does Z3 handle non-linear integer arithmetic?），Leonardo de Moura 本人回答如下：如果一个公式有解，我们可以总是通过蛮力找到它。也就是说，我们不断地枚举所有可能的赋值，并测试它们是否满足公式。这与尝试通过运行程序并检查它是否在给定的步数后终止来解决暂停问题没有什么不同。

好的，我知道 NIA 是 半可判定的 。这样对吗？然而...

在 (https://hal.archives-ouvertes.fr/hal-00924646/document) 中陈述如下：哥德尔表明 (NIA) 是一个不可判定的问题。

另外，在(Quantifier Elimination - More questions)中，也是这样说的：NIA不承认量词消去。此外，NIA的决策问题是不可判定的。

那么，NIA是不可判定的还是半可判定的？显然，我看到可以有一些解决方案。那么哥德尔在不可判定的意义上是否意味着不可判定（但对 semi-可判定性只字不提）？

是否存在完全不可判定的 LIA 片段？例如，在 NRA 中，在 (Z3 support for nonlinear arithmetic) 中声明只有非线性 多项式 是可判定的（对于 Z3）。

任何人都可以提供一些说明吗？

Answer 1

半可判定问题的class是不可判定问题的子class。

由于我们正在寻找整数解，因此有一种简单的方法可以枚举某些自然数 n 的参数化解：首先考虑变量的所有值，使其绝对值之和为 0，然后为 1，依此类推. 并检查等式是否成立。该策略涵盖所有可能的值，这样算法最终将 return 一个解决方案（如果存在）或继续无限期地枚举。这是半可判定算法的定义，所以如果我们有一个不可判定的结果，它在最坏的情况下是半可判定的。

NIA 的实际不可判定性证明是 Matyasevich's Theorem - 希尔伯特著名问题之一的答案。

class 的可判定性意味着每个实例都是可判定的。由于 LIA 是可判定的，因此没有不可判定的反例。

顺便说一下：real closed fields 是一个可判定的理论（通过用值替换量化变量来证明工作——这是量词消除的一个例子）这意味着 NRA 也是可判定的。这对我来说有点违反直觉，因为整数算术感觉更简单。现在我认为它是具有更多可能解决方案的实数，其中解决方案是整数的附加约束是困难的部分。

Z3：是非线性整数算术不可判定或半可判定的

Z3: is Nonlinear integer arithmetic undecidable or semi-decidable

z3

z3py

theorem-proving

first-order-logic

decidable