|
We used QEPCAD B to repeat the calculation we did by hand for two coins. Note the use of keyboard symbols for logic symbols they closely resemble: E for \( \exists \), "there exists"; /\ for \( \wedge \), "and"; and ~ for \( \) "not".
Fordham-David-Swinarski:~ davids$ qepcad
=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition
Version B 1.65, 10 May 2011
by
Hoon Hong
(hhong@math.ncsu.edu)
With contributions by: Christopher W. Brown, George E.
Collins, Mark J. Encarnacion, Jeremy R. Johnson
Werner Krandick, Richard Liska, Scott McCallum,
Nicolas Robidoux, and Stanly Steinberg
=======================================================
Enter an informal description between '[' and ']':
[ two 2-sided dice ]
Enter a variable list:
(p1,p2,q1,q2)
Enter the number of free variables:
0
Enter a prenex formula:
(E p1)(E p2)(E q1)(E q2)[
p1 >= 0
/\ p2 >= 0
/\ q1 >= 0
/\ q2 >= 0
/\ p1 + p2 = 1
/\ q1 + q2 = 1
/\ p1 q1 = 1/4
/\ p1 q2 + p2 q1 = 2/4
/\ p2 q2 = 1/4
/\ [ ~[ [ p1 = 1/2] /\ [ p2 = 1/2] /\ [q1 =1/2] /\ [q2 = 1/2] ] ] ].
=======================================================
Before Normalization >
finish
An equivalent quantifier-free formula:
FALSE
===================== The End =======================
-----------------------------------------------------------------------------
2 Garbage collections, 942150 Cells and 0 Arrays reclaimed, in 10 milliseconds.
394488 Cells in AVAIL, 500000 Cells in SPACE.
System time: 88 milliseconds.
System time after the initialization: 82 milliseconds.
-----------------------------------------------------------------------------
When we tried to use QEPCAD B to analyze two three-sided dice, the program crashed. We do not understand the error message completely, but suspect that GCSI is a garbage collecting utility. It seemed unlikely to us that QEPCAD B would be able to analyze other sacks.
Fordham-David-Swinarski:~ davids$ qepcad
=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition
Version B 1.65, 10 May 2011
by
Hoon Hong
(hhong@math.ncsu.edu)
With contributions by: Christopher W. Brown, George E.
Collins, Mark J. Encarnacion, Jeremy R. Johnson
Werner Krandick, Richard Liska, Scott McCallum,
Nicolas Robidoux, and Stanly Steinberg
=======================================================
Enter an informal description between '[' and ']':
[ two 3-sided dice ]
Enter a variable list:
(p1,p2,p3,q1,q2,q3)
Enter the number of free variables:
0
Enter a prenex formula:
(E p1)(E p2)(E p3)(E q1)(E q2)(E q3)[
p1 >= 0
/\ p2 >= 0
/\ p3 >= 0
/\ q1 >= 0
/\ q2 >= 0
/\ q3 >= 0
/\ p1 + p2 + p3 = 1
/\ q1 + q2 + q3 = 1
/\ p1 q1 = 1/9
/\ p1 q2 + p2 q1 = 2/9
/\ p1 q3 + p2 q2 + p3 q1 = 3/9
/\ p2 q3 + p3 q2 = 2/9
/\ p3 q3 = 1/9
/\ [ ~[ [ p1 = 1/3] /\ [ p2 = 1/3 ] /\ [p3 = 1/3 ] /\ [q1 =1/3] /\ [q2 = 1/3] /\ [q3 = 1/3] ] ] ].
=======================================================
Before Normalization >
finish
** 99860 cells, 19999 arrays in 12 milliseconds.
Failure occurred in: GCSI (final check)
Reason for the failure: Too few cells reclaimed.
N = 99860
NU = 1000000
RHO = 10
Now the FAIL handler is aborting the program ...
Abort trap: 6