2

在 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 do dos Z3 handle non-linear integer algorithms?），里面是Leonardo de Moura自己回答的：如果一个公式有解，我们总能通过蛮力找到力量。也就是说，我们不断枚举所有可能的赋值，并测试它们是否满足公式。这与尝试通过运行程序并检查它是否在给定数量的步骤后终止来解决停机问题没有什么不同。

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

在（https://hal.archives-ouvertes.fr/hal-00924646/document）中陈述了以下内容：哥德尔表明（NIA）是一个无法确定的问题。

此外，在（量词消除 - 更多问题）中，同样指出：NIA 不承认量词消除。此外，NIA 的决策问题是不可判定的。

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

是否存在完全无法确定的 LIA 片段？例如，在 NRA 中，在（Z3 支持非线性算术）中声明只有非线性多项式是可判定的（对于 Z3）。

谁能提供一些澄清？

4

1 回答 1

2

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

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

NIA 的实际不可判定性证明是Matyasevich 定理- 对希尔伯特著名问题之一的回答。

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

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

于 2021-11-24T13:15:34.300 回答