Sun Jan 11 14:45:06 MST 1998 euler% math Mathematica 3.0 for Solaris Copyright 1988-96 Wolfram Research, Inc. -- Terminal graphics initialized -- In[1]:= In[2]:= In[3]:= (* ----------[ M a t h e m a t i c a ]---------- *) 0. Second In[4]:= (* ---------- Initialization ---------- *) 0. Second In[5]:= (* ---------- Boolean Logic and Quantifier Elimination ---------- *) 0. Second In[6]:= (* Simplify logical expressions => false *) 0. Second In[7]:= True && False 0. Second Out[7]= False In[8]:= (* => true *) 0. Second In[9]:= x || (! x) 0. Second Out[9]= x || !x In[10]:= LogicalExpand[%] 0. Second Out[10]= True In[11]:= (* => x or y *) 0. Second In[12]:= x || y || (x && y) 0. Second Out[12]= x || y || x && y In[13]:= LogicalExpand[%] 0. Second Out[13]= x || y In[14]:= (* => x *) 0. Second In[15]:= Xor[Xor[x, y], y] 0. Second Out[15]= Xor[x, y, y] In[16]:= LogicalExpand[%] 0. Second Out[16]= x In[17]:= (* => [not (w and x)] or (y and z) *) 0. Second In[18]:= Implies[w && x, y && z] 0. Second Out[18]= Implies[w && x, y && z] In[19]:= LogicalExpand[%] 0. Second Out[19]= y && z || !w || !x In[20]:= (* => (x and y) or [not (x or y)] *) 0. Second In[21]:= (*Iff[x, y] LogicalExpand[%]*) 0. Second In[22]:= (* => false *) 0. Second In[23]:= x && 1 > 2 0. Second Out[23]= False In[24]:= (* 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. *) 0. Second In[25]:= (* => (a > 0 and b > 0 and c > 0) or (a < 0 and b < 0 and c < 0) [Hong, Liska and Steinberg, p. 169] *) 0. Second In[26]:= (*forAll y in C {Implies[a*y^2 + b*y + c == 0, Re[y] < 0]}*) 0. Second In[27]:= (* => v > 1 [Liska and Steinberg, p. 24] *) 0. Second In[28]:= (*thereExists w in R suchThat {v > 0 and w > 0 and -5*v^2 - 13*v + v*w - w > 0}*) 0. Second In[29]:= (* => a^2 <= 1/2 [Hoon, Liska and Steinberg, p. 174] *) 0. Second In[30]:= (*forAll c in R {Implies[-1 <= c <= 1, a^2*(-c^4 - 2*c^3 + 2*c + 1) + c^2 + 2*c + 1 <=\ > 4]}*) 0. Second In[31]:= (* => v > 0 and w > |W| [Liska and Steinberg, p. 22] *) 0. Second In[32]:= (*forAll y in C {Implies[v > 0 && 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, Re[y] < 0]}*) 0. Second In[33]:= (* This quantifier free problem was derived from the above example\ > by QEPCAD => v > 0 and w > |W| [Liska and Steinberg, p. 22] *) 0. Second In[34]:= (v > 0 && 4*w*v > 0 && 4*w*(4*w^2*v^2 + 3*W^2 + w^2) > 0 && 64*w^2*v^2*(w^2 - W^2)*(w^2*v^2 + W^2) > 0 && 64*w^2*v^2*(w^2 - W^2)^3*(w^2*v^2 + W^2) > 0) 0. Second 2 2 2 2 Out[34]= v > 0 && 4 v w > 0 && 4 w (w + 4 v w + 3 W ) > 0 && 2 2 2 2 2 2 2 > 64 v w (w - W ) (v w + W ) > 0 && 2 2 2 2 3 2 2 2 > 64 v w (w - W ) (v w + W ) > 0 In[35]:= LogicalExpand[%] 0. Second 2 2 2 2 2 2 2 Out[35]= v > 0 && 4 v w > 0 && 64 v w (w - W ) (v w + W ) > 0 && 2 2 2 2 3 2 2 2 2 2 2 2 > 64 v w (w - W ) (v w + W ) > 0 && 4 w (w + 4 v w + 3 W ) > 0 In[36]:= (* => B < 0 and a b > 0 [Liska and Steinberg, p. 49 (equation 86)]\ > *) 0. Second In[37]:= (*thereExists y in C, thereExists n in C, thereExists e in R suchThat {Re[y] > 0 && Re[n] < 0 && y + A*I*e - B*n == 0 && a*n + b == 0}*) 0. Second In[38]:= (* ---------- Quit ---------- *) 0. Second In[39]:= Quit[] real 2.60 user 0.76 sys 0.46