小编que*_*ten的帖子

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

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