QEPCAD B: A program for computing with semi-algebraic sets using CADs. (English) Zbl 1083.68148

Brown, Christopher W.

SIGSAM Bull. 37, No. 4, 97-108 (2003).

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.

Reviewer: Francis John Wright (London)

MSC:

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

Keywords:

algebraic simplification; quantifier elimination; cylindrical algebraic decomposition

Citations:

Zbl 0318.02051; Zbl 0754.68063; Zbl 0981.68186; Zbl 0900.68279; Zbl 0906.03033; Zbl 1007.68210

Software:

SACLIB; REDLOG; QEPCAD