# Q E P C A D - Basic User Information

```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`". If you attempt a problem and get a failure message that QEPCAD/SACLIB ran out of memory, try upping the space with "+N".

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`".

These five steps (or fewer if you choose to ignore them with a "`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.
`(E x)[ x = _root_3 x^3 + a x^2 + b x + c /\ x > c ].`