Validity proof of Lazard's method for CAD construction

Scott McCallum*, Adam Parusiński, Laurentiu Paunescu

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

15 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)52-69
Number of pages18
JournalJournal of Symbolic Computation
Issue numberMay-June
Early online date27 Dec 2017
Publication statusPublished - 2019


  • Cylindrical algebraic decomposition
  • Lazard valuation
  • Puiseux with parameter theorem


Dive into the research topics of 'Validity proof of Lazard's method for CAD construction'. Together they form a unique fingerprint.

Cite this