Q E P C A D - The Normalization Phase

In the normalization the formula input by the user is put into a special form

all atomic formula f op g are put in the form f - g op 0
all polynomials appearing in atomic formula are factored, and when more than one factor is present the atomic formula is broken up into a boolean combination of several atomic formulas involving irreducible polynomials
etc.

From the user presepective this stuff is not all that interesting, and you'll probably just type go to get through this phase. There are, however, a few commands that can be given here, and some of them are described below.

New with Version 1.6, the user can input assumptions in the normalization phase. Assumptions take the form of a quantifier-free formula in the free variables, and QEPCAD will ignore any part of free-variable space that does not satisfy the assumptions. When a solution formula is produced, the formula will also make the same assumptions, meaning that a true solution formula is the conjunction of the assumptions and the formula output by QEPCAD. The main advantage to using assumptions is the solution formula will probably be easier to interpret, since QEPCAD doesn't try to "simplify" the assumptions, and you don't have to wade through the formula and figure out what parts of the formula simply echo your assumptions, and what parts are new results. Example:
```
assume [ a > 0 /\ b > 0 ]
```
The command name, as you can see, is assume, and the syntax for the formula itself is the same as for input formulas.
If you are going to use Equational Constraints (which requires some care, and which you at present do "at your own risk") you need to issue the "prop-eqn-const" command, which simply "enables" equational constraints. Information on Equational Constraints
One command that can be issued here (although it could as well be pushed back later) is "full-cad". This forces a full CAD of free-variable space to be constructed. (Note: if the "cell-choice-bound" command is used, the "full-cad" command has no effect.)

Christopher W Brown