Q E P C A D - Example Problems

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.