Lazard's CAD exploiting equality constraints
Lazard's CAD exploiting equality constraints
复制标题
Lazard 的 CAD 利用等式约束
DOI：
10.1145/3377006.3377020
复制
发表时间：
2019
影响因子：
0.1
通讯作者：
Nair A
中科院分区：
文献类型：
--
作者：
Nair A
McCallum改进了原始的柯林斯CAD投影算子（假设良好的方向），并进一步减少了具有等式约束的量词消除问题的投影集[6，7]。Lazard提供了一个投影算子（和相应的提升过程），与McCallum的相比，它减少了投影集，并且是无条件的，就像柯林斯的原始算法[2]。我们的研究扩展了Lazard的工作，提供了一个修改，当量词消除问题中有一个等式约束时（如[6]），该修改进一步减少了投影集。我们还报告了[7]中的一个小错误。
McCallum improved the original Collins CAD projection operator (assuming well-orientation) and reduced the projection set even further for quantifier elimination problems which have equality constraints [6, 7]. Lazard provided a projection operator (and corresponding lifting process) that reduces the projection set as compared to McCallum's and is unconditional like Collins' original algorithm [2]. Our research extends Lazard's work by providing a modification that reduces the projection set even further when there is a single equality constraint in the quantifier elimination problem (as in [6]). We also report a slight error in [7].
影响因子：
0.7
作者：
McCallum, Scott;Parusinski, Adam;Paunescu, Laurentiu
通讯作者：
Paunescu, Laurentiu