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                 
            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 ']':
[ Finds x-coordinates of circle-line intersections ]
Enter a variable list:
Enter the number of free variables:
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:

Thus, "there exists an x such that for all y ..." would be written as (E x)(A y). The quantifier-free part of the input must appear in brackets, and throughout the formula brackets are used for groupings of formulas, and parentheses are used for algebraic expressions. The boolean operators are: /\ , \/ , ~ , ==> , <== , <==>. The relational operators are: = , /= , < , > , <= , >=. Hopefully these are all self explanatory. Qepcad doesn't understand precedence for boolean operators, so you must use brackets to remove ambiguity. Atomic formulas can be equalities or inequalities of polynomials in the variables you've entered with rational coefficients, or they may proper indexed root expressions - please see Extended Tarski Formulas for more information. Finally, the input formula must be terminated by a period.

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.

Christopher W Brown
Last modified: Tue Jul 30 17:02:57 EDT 2002