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 (email@example.com) 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"
(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: