英文:
Implementation for decision procedure for the theory of the reals
问题
有关实数的一阶理论的实现吗？我知道Collins基于圆柱代数分解提出了一种技术，但我不知道有哪些定理证明器实现了它。
英文:
Is there an implementation for the first-order theory of the reals? I know there exists one technique by Collins based on cylindrical algebraic decomposition but I don't know of any theorem provers that implement it.
答案1
得分: 0
决策程序由z3实现，用于各种算术领域，详见：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arithmetic。
英文:
The decision procedures implemented by z3 for various arithmetic domains is listed here: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arithmetic.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论