Sun Jan 11 22:52:29 MET 1998 anne % axiom Axiom Computer Algebra System (Release 2.1) Digital Unix on DEC Alpha (AXIOM Sockets) The AXIOM server number is undefined. ----------------------------------------------------------------------------- Issue )copyright to view copyright notices. Issue )summary for a summary of useful system commands. Issue )quit to leave AXIOM and return to shell. ----------------------------------------------------------------------------- initial (1) -> -- ----------[ A x i o m ]---------- -- ---------- Initialization ---------- )set messages autoload off )set messages time on )set quit unprotected -- ---------- Boolean Logic and Quantifier Elimination ---------- -- Simplify logical expressions => false true and false (1) false Type: Boolean Time: 0.03 (OT) + 0.02 (GC) = 0.05 sec -- => true x or (not x) Argument number 1 to "or" must be a Boolean. x : Boolean Type: Void Time: 0 sec x or (not x) x is declared as being in Boolean but has not been given a value. -- => x or y y : Boolean Type: Void Time: 0 sec x or y or (x and y) x is declared as being in Boolean but has not been given a value. -- => x xor(xor(x, y), y) x is declared as being in Boolean but has not been given a value. -- => [not (w and x)] or (y and z) w : Boolean Type: Void Time: 0 sec z : Boolean Type: Void Time: 0 sec implies(w and x, y and z) w is declared as being in Boolean but has not been given a value. -- => (x and y) or [not (x or y)] --x iff y -- => false x and 1 > 2 x is declared as being in Boolean but has not been given a value. )clear properties w x y z -- Quantifier elimination: See Richard Liska and Stanly Steinberg, ``Using -- Computer Algebra to Test Stability'', draft of September 25, 1995, and -- Hoon Hong, Richard Liska and Stanly Steinberg, ``Testing Stability by -- Quantifier Elimination'', _Journal of Symbolic Computation_, Volume 24, -- 1997, 161--187. -- => (a > 0 and b > 0 and c > 0) or (a < 0 and b < 0 and c < 0) -- [Hong, Liska and Steinberg, p. 169] --forAll y in C {implies(a*y**2 + b*y + c = 0, real(y) < 0)} -- => v > 1 [Liska and Steinberg, p. 24] --thereExists w in R suchThat _ --{v > 0 and w > 0 and -5*v**2 - 13*v + v*w - w > 0} -- => a^2 <= 1/2 [Hoon, Liska and Steinberg, p. 174] --forAll c in R _ --{implies(-1 <= c <= 1, a**2*(-c**4 - 2*c**3 + 2*c + 1) + c**2 + 2*c + 1 <= 4)} -- => v > 0 and w > |W| [Liska and Steinberg, p. 22] --forAll y in C _ --{implies(v > 0 and y**4 + 4*v*w*y**3 + 2*(2*v**2*w**2 + w**2 + W**2)*y**2 _ -- + 4*v*w*(w**2 - W**2) _ -- + (w**2 - W**2)**2 = 0, real(y) < 0)} -- This quantifier free problem was derived from the above example by QEPCAD -- => v > 0 and w > |W| [Liska and Steinberg, p. 22] v > 0 and 4*w*v > 0 and 4*w*(4*w**2*v**2 + 3*W**2 + w**2) > 0 _ and 64*w**2*v**2*(w**2 - W**2)*(w**2*v**2 + W**2) > 0 _ and 64*w**2*v**2*(w**2 - W**2)**3*(w**2*v**2 + W**2) > 0 (6) true Type: Boolean Time: 0.40 (IN) + 0.05 (EV) + 0.08 (OT) + 0.03 (GC) = 0.57 sec -- => B < 0 and a b > 0 [Liska and Steinberg, p. 49 (equation 86)] --thereExists y in C, thereExists n in C, thereExists e in R suchThat _ --{real(y) > 0 and real(n) < 0 and y + A*%i*e - B*n = 0 and a*n + b = 0} -- ---------- Quit ---------- )quit real 3.1 user 1.4 sys 0.2