标题： Lazard方法的CAD构造有效性证明 显示英文标题

标题： Validity proof of Lazard's method for CAD construction

摘要： 1994年，Lazard提出了一种改进的圆柱代数分解（CAD）方法。 该方法包括一个简化的投影运算以及一种广义的单元提升（即，堆栈构造）技术。 为了证明该方法的有效性，Lazard引入了多元多项式在一点处的新估值概念。 然而，随后发现他的证明中的一个关键支持结果存在漏洞。 在本文中，我们提供了Lazard方法的完整有效性证明。 我们的证明基于普森定理的经典参数化版本以及Lazard估值的基本性质。 这一结果具有重要意义，因为 Lazard的方法可以应用于任何有限多项式族，而无需对坐标系做出任何假设。 因此，它具有更广泛的应用范围，并且可能比其他CAD的投影和提升方案更高效。 显示英文摘要

摘要： 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.