Q E P C A D - A Triangles Problem

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 ABC with the external bisector of vertex B with respect to A.

It is fairly clear from the diagram that this external bisector exists as drawn if and only if theta > (pi - phi)/2. Suppose we want this characterization of the existence of the "external bisector" in terms of the side lengths a, b and c rather than the angles theta and phi. Straightforward application of the common trigonometric identities produces the equivalent characterization that, if a, b and c are the side lengths of a non-degenerate triangle, this external bisector exists if and only if

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 if

a > 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 formula

c > 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                 
            Elementary Algebra and Geometry            
      Partial Cylindrical Algebraic Decomposition      
               Version B 1.6, 20 Sep 2002
                       Hoon Hong                       
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:
Enter the number of free variables:
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 >

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.

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