SMT-LIB 中的 QF_NRA 逻辑是否可判定？
我知道 Tarski 证明了非线性算术是可判定的，即实数中的多项式系统是可判定的。但是，QF_NRA 是否属于这一范畴并不明显，因为 QF_NRA 包含除法。所以第一个问题是 QF_NRA 中的除法是否包括分母可能为零的变量除法。 I posted that as a separate question，因为单独回答这个问题已经够难了。
如果除以零不是 QF_NRA 的一部分，那么 QF_NRA 中的除法可以转换为乘法，并且问题将是可判定的，如 Tarski 所证明的。如果除法实际上包含在 QF_NRA 中，那么我就不太确定了。我的感觉是，问题仍然可以按情况分解，为发生被零除的情况引入新变量。在这种情况下，QF_NRA 仍然是可判定的。
【问题讨论】：
标签： z3 smt theorem-proving cvc4
这是可判定的。
您可以通过将除法视为未解释的函数来编码 SMT-LIB 除法，您可以在需要的地方公理化，即对于出现在问题中的每个 (/t1 t2)，您可以添加
t2 != 0 => t1 = (/ t1 t2)*t2 .
这实际上将 QF_NRA 的 SMT-LIB 理论简化为两种理论的组合：实数（没有除法）和未解释的函数。现在，由于实数和未解释函数都是无量词片段中的可判定理论，您可以依靠 Nelson 和 Oppen 的经典论证来证明组合理论是可判定的。
Yices2，例如，可以决定这种实数和未解释函数的组合（基于 MCSAT）。据我所知，Z3 不能结合实数和未解释的函数，而 CVC4 还没有实数的决策程序。
【讨论】：
/吗？
t2 == 0 案件与 t2 != 0 案件分开的形式化，后者允许消除划分，并且通过为(/ t1 t2) 引入一个新符号，前者可以自行解决。