SMT-LIB中的QF_NRA逻辑是可判定的吗？

Question

SMT-LIB中的QF_NRA逻辑是可判定的吗？

我知道Tarski证明了非线性算法是可判定的，在实数中多项式系统是可判定的。然而，QF_NRA是否属于这一保护伞并不明显，因为QF_NRA包含除法。第一个问题是，QF_NRA中的除法是否包括分母可能为零的变量除法。我把它作为一个单独的问题发布，因为答案本身就足够困难了。

如果零除法不是QF_NRA的一部分，那么QF_NRA中的除法就可以转换为乘法，这个问题将如Tarski所证明的那样是可判定的。如果QF_NRA中实际上包含了部门，那么我就不太确定了。我的感觉是，这个问题仍然可以按情况分解，在除以零的情况下引入新的变量。在这种情况下，QF_NRA仍然是可判定的。

Answer 1

它是可判定的。

您可以通过将除法视为一个未解释的函数来编码SMT-LIB除法，在需要时，可以将其公理化，即对于问题中出现的每个(/ t1 t2)，可以添加

t2 != 0 => t1 = (/ t1 t2)*t2  .

这实际上将QF_NRA的SMT理论简化为两种理论的结合: reals (无除法)和未解释函数。现在，由于reals和未解释函数都是无量词片段中的可判定理论，所以可以依靠Nelson和Oppen的经典论点来证明组合理论是可判定的。

例如，Yices2可以决定reals和未解释函数的组合(基于MCSAT)。据我所知，Z3不能将reals和未解释的函数组合在一起，而且CVC4还没有对reals的判定过程。