- 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
- This example uses formula simplification and the
assume command to discover and prove a theorem
- 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
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
- 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