logic - 为什么非线性实数算术可判定而非线性整数算术不可判定？

Question

我知道非线性整数算术基本上是希尔伯特的第十个问题，并且被证明是不可判定的。然而，Z3 求解器能够为非线性实数算法提供完整的解决方案。我只是好奇这两个问题之间的根本区别是什么，以便有一个确定的非线性实数算法？

好像有一个 paper关于 Z3 的非线性多项式实数算法的实现。我没有很强的正式方法/数学背景。对这个问题背后的任何直觉表示赞赏!

Answer 1

考虑到您知道非线性实数算术是可判定的，而非线性整数算术则不是，您所能希望的最好是更好的直觉和一些示例，以帮助您了解 QF_NRA 与 QF_NIA 的不同之处。

我在this answer中举了几个例子.我再给出一个:考虑方程 y = x2。如果 x 和 y 是实数，则 y 是加或减 x 的平方根(假设 x 是非负数)。然而，如果你说 x 和 y 必须是整数，那么 y = x2 可能有也可能没有解，这取决于 x 的值。

基本事实是，如果您的变量是实数，则有很多数学问题很容易解决，但如果您的变量必须是整数，则要困难得多，在某些情况下，它们甚至可能没有解决方案。