tests/wester_problems/test_boolean_logic.mac

   1 /* Original version of this file copyright 1999 by Michael Wester,
   2  * and retrieved from http://www.math.unm.edu/~wester/demos/BooleanLogic/problems.macsyma
   3  * circa 2006-10-23.
   4  *
   5  * Released under the terms of the GNU General Public License, version 2,
   6  * per message dated 2007-06-03 from Michael Wester to Robert Dodier
   7  * (contained in the file wester-gpl-permission-message.txt).
   8  *
   9  * See: "A Critique of the Mathematical Abilities of CA Systems"
  10  * by Michael Wester, pp 25--60 in
  11  * "Computer Algebra Systems: A Practical Guide", edited by Michael J. Wester
  12  * and published by John Wiley and Sons, Chichester, United Kingdom, 1999.
  13  */
  14 /* ----------[ M a c s y m a ]---------- */
  15 /* ---------- Initialization ---------- */
  16 showtime: all$
  17 prederror: false$
  18 /* ---------- Boolean Logic and Quantifier Elimination ---------- */
  19 /* Simplify logical expressions => false */
  20 true and false;
  21 /* => true */
  22 x or (not x);
  23 boolsimp(%);
  24 /* => x or y */
  25 x or y or (x and y);
  26 boolsimp(%);
  27 /* => x */
  28 logxor(logxor(x, y), y);
  29 /* => [not (w and x)] or (y and z) */
  30 /*(w and x) implies (y and z);*/
  31 /* => (x and y) or [not (x or y)] */
  32 /*x iff y;*/
  33 /* => false */
  34 x and 1 > 2;
  35 errcatch(boolsimp(%));
  36 /* Quantifier elimination: See Richard Liska and Stanly Steinberg, ``Using
  37    Computer Algebra to Test Stability'', draft of September 25, 1995, and
  38    Hoon Hong, Richard Liska and Stanly Steinberg, ``Testing Stability by
  39    Quantifier Elimination'', _Journal of Symbolic Computation_, Volume 24,
  40    1997, 161--187. */
  41 /* => (a > 0 and b > 0 and c > 0) or (a < 0 and b < 0 and c < 0)
  42       [Hong, Liska and Steinberg, p. 169] */
  43 /*forAll y in C {a*y^2 + b*y + c = 0 implies realpart(y) < 0}*/
  44 /* => v > 1   [Liska and Steinberg, p. 24] */
  45 /*thereExists w in R suchThat
  46   {v > 0 and w > 0 and -5*v^2 - 13*v + v*w - w > 0};*/
  47 /* => a^2 <= 1/2   [Hoon, Liska and Steinberg, p. 174] */
  48 /*forAll c in R
  49   {-1 <= c <= 1 implies a^2*(-c^4 - 2*c^3 + 2*c + 1) + c^2 + 2*c + 1 <= 4};*/
  50 /* => v > 0 and w > |W|   [Liska and Steinberg, p. 22] */
  51 /*forAll y in C
  52   {v > 0 and y^4 + 4*v*w*y^3 + 2*(2*v^2*w^2 + w^2 + WW^2)*y^2
  53      + 4*v*w*(w^2 - WW^2) + (w^2 - WW^2)^2 = 0 implies realpart(y) < 0};*/
  54 /* This quantifier free problem was derived from the above example by QEPCAD
  55    => v > 0 and w > |W|   [Liska and Steinberg, p. 22] */
  56 v > 0 and 4*w*v > 0 and 4*w*(4*w^2*v^2 + 3*WW^2 + w^2) > 0
  57    and 64*w^2*v^2*(w^2 - WW^2)*(w^2*v^2 + WW^2) > 0
  58    and 64*w^2*v^2*(w^2 - WW^2)^3*(w^2*v^2 + WW^2) > 0;
  59 errcatch(boolsimp(%));
  60 /* => B < 0 and a b > 0   [Liska and Steinberg, p. 49 (equation 86)] */
  61 /*thereExists y in C, thereExists n in C, thereExists e in R suchThat
  62   {realpart(y) > 0 and realpart(n) < 0 and y + A*%i*e - B*n = 0
  63       and a*n + b = 0};*/