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则不是(在理性主义中也是如此)。结果是[]，顺便说一句：有效。

所以我在这一边搜索了这个问题，发现(Z3如何处理非线性整数算法？)，是莱昂纳多·德莫拉自己回答如下:如果一个公式有一个解，我们总是可以用蛮力找到它。也就是说，我们一直在列举所有可能的作业，并测试它们是否满足这个公式。这与试图通过运行程序和检查程序在给定步骤后是否终止而试图解决停止问题没有多大区别。

好吧，我知道NIA是semi-decidable.是对的吗？然而..。

在(https://hal.archives-ouvertes.fr/hal-00924646/document)中:G del证明了(NIA)是一个不可判定的问题。

另外，在(量词消除-更多问题)中，同样声明: NIA不承认量词消除。另外，NIA的决策问题是不可判定的。

那么，NIA是不可判定的还是半可判定的？显然，我看到了一些解决办法。同样，在不可判定的意义上，G del的意思是不可判定的(但对semi-decidability)？只字不提)

是否有完全无法分辨的LIA片段？例如，在NRA中，在(非线性算法的Z3支持)中，只有非线性多项式是可判定的(对于Z3)。

有人能提供一些澄清吗？

Answer 1

半可判定问题是不可判定问题的一个子类.

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

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

类的可判定性意味着每个实例都是可判定的。既然LIA是可判定的，就没有不可判定的反例。

顺便说一句：实闭域是一种可判定的理论(证明方法是用值替换量化变量--这是量化消除的一个例子)，这意味着NRA也是可判定的。这对我来说有点违背直觉，因为整数仿真器感觉更简单。现在，我认为它是有更多可能的解决方案，其中附加的约束，解决方案是一个整数是困难的部分。