Validity proof of Lazard's method for CAD construction
Validity proof of Lazard's method for CAD construction
复制标题
DOI：
10.1016/j.jsc.2017.12.002
复制
发表时间：
2019-05-01
影响因子：
0.7
通讯作者：
Paunescu, Laurentiu
中科院分区：
文献类型：
--
作者：
McCallum, Scott;Parusinski, Adam;Paunescu, Laurentiu
1994年Lazard提出了圆柱代数分解（CAD）的改进方法。该方法包括一个简化的投影操作和一个广义的单元提升（即堆栈构建）技术。为了证明该方法的有效性，Lazard引入了多元多项式在一点处求值的新概念。然而，在他的证明的一个关键支持结果中，一个缺口随后被注意到。本文给出了Lazard方法的一个完整的有效性证明。我们的证明是基于普塞定理的经典参数化版本和拉扎德估值的基本性质。这个结果很重要，因为Lazard的方法可以应用于任何有限的多项式族，而不需要对坐标系做任何假设。因此，它具有更广泛的适用性，并且可能比CAD的其他投影和提升方案更有效。(C) 2018 Elsevier Ltd.版权所有。
In 1994 Lazard proposed an improved method for cylindrical algebraic decomposition (CAD). The method comprised a simplified projection operation together with a generalized cell lifting (that is, stack construction) technique. For the proof of the method's validity Lazard introduced a new notion of valuation of a multivariate polynomial at a point. However a gap in one of the key supporting results for his proof was subsequently noticed. In the present paper we provide a complete validity proof of Lazard's method. Our proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation. This result is significant because Lazard's method can be applied to any finite family of polynomials, without any assumption on the system of coordinates. It therefore has wider applicability and may be more efficient than other projection and lifting schemes for CAD. (C) 2018 Elsevier Ltd. All rights reserved.