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

1. Entering the quantified input formula
2. The normalization phase
3. The projection phase
4. The stack constuction (or lifting) phase
5. Solution formula construction

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
  (E x)[ x = _root_3 x^3 + a x^2 + b x + c /\ x > c ]. to express that there exist at least three distinct roots of the polynomial x³ + a x² + b x + c and that the third root (smallest to largest) is greater than c, the polynomials's trailing coefficient. QEPCAD accepts input and produces output in this extended language.