# zbMATH — the first resource for mathematics

QEPCAD B: A program for computing with semi-algebraic sets using CADs. (English) Zbl 1083.68148
Cylindrical Algebraic Decomposition (CAD) is a method for quantifier elimination developed by George Collins [“Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition”, Lect. Notes Comput. Sci. 33, 134–183 (1975; Zbl 0318.02051)]. Qepcad b is a development of the Qepcad [G. E. Collins and H. Hong, “Partial cylindrical algebraic decomposition for quantifier elimination”, J. Symb. Comput. 12, No. 3, 299–328 (1991; Zbl 0754.68063)] implementation by Hoon Hong and is available at http://www.cs.usna.edu/~qepcad. It is a command-line program written mainly in C and based on the Saclib library of computer algebra functions.
Quantifiers ($$\exists, \forall$$) are eliminated by constructing a CAD representing a semi-algebraic set, applying the projection implied by the quantifiers to give a new CAD, and then reconstructing a formula representation. CADs can also be used for other purposes, which is one of the goals of Qepcad b. Qepcad b uses the projections due to McCallum [C. W. Brown, “Improved projection for cylindrical algebraic decomposition”, J. Symb. Comput. 32, No. 5, 447–465 (2001; Zbl 0981.68186); S. McCallum, “An improved projection operator for cylindrical algebraic decomposition”, in: Quantifier elimination and cylindrical algebraic decomposition, 242–268 (1998; Zbl 0906.03033)] if possible and it uses interval arithmetic [G. E. Collins, J. R. Johnson and W. Krandick, “Interval arithmetic in cylindrical algebraic decomposition”, J. Symb. Comput. 34, No. 2, 145–157 (2002; Zbl 1007.68210)] in the lifting phase. It always produces a formula (provided McCallum’s projection succeeds).
Given a quantifier-free input formula, Qepcad b attempts to produce a “simpler” equivalent (in some sense), which can be subject to specified assumptions. A very large formula can be simplified recursively by a program called SLFQ that applies Qepcad b. Qepcad b can produce topologically correct plots of 2-dimensional CADs (as EPS files). Constructing CADs from Tarski formulas is inefficient and Qepcad b allows more direct input via an extension of Tarski formulas involving equality and inequality symbols applied to roots of polynomials. Qepcad b allows additional quantifiers such as “exist exactly $$k$$”, “exist infinitely many” and “for all but finitely many”, which aid efficiency by avoiding the need to introduce extra variables or perform unnecessary tests.

##### MSC:
 68W30 Symbolic computation and algebraic computation 14P10 Semialgebraic sets and related spaces 03C10 Quantifier elimination, model completeness, and related topics