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

Question

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

似乎在 Z3 的非线性多项式实数算术实现上有一个 paper。我没有很强的形式化方法/数学背景。对此问题背后的任何直觉表示赞赏！

Answer 1

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

我在this answer 中举了几个例子。我再给出一个：考虑方程y = x²。如果 x 和 y 是实数，则 y 是正负 x 的平方根（假设x 是非负数）。但是，如果您说 x 和 y 必须是整数，那么 y = x² 可能有也可能没有一个解决方案，取决于 x 的值。

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