Q E P C A D - Basic User Information

prompt% qepcad
                Quantifier Elimination                 
            Elementary Algebra and Geometry            
      Partial Cylindrical Algebraic Decomposition      
               Version B 0.1, 30 Jul 2002
                       Hoon Hong                       
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:
Enter the number of free variables:
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 >
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 ]


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

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