#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