Validity proof of Lazard's method for CAD construction

DOI10.1016/J.JSC.2017.12.002MaRDI QIDQ1757004zbMATH OpenOpenAlexFDO

Authors Scott McCallum, Adam Parusiński, Laurentiu Paunescu

Publication date 28 December 2018

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1607.00264

cylindrical algebraic decomposition Lazard valuation Puiseux with parameter theorem

Quantifier elimination, model completeness, and related topics (03C10) Semialgebraic sets and related spaces (14P10) Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Symbolic computation and algebraic computation (68W30)

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.

Review text

The authors provide a proof of Lazard's method for cylindrical algebraic decomposition. This method was introduced by \textit{D. Lazard} [in: Algebraic geometry and its applications. Collections of papers from Shreeram S. Abhyankar's 60th birthday conference held at Purdue University, West Lafayette, IN, USA, June 1-4, 1990. New York: Springer-Verlag. 467--476 (1994; Zbl 0822.68118)]. It can be applied to any finite family of polynomials, without any assumption on the system of coordinates. The method therefore has wider applicability and may be more efficient than other projection and lifting schemes for cylindrical algebraic decomposition. However, the proof presented in the aforementioned article was not complete due to a gap in one of the key supporting results. In [\textit{S. McCallum} and \textit{H. Hong}, J. Symb. Comput. 72, 65--81 (2016; Zbl 1325.13026)] it was shown that Lazard's projection is valid for cylindrical algebraic decomposition construction for so-called well oriented polynomial sets. The present article provides a complete validity proof of Lazard's method using Lazard's notion of valuation. The proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation.

Recommendations

Cites work

Cited in

(18)

Describes a project that uses

Uses Software

QEPCAD

This page was built for publication: Validity proof of Lazard's method for CAD construction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1757004)