Mon Feb 16 11:21:48 MST 1998 aquarius% mupad *----* MuPAD 1.4.0 -- Multi Processing Algebra Data Tool /| /| *----* | Copyright (c) 1997 - 98 by SciFace Software GmbH | *--|-* All rights reserved. |/ |/ *----* Licensed to: Michael Wester >> # ----------[ M u P A D ]---------- # >> # ---------- Initialization ---------- # >> TEXTWIDTH:= 80: >> read("../../Time.mupad"): >> # ---------- Boolean Logic and Quantifier Elimination ---------- # >> # Simplify logical expressions => false # >> TRUE and FALSE; FALSE Time: 80 msec Type: DOM_BOOL >> # => true # >> x or (not x); TRUE Time: 60 msec Type: DOM_BOOL >> # => x or y # >> x or y or (x and y); x or y or x and y Time: 60 msec Type: "_or" >> simplify(%, logic); x or y Time: 1250 msec Type: "_or" >> # => x # >> #x xor y xor y;# >> # => [not (w and x)] or (y and z) # >> #(w and x) implies (y and z);# >> # => (x and y) or [not (x or y)] # >> #x iff y;# >> # => false # >> x and 1 > 2; x and 2 < 1 Time: 130 msec Type: "_and" >> simplify(%, logic); FALSE Time: 210 msec Type: DOM_BOOL >> # 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 {a*y^2 + b*y + c = 0 implies Re(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 &> {-1 <= c <= 1 implies 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 &> {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 implies Re(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; 2 2 2 2 0 < v and 0 < 4 v w and 0 < 4 w (3 W + w + 4 v w ) and 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 0 < 64 v w (w - W ) (W + v w ) and 0 < 64 v w (w - W ) (W + v w ) Time: 190 msec Type: "_and" >> simplify(%, logic); 3 2 2 3 0 < v and 0 < 4 v w and 0 < 4 w + 12 W w + 16 v w and 4 6 2 2 4 4 2 2 2 4 4 4 10 0 < 64 v w + 64 W v w - 64 W v w - 64 W v w and 0 < 64 v w + 2 2 8 4 2 6 6 2 4 8 2 2 2 4 8 64 W v w - 192 W v w + 192 W v w - 64 W v w - 192 W v w + 4 4 6 6 4 4 192 W v w - 64 W v w Time: 620 msec Type: "_and" >> # => 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 &> {Re(y) > 0 and Re(n) < 0 and y + A*I*e - B*n = 0 and a*n + b = 0};# >> # ---------- Quit ---------- # >> quit real 6.04 user 4.43 sys 0.59