This example illustrates both quantifier-free formula
simplification, and the `assume`

command. In it, a
new theorem is both discovered and proved using nothing but
formula simplification.

If a formula that is already quantifier free is entered into QEPCAD B,
the program produces a simple equivalent formula. As an interesting
example of formula simplification in QEPCAD B, consider the following:
Figure 1 shows a triangle *ABC* with what we might
call the "external bisector" of vertex *B* with respect to *A*.

Figure 1: Triangle

*
b ^{2} + a^{2} - c^{2} <= 0 \/ c (b^{2} + a^{2} - c^{2})^{2} < a b^{2} (2 a c - (c^{2} +
a^{2} - b^{2}))*.

*
a > 0 /\ b > 0 /\ c > 0 /\ a < b + c /\ b < a + c /\ c < a + b*. **(2)**

*c > 0 /\ b > 0 /\ a - b + c > 0 /\ a - c < 0 /\ a + b - c >
0*,

======================================================= Quantifier Elimination in Elementary Algebra and Geometry by Partial Cylindrical Algebraic Decomposition Version B 1.6, 20 Sep 2002 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 ']': [ Charaterizing triangles with external bisectors ] Enter a variable list: (c,b,a) Enter the number of free variables: 3 Enter a prenex formula: [ b^2 + a^2 - c^2 <= 0 \/ c (b^2 + a^2 - c^2)^2 < a b^2 (2 a c - (c^2 + a^2 - b^2)) ]. ======================================================= Before Normalization > assume [ a > 0 /\ b > 0 /\ c > 0 /\ a < b + c /\ b < a + c /\ c < a + b ] Before Normalization > finish An equivalent quantifier-free formula: a - c < 0 ====================================================In other words, given the assumption (i.e. the conditions that

Christopher W Brown Last modified: Sat Nov 2 13:25:23 EST 2002