**Simplifying Quantifier-free Formulas with QEPCAD**

[ [s z + s - 1 >= 0 /\ s = 0 /\ z + 1 >= 0] \/ [s z + s >= 0 /\ s = 0 /\ z = 0] \/ [s^2 + 4 s z >= 0 /\ [[ s^2 - 2 s <= 0 /\ s z + s - 1 <= 0 /\ s = 0 /\ [ s^2 + 3 s z - s - 2 z <= 0 \/ [s + z - 1 <= 0 /\ [s z + s - 1 = 0 \/ z = 0]]] /\ [s + 2 z >= 0 \/ z = 0]] \/ [s^2 - 2 s <= 0 /\ s + 2 z >= 0 /\ s = 0 /\ [ [s^2 + 3 s z - s - 2 z <= 0 /\ [s z + s - 1 <= 0 \/ z = 0]] \/ [s + z - 1 >= 0 /\ [s z + s - 1 >= 0 \/ z = 0]]]]]] \/ [s = 0 /\ z >= 0] ].This formula is already quantifier-free, but we might try using QEPCAD anyway to see if it can simplify the formula. In this case, it simplifies it to

`s = 0 /\ z >= 0`

. Here's
what the QEPCAD session looks like:
======================================================= 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 ']': [ Anai's Problem ] Enter a variable list: (s,z) Enter the number of free variables: 2 Enter a prenex formula: [ [s z + s - 1 >= 0 /\ s = 0 /\ z + 1 >= 0] \/ [s z + s >= 0 /\ s = 0 /\ z = 0] \/ [s^2 + 4 s z >= 0 /\ [[ s^2 - 2 s <= 0 /\ s z + s - 1 <= 0 /\ s = 0 /\ [ s^2 + 3 s z - s - 2 z <= 0 \/ [s + z - 1 <= 0 /\ [s z + s - 1 = 0 \/ z = 0]]] /\ [s + 2 z >= 0 \/ z = 0]] \/ [s^2 - 2 s <= 0 /\ s + 2 z >= 0 /\ s = 0 /\ [ [s^2 + 3 s z - s - 2 z <= 0 /\ [s z + s - 1 <= 0 \/ z = 0]] \/ [s + z - 1 >= 0 /\ [s z + s - 1 >= 0 \/ z = 0]]]]]] \/ [s = 0 /\ z >= 0] ]. ======================================================= Before Normalization > finish An equivalent quantifier-free formula: s = 0 /\ z >= 0 ==========================================

Christopher W Brown Last modified: Tue Jul 30 17:04:20 EDT 2002