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
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 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 in Elementary Algebra and Geometry by Partial Cylindrical Algebraic Decomposition Version B 1.6, 20 Sep 2002 by Hoon Hong (firstname.lastname@example.org) 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.