Validity proof of Lazard's method for CAD construction
From MaRDI portal
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3645246 (Why is no real title available?)
- scientific article; zbMATH DE number 3823145 (Why is no real title available?)
- scientific article; zbMATH DE number 3916701 (Why is no real title available?)
- scientific article; zbMATH DE number 4029737 (Why is no real title available?)
- scientific article; zbMATH DE number 45943 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 589124 (Why is no real title available?)
- scientific article; zbMATH DE number 1157648 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 3279238 (Why is no real title available?)
- scientific article; zbMATH DE number 3196340 (Why is no real title available?)
- Algorithmic methods for investigating equilibria in epidemic modeling
- An improved projection operation for cylindrical algebraic decomposition of three-dimensional space
- Analytic functions of several complex variables
- Arc-wise analytic stratification, Whitney fibering conjecture and Zariski equisingularity
- CAD and topology of semi-algebraic sets
- Computer Algebra of Polynomials and Rational Functions
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Explicit factors of some iterated resultants and discriminants
- Improved projection for cylindrical algebraic decomposition
- Iterated discriminants
- On delineability of varieties in CAD-based quantifier elimination with two equational constraints
- On propagation of equational constraints in CAD-based quantifier elimination
- On the Piano Movers problem. II: General techniques for computing topological properties of real algebraic manifolds
- On the Ramification of Algebraic Functions
- On using Lazard's projection in CAD construction
- On using bi-equational constraints in CAD construction
- Partial cylindrical algebraic decomposition for quantifier elimination
- Simulation and optimization by quantifier elimination
- Studies in Equisingularity I Equivalent Singularities of Plane Algebroid Curves
- Studies in Equisingularity II. Equisingularity in Codimension 1 (and Characteristic Zero)
- Testing stability by quantifier elimination
- The Abhyankar-Jung theorem
- Truth table invariant cylindrical algebraic decomposition
Cited in
(13)- Cylindrical algebraic decomposition with equational constraints
- Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
- Levelwise construction of a single cylindrical algebraic cell
- On using Lazard's projection in CAD construction
- Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Computing and using minimal polynomials
- Variable ordering selection for cylindrical algebraic decomposition with artificial neural networks
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- What does ``without loss of generality mean, and how do we detect it
- Proving an execution of an algorithm correct?
- Lazard-style CAD and Equational Constraints
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)
