When the stack construction phase is complete, QEPCAD has a CAD of
free-variable space with truth values attached to each cell. This
represents the solution set of the (possibly quantified) input
formula. The last step is to represent this set as a formula (a
solution formula), and
one of the big advantages of quantifier elimination by CAD is its
ability to produce simple solution formula. If you
go at the "
Before Solution >"
prompt, QEPCAD will automatically construct a (hopefully) simple
solution formula in the language of Tarski formulas. However,
more options are available with the
command. To understand these options a bit better it's good to
know a little bit about how solution formulas are constructed.
QEPCAD constructs solution formulas from the polynomials in the
projection factor set defining the CAD of free-variable space.
It is not always possible to construct a Tarski formula solely
from these polynomials, in which case we must add polynomials to
the projection factor set.
A CAD-with-truth-values for which a Tarski solution formula can
be built exclusively from the elements of the projection factor
set is called projection definable.
The command "
pdq", which stands for projection
definability query, allows the user to ask QEPCAD whether the
CAD in the solution formula construction phase is projection
definable. It is, however, always possible
to construct an Extended Tarski
formula for a CAD-with-truth-values using just the polynomials
in the projection factor set.
The Basic Options
solution-extension command takes a letter as an
arguments that provides several different possibilities for
solution formula construction.
Enter an informal description between '[' and ']': [Produces a CAD that's not projection definable ] Enter a variable list: (x,y) Enter the number of free variables: 1 Enter a prenex formula: (Ey)[ x^2 + y^2 - 3 = 0 /\ x + y > 0 ]. ======================================================= Before Normalization > go Before Projection (y) > go Before Choice > go Before Solution > pdq CAD is not projection definable. Before Solution > solution-extension T An equivalent quantifier-free formula: x^2 - 3 <= 0 /\ [ x >= 0 \/ 2 x^2 - 3 < 0 ] Before Solution > solution-extension E An equivalent quantifier-free formula: x^2 - 3 <= 0 /\ x > _root_1 2 x^2 - 3
solution-extension TThis option produces a formula in the language of Tarski formulas, and in fact this exactly the routine that gets called if you simply type "
go" at the "
Before Solution >" prompt, or "
finish" at any point. If the CAD is not projection definable, polynomials will be added to the projection factor set.
solution-extension EThis option produces a formula in the language of Extended Tarski Formulas (ETFs). Projection factors are never added to the projection factor set.
solution-extension GThis option tries to produce a formula that gives insight into the geometry of the solution set. The method of doing so, and the properties of the formulas that the method produces are described in Chapter 8 of my thesis. Generally the formula will be an ETF rather than a Tarski formula. The basic idea is that the set gets described in diskoint pieces.
solution-extension FThis option produces a formula based purely ono the full-dimensional cells in free variable space. This means that the truth values of lower dimensional cells are ignored.
solution-extension IThis option enters the user into an "interactive" mode, which gives him more control over how solution formulas are constructed.
G" option, because it really isn't interesting for CAD's of 1-space - it needs at least 2-levels to do anything fun. You see in this example that the polynomial x only appears in the formula produced by "
soltution-extension T". That polynomial is not in the projection factor set, and was actually added after the fact by QEPCAD in order to make it possible to construct a solution formula in the language of Tarski formulas.