#1: " ----------[ D e r i v e ]---------- " User
#2: " ---------- Initialization ---------- " User
User
#3: " ---------- Boolean Logic and Quantifier Elimination ----------
"
#4: " Simplify logical expressions => false " User
#5: true AND false User
#6: false Simp(#5)
#7: " => true " User
#8: x OR NOT x User
#9: true Simp(#8)
#10: " => x or y " User
#11: x OR y OR x AND y User
#12: x OR y Simp(#11)
#13: " => x " User
#14: x XOR y XOR y User
#15: x Simp(#14)
#16: " => [not (w and x)] or (y and z) " User
#17: w AND x IMP y AND z User
#18: NOT x OR y AND z OR NOT w Simp(#17)
#19: " => (x and y) or [not (x or y)] " User
#20: "x iff y" User
#21: " => false " User
#22: x AND 1 > 2 User
#23: false Simp(#22)
User
#24: " Quantifier elimination: See Richard Liska and Stanly
Steinberg, ``Using "
User
#25: " Computer Algebra to Test Stability'', draft of September 25,
1995, and "
User
#26: " Hoon Hong, Richard Liska and Stanly Steinberg, ``Testing
Stability by "
User
#27: " Quantifier Elimination'', _Journal of Symbolic Computation_,
Volume 24, "
#28: " 1997, 161--187. " User
User
#29: " => (a > 0 and b > 0 and c > 0) or (a < 0 and b < 0 and c < 0)
"
#30: " [Hong, Liska and Steinberg, p. 169] " User
#31: "forAll y in C {a*y^2 + b*y + c = 0 IMP RE(y) < 0}" User
#32: " => v > 1 [Liska and Steinberg, p. 24] " User
#33: "thereExists w in R suchThat ~" User
#34: "{v > 0 AND w > 0 AND -5*v^2 - 13*v + v*w - w > 0}" User
#35: " => a^2 <= 1/2 [Hoon, Liska and Steinberg, p. 174] "User
#36: "forAll c in R ~" User
User
#37: "{-1 <= c <= 1 IMP a^2*(-c^4 - 2*c^3 + 2*c + 1) + c^2 + 2*c + 1
<= 4}"
#38: " => v > 0 and w > |W| [Liska and Steinberg, p. 22] "User
#39: "forAll y in C ~" User
User
#40: "{v > 0 AND y^4 + 4*v*w*y^3 + 2*(2*v^2*w^2 + w^2 + WW^2)*y^2 ~"
User
#41: " + 4*v*w*(w^2 - WW^2) + (w^2 - WW^2)^2 = 0 IMP RE(y) < 0}"
User
#42: " This quantifier free problem was derived from the above
example by QEPCAD"
#43: " => v > 0 and w > |W| [Liska and Steinberg, p. 22] "User
User
2 2 2 2
#44: v > 0 AND 4*w*v > 0 AND 4*w*(4*w *v + 3*ww + w ) > 0 AND
2 2 2 2 2 2 2 2 2 2
64*w *v *(w - ww )*(w *v + ww ) > 0 AND 64*w *v *(w -
2 3 2 2 2
ww ) *(w *v + ww ) > 0
Simp(#44)
2 2 2 2 2 2 2 2 2 2
#45: 4*w*(4*v *w + w + 3*ww ) > 0 AND 64*v *w *(w - ww )*(v *w +
2 2 2 2
ww ) > 0 AND 4*v*w > 0 AND v > 0 AND 64*v *w *(w -
2 3 2 2 2
ww ) *(v *w + ww ) > 0
User
#46: " => B < 0 and a b > 0 [Liska and Steinberg, p. 49 (equation
86)] "
User
#47: "thereExists y in C, thereExists n in C, thereExists e in R
suchThat ~"
User
#48: "{RE(y) > 0 AND RE(n) < 0 AND y + A*#i*e - B*n = 0 AND a*n + b =
0}"
#49: " ---------- Quit ---------- " User