CAD带有等式约束的潜力和挑战对于SC-Square。
摘要：圆柱代数分解（CAD）是符号计算中的核心算法，特别用于实数量化消除和多项式系统求解等。现在，在与非线性实数算术一起使用时，它越来越多地作为满足性模理论（SMT）求解器的决策过程应用。我们讨论了SMT应用和SC-Square项目的逻辑结构引入的潜力，特别是等式约束的存在。我们还强调了利用这些的挑战：原始性限制、良序性问题和增量性的前景。
作者：James H. Davenport and Matthew England
论文ID：1711.00312
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2017-12-22