Figure 1: Triangle ABC with the external bisector of vertex B with respect to A.
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.
b2 + a2 - c2 <= 0 \/ c (b2 + a2 - c2)2 < a b2 (2 a c - (c2 + a2 - b2)). (1)
Of course a, b and c are the side lengths of a non-degenerate triangle if and only ifa > 0 /\ b > 0 /\ c > 0 /\ a < b + c /\ b < a + c /\ c < a + b. (2)
The conjunction of (1) and (2) completely characterizes the triples of real numbers (a,b,c) that are side-lengths of non-degenerate triangles for which the above described external bisector exists. Entering this conjunction as input to QEPCAD B produces the equivalent formulac > 0 /\ b > 0 /\ a - b + c > 0 /\ a - c < 0 /\ a + b - c > 0,
which is a little hard to interpret, because it's unclear which conditions simply specify a non-degenerate triangle, and which are specific to characterizing the existence of the external bisector. QEPCAD B allows us to declare "assumptions", which are conditions on the free variables that are "assumed" by the solution formula produced. A true solution formula is actually the conjunction of the assumptions and the solution formula QEPCAD B produces. Here is a QEPCAD B session for this simplification problem:
=======================================================
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 a,
b and c really form a triangle), the input formula is equivalent
to a - c < 0. Simplification has "discovered" the theorem
that the external bisector described above exists if and only if side
c is longer than side a.