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:
(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 T This 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 E This option produces a formula in the language of Extended Tarski Formulas (ETFs). Projection factors are never added to the projection factor set.
• solution-extension G This 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 F This 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 I This option enters the user into an "interactive" mode, which gives him more control over how solution formulas are constructed.