Validity proof of Lazard's method for CAD construction. (May 2019)

• Record Type: Journal Article
• Authors: McCallum, Scott; Parusiński, Adam; Paunescu, Laurentiu
• Is Part Of: Journal of symbolic computation. Volume 92(2019)
• Page Start: 52
• Page End: 69
• Publication Date: 2019-05
• Subjects: Cylindrical algebraic decomposition -- Lazard valuation -- Puiseux with parameter theorem; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2017.12.002
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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.