**Deciding Positive Semidefiniteness**-
This example comes from "An effective decision method for semidefinite polynomials",
Zeng Guangxing and Zeng Xiaoning,
*Journal of Symbolic Computation*37 (2004) pages 83-99. We show how to use the "there exist infintely many" quantifier to produce an efficient formulation of the positive semidefiniteness problem for QEPCAD. We then apply this approach to the final example from Guangxing and Xiaoning's paper. **Triangles**- This example uses formula simplification and the
`assume`

command to discover and prove a theorem about triangles. **A Problem Due to Anai**- This example shows QEPCAD being used to simplify a formula that is already quantifier-free.
**The Edge-Square Product Problem**- This example demonstrates using easy eliminations before calling QEPCAD, declaring an equational contraint, using topological information in 2D.
**The Positive Definite Quartic Problem**- This classic benchmark QE problem is interesting because with the McCallum Projection (which is now the default), QEPCAD constructs a CAD of free-variable space that is not projection definable.
**Hong-Liska-Steinberg 5.14**- This problem shows the twin benefits of using the "for all but finitely many" quantifier.

Christopher W Brown Last modified: Fri Feb 6 10:10:39 EST 2004