1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
/* Original version of this file copyright 1999 by Michael Wester,
* and retrieved from http://www.math.unm.edu/~wester/demos/BooleanLogic/problems.macsyma
* circa 2006-10-23.
*
* Released under the terms of the GNU General Public License, version 2,
* per message dated 2007-06-03 from Michael Wester to Robert Dodier
* (contained in the file wester-gpl-permission-message.txt).
*
* See: "A Critique of the Mathematical Abilities of CA Systems"
* by Michael Wester, pp 25--60 in
* "Computer Algebra Systems: A Practical Guide", edited by Michael J. Wester
* and published by John Wiley and Sons, Chichester, United Kingdom, 1999.
*/
/* ----------[ M a c s y m a ]---------- */
/* ---------- Initialization ---------- */
showtime: all$
prederror: false$
/* ---------- Boolean Logic and Quantifier Elimination ---------- */
/* Simplify logical expressions => false */
true and false;
/* => true */
x or (not x);
boolsimp(%);
/* => x or y */
x or y or (x and y);
boolsimp(%);
/* => x */
logxor(logxor(x, y), 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;
errcatch(boolsimp(%));
/* 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 realpart(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 + WW^2)*y^2
+ 4*v*w*(w^2 - WW^2) + (w^2 - WW^2)^2 = 0 implies realpart(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*WW^2 + w^2) > 0
and 64*w^2*v^2*(w^2 - WW^2)*(w^2*v^2 + WW^2) > 0
and 64*w^2*v^2*(w^2 - WW^2)^3*(w^2*v^2 + WW^2) > 0;
errcatch(boolsimp(%));
/* => 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
{realpart(y) > 0 and realpart(n) < 0 and y + A*%i*e - B*n = 0
and a*n + b = 0};*/
|
