Q E P C A D - The Solution Formula Construction Phase

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 simply type 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 solution-extension 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 (ETF) solution formula for a CAD-with-truth-values using just the polynomials in the projection factor set.

The Basic Options The 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:
Enter the number of free variables:
Enter a prenex formula:
(Ey)[ x^2 + y^2 - 3 = 0 /\ x + y > 0 ].

Before Normalization >

Before Projection (y) >

Before Choice >

Before Solution >
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

The example to the left shows the various options in use on a simple example of an input that produces a CAD of 1-space that is not projection definable. I left out the "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.

Christopher W Brown
Last modified: Tue Mar 13 13:28:09 EDT 2007