# Q E P C A D - The Positive-Definite Quartic Problem

```valiant[16] [~/]> qepcad
=======================================================
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 ']':
[ The positive-definite quartic problem ]
Enter a variable list:
(a,b,c,d,x)
Enter the number of free variables:
4
Enter a prenex formula:
(Ax)[ x^4 + a x^3 + b x^2 + c x + d > 0 ].

=======================================================

Before Normalization >
go

Before Projection (x) >
go

Before Choice >
go

Before Solution >
pdq

Before Solution >
sol E

An equivalent quantifier-free formula:

d > _root_1 256 d^3 - 192 a c d^2 - 128 b^2 d^2 + 144
a^2 b d^2 - 27 a^4 d^2 + 144 b c^2 d - 6 a^2 c^2 d -
80 a b^2 c d + 18 a^3 b c d + 16 b^4 d - 4 a^2 b^3 d -
27 c^4 + 18 a b c^3 - 4 a^3 c^3 - 4 b^3 c^2 + a^2 b^2
c^2 /\ [ 108 c^2 - 108 a b c + 27 a^3 c + 32 b^3 - 9 a^2
b^2 > 0 \/ d > _root_-1 256 d^3 - 192 a c d^2 - 128 b^2
d^2 + 144 a^2 b d^2 - 27 a^4 d^2 + 144 b c^2 d - 6 a^2
c^2 d - 80 a b^2 c d + 18 a^3 b c d + 16 b^4 d - 4 a^2
b^3 d - 27 c^4 + 18 a b c^3 - 4 a^3 c^3 - 4 b^3 c^2 +
a^2 b^2 c^2 ]

Before Solution >
sol T
An equivalent quantifier-free formula:

256 d^3 - 192 a c d^2 - 128 b^2 d^2 + 144 a^2 b d^2 -
27 a^4 d^2 + 144 b c^2 d - 6 a^2 c^2 d - 80 a b^2 c d +
18 a^3 b c d + 16 b^4 d - 4 a^2 b^3 d - 27 c^4 + 18 a b
c^3 - 4 a^3 c^3 - 4 b^3 c^2 + a^2 b^2 c^2 >= 0 /\ [ [
108 c^2 - 108 a b c + 27 a^3 c + 32 b^3 - 9 a^2 b^2 > 0
/\ 384 d^2 - 192 a c d - 128 b^2 d + 144 a^2 b d - 27
a^4 d + 72 b c^2 - 3 a^2 c^2 - 40 a b^2 c + 9 a^3 b c +
8 b^4 - 2 a^2 b^3 <= 0 ] \/ [ 256 d^3 - 192 a c d^2 -
128 b^2 d^2 + 144 a^2 b d^2 - 27 a^4 d^2 + 144 b c^2 d -
6 a^2 c^2 d - 80 a b^2 c d + 18 a^3 b c d + 16 b^4 d -
4 a^2 b^3 d - 27 c^4 + 18 a b c^3 - 4 a^3 c^3 - 4 b^3
c^2 + a^2 b^2 c^2 > 0 /\ 384 d^2 - 192 a c d - 128 b^2
d + 144 a^2 b d - 27 a^4 d + 72 b c^2 - 3 a^2 c^2 - 40 a
b^2 c + 9 a^3 b c + 8 b^4 - 2 a^2 b^3 >= 0 /\ 768 d - 192
a c - 128 b^2 + 144 a^2 b - 27 a^4 >= 0 ] \/ [ 108 c^2 -
108 a b c + 27 a^3 c + 32 b^3 - 9 a^2 b^2 >= 0 /\ 256
d^3 - 192 a c d^2 - 128 b^2 d^2 + 144 a^2 b d^2 - 27 a^4
d^2 + 144 b c^2 d - 6 a^2 c^2 d - 80 a b^2 c d + 18 a^3 b
c d + 16 b^4 d - 4 a^2 b^3 d - 27 c^4 + 18 a b c^3 - 4 a^3
c^3 - 4 b^3 c^2 + a^2 b^2 c^2 > 0 ] ]

Before Solution >
quit
valiant[17] [~/]>
```

This is a classic quantifier elimination benchmark problem. It asks for a characterization of all monic polynomials in x of degree 4 that are positive for all x values. As a Q.E. problem, this is: `(Ax)[ x^4 + a x^3 + b x^2 + c x + d > 0 ]`. One interesting thing about this problem is that when the McCallum Projection is used, the resulting CAD is not projection definable, meaning that a solution formula in the usual sense (Tarski Formula) cannot be constructed using only those polynomials appearing in the projection factor set. Since the only polynomials we know anything about are those in the projection factor set, this is a problem. There are two solutions.

1. Expand the language in which solution formulas may be expressed.
2. Add polynomials to the projection factor set.
Both of these are available with the `solution-extension` command. For a formula in an expanded language give:
```solution-extension E
```
The extended language includes references to "indexed roots" of polynomial. The expression "_root_k P(x)" means the |k|th root (not counting multiplicities) of P(x) counting left-to-right if k > 0 and right-to-left if k < 0. (more on the extended language) If you really want a solution in the language of Taski Formulas, give the command:
```solution-extension T
```
This will add polynomials to the projection factor set (which may be an expensive operation!) and construct a solution formula as soon as it is able.

The command `pdq`, for "projection definability query" will tell you if the CAD of free-variable space is projection definable.

Christopher W Brown