Simplifying Quantifier-free Formulas with QEPCAD
This example problem comes from a paper by H. Anai in the on-line proceedings of IMACS-ACA 1998 (H. Anai, Solving LMI and BMI problems by quantifier elimination, Proc. of IMACS-ACA '98, Edited by R. Liska, http://www-troja.fjfi.cvut.cz/aca98/proceedings.html). In the last problem from that paper, he ends up with the following formula describing the solution to his problem:[ [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
==========================================