prompt% qepcad ======================================================= Quantifier Elimination in Elementary Algebra and Geometry by Partial Cylindrical Algebraic Decomposition Version B 0.1, 30 Jul 2002 by Hoon Hong (hhong@math.ncsu.edu) With contributions by: Christopher W. Brown, George E. Collins, Mark J. Encarnacion, Jeremy R. Johnson Werner Krandick, Richard Liska, Scott McCallum, Nicolas Robiduex, and Stanly Steinberg ======================================================= Enter an informal description between '[' and ']': [ This is the ever-popular "X Axis Ellipse" problem ] Enter a variable list: (a,b,c,x,y) Enter the number of free variables: 3 Enter a prenex formula: (A x)(A y)[ a > 0 /\ b > 0 /\ [ [ b^2 (x - c)^2 + a^2 y^2 - a^2 b^2 = 0] ==> x^2 + y^2 - 1 <= 0 ] ]. ======================================================= Before Normalization > finish An equivalent quantifier-free formula: a > 0 /\ b > 0 /\ c - a + 1 >= 0 /\ c + a - 1 <= 0 /\ [ b^2 - a <= 0 \/ b^2 c^2 + b^4 - a^2 b^2 - b^2 + a^2 <= 0 ] ======================================================= prompt%

**Starting QEPCAD**
QEPCAD is a command-line program, so you launch it at the command
prompt. Assuming that the *qe* environment variable in
your shell has been set to the root directory of your QEPCAD
installation (*Example: * `setenv qe ${HOME}/qesource`

)
you run QEPCAD with the command "** $qe/bin/qepcad**".
A somewhat unfortunate feature of the SACLIB library on which
QEPCAD is based is that it initializes itself with a fixed-size
piece of memory and simply fails if that gets filled up. A larger
size piece of memory can be requested with the command-line
argument

**+N**

. The "+N" is followed by a number
- the number of cells in the garbage collected space. the default
value is 2000000. So to run QEPCAD with more memory you might
give the command "`$qe/bin/qepcad +N8000000`

**Basic Quantifier Elimination with QEPCAD**
QEPCAD is an inherently iteractive program, and I will describe it
as such. There are five basic steps in a QEPCAD session, though
all but the first may be by-passed by the user simply by typing
"`finish`

".

**Entering the quantified input formula****The normalization phase****The projection phase****The stack constuction (or lifting) phase****Solution formula construction**

`finish`

" command) are enough to use QEPCAD to naively
solve quantifier-elimination problems. Please follow the above
links to the documentation on the individual steps to see how to
use QEPCAD less naively and more effetively.
**Beyond Basic Quantifier Elimination**
Basic quantifier elimination takes a quantified Tarski formula
as input and produces a quantifier-free Tarski formula as
output. QEPCAD does more than just this, however, and using its
other capabilities often allows you to solve problems more
efficiently.

**Simplification of Quantifier-free Formulas**. One of QEPCAD's most important features is its ability to produce simple quantifier-free equivalent formulas (see the above link for Solution formula construction). However, QEPCAD produces simple equivalent formulas even when the input formula is already quantifier-free. Thus, QEPCAD can be used to do formula simplification ... perhaps for formulas that generated by other quantifier elimination programs. For very large formulas, repeated applications of QEPCAD for simplification of subformulas may succeed when applying QEPCAD directly to the entire formula fails. I have some software for this, so please e-mail me if you're interested.**Beyond "there exists" and "for all"**. Cylindrical Algebraic Decomposition (CAD) is essentially nothing more than a representation for*semi-algebraic sets*, which are precisely the sets that can be defined by Tarski formulas. Their importance for quantifier elimination lies in the fact that the projections implied by "there exists" and "for all" are trivial to carry out with the CAD representation. However, there are many other "quantifiers" that can be carried out just as easily with CADs, and QEPCAD offers several (see the above link for Entering the quantified input formula). Using these quantifiers in phrasing problems can drastically decrease the number of variables needed, which in turn can reduce computing time.**Plotting 2-dimensional CADs**. QEPCAD can generate "adjacency information" for 2-dimensional CADs, which allows it to generate topologically correct plots.**More Information ...****Beyond Tarski Formulas**. Both the input formula and the solution formula in the quantifier elimination problem are assumed to be Tarski formulas, meaning that each atomic formula is an equality or inequality in the free and bound variables. QEPCAD is actually a quantifier elimination procedure for an extended language that includes "indexed root expressions". For example, we can use the input formula

to express that there exist at least three distinct roots of the polynomial`(E x)[ x = _root_3 x^3 + a x^2 + b x + c /\ x > c ].`

*x*and that the third root (smallest to largest) is greater than^{3}+ a x^{2}+ b x + c*c*, the polynomials's trailing coefficient. QEPCAD accepts input and produces output in this extended language.

Christopher W Brown Last modified: Wed Jul 31 15:07:09 EDT 2002