×

Real quantifier elimination in practice. (English) Zbl 0934.68130

Matzat, B. Heinrich (ed.) et al., Algorithmic algebra and number theory. Selected papers from a conference, Heidelberg, Germany, October 1997. Berlin: Springer. 221-247 (1999).
An interesting problem of quantifier elimination is defined in first order logic as follows: Given a formula \(\varphi\), find a quantifier-free formula \(\varphi'\) such that both \(\varphi\) and \(\varphi'\) are equivalent in the domain of real numbers. This paper surveys the following implemented real quantifier elimination methods: partial cylindrical algebraic decomposition, virtual substitution of test terms, and combination of Gröbner basis computations with multivariate root counting. The survey starts with Descartes’ rule of signs and evolves into implementations in the available packages QEPCAD, QERRC, and especially REDLOG. The applications discussed are in constraint solving, optimization, scheduling, simulation, sizing, and diagnosis, control theory and stability, real implicitization, automatic theorem proving, computer aided design, computer vision, and solid modeling, collision detection and path finding. The examples used for illustration are all quadratic. None of the surveyed methods is universally superior to the others and it may take a combination of all three to solve particular problems.
For the entire collection see [Zbl 0903.00035].

MSC:

68W30 Symbolic computation and algebraic computation
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
13-04 Software, source code, etc. for problems pertaining to commutative algebra

Software:

QERRC; QEPCAD; REDLOG
PDFBibTeX XMLCite