爲什麼非線性實數算術可判定，而非線性整數算術不可？

Question

我知道非線性整數算術基本上是希爾伯特的第十個問題，並且被證明是不可判定的。然而Z3解算器能夠爲非線性實數算術提供完整的解決方案。我只是好奇這兩個問題之間的根本區別是什麼，所以有一個非線性實數算術的確定算法？

好像有一個paper Z3的實現非線性多項式實數算術。我沒有很強的正式方法/數學背景。任何在這個問題背後的直覺表示讚賞！

Answer 1

考慮到您知道非線性實數算法是可確定的，而非線性整數算術不可行，您可以期待的最好的直覺和一些示例可幫助您瞭解QF_NIA與QF_NIA的不同之處。

我舉幾個例子this answer。我會再給一個：考慮方程y = x。如果X和ÿ是實數，則ÿ是加或減的X平方根（假設X是非負的）。然而，如果你說X和ÿ必須是整數，然後Y = X可能會或可能不會有一個解決方案，取決於X值。

基本的事實是，如果你的變量是實數，有很多數學問題很容易解決，但如果你的變量必須是整數，並且在很多情況下它們可能甚至沒有一個辦法。