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"`X`

*k*= "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,
**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:

- The fewer variables the better! Use the extended language if you can as an alternative to introducing new variables.
- 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. - 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!
- Split formulas up into small independent pieces if possible!
- 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