Q E P C A D - Entering Formulas

---

Entering formulas in QEPCAD requires a little bit of thought. There are some decisions to made that can have a considerable impact on the time required for your problem.

=======================================================
                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 ']':
[ Finds x-coordinates of circle-line intersections ]
Enter a variable list:
(x,y)
Enter the number of free variables:
1
Enter a prenex formula:
(Ey)[ x^2 + y^2 = 1 /\ 3 x - 5 y + 1 = 0 ].

General Information QEPCAD fist asks for a problem description, which is really quite nice if you store a list of commands in a file that then gets sent to QEPCAD by indirection. Next you need to specify the variables that you use. Ordering of variables is very important in quantifier elimination by CAD, and the variable list you give specifies not only the variables themselves, but also their ordering. Free variables must appear before quantified variables, and the quantified variables must appear in the same order in which they will appear in the prenex input formula (which is entered later). Be forewarned that different variable orderings often produce wildly different running times! Finally, you must tell QEPCAD how many variables are free in the problem. If you enter k for this value, then QEPCAD assumes that the first k variables in the given variable list are free.

The Formula The formula you enter must be in prenex form. Each quantified variable is introduced in parentheses by the quantifier followed by the variable name. Quantifiers are:

• E = "there exists"
• A = "for all"
• F = "for infinitely many"
• G = "for all but finitely many"
• C = "for a connected subset"
• Xk = "for exactly k distinct values"

Phrasing Problems in the Best Way for QEPCAD You can affect QEPCAD's performance quite drastically by how you happen to translate a problem into an input formula. Here are a few things to keep in mind:

1. The fewer variables the better! Use the extended language if you can as an alternative to introducing new variables.
2. Keep degrees low if possible! For example, if a variable x always appears to an even power in a formula, replace x with sqrt(x) and add the restriction x >= 0 to the formula.
3. If you can use the quantifiers F = "for infintely many" or G = "for all but finitely many" in place of E = "there exists" and A = "for all", definitely do it!! QEPCAD can get rid of some algebraic number computations this way, and that can make a huge difference!
4. Split formulas up into small independent pieces if possible!
5. If you can eliminate some variables on your own, do it! Remember, the fewer variables QEPCAD sees the better.