实数的一阶理论有实现吗？我知道柯林斯存在一种基于圆柱代数分解的技术，但我不知道有任何实现它的定理证明器。
这里列出了 z3 为各种算术域实现的决策过程：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arithmetic.