Prove Command

Warning:

This GeoGebra command is heavily under construction. Expect to encounter various problems when trying it out.

Prove[ <Boolean Expression> ]

Returns if the result of the automated proof is true under certain conditions.

GeoGebra uses several methods to decide if a boolean expression is true or not in general. This means that if we change the free points to a different set of positions, a boolean expression may still be true in most cases (e.g. when no triplets of the the free points are collinear). When the boolean expression is evaluated only once, a numerical computation is used, but a general answer (a so-called decision) needs further testing.

The decision method is based on symbolic calculations in GeoGebra, which usually require heavy computations. Hence the details of these computations are hidden, and the output is a simple true or false: true when the computations assure that the statement is surely true under certain conditions, and false when the statement is false in most cases or the calculations cannot give an exact answer.

Example:

We define three free points, A=(1,2), B=(3,4), C=(5,6). Now AreCollinear[A,B,C] yields true, since a numerical check is used for this single case, but Prove[AreCollinear[A,B,C]] yields false, since the three points are in general not collinear, when we drag the free points.

Example:

Let us define a triangle with vertices A, B and C, and define D=MidPoint[B,C], E=MidPoint[A,C], p=Line[A,B], q=Line[D,E]. Now both AreParallel[p,q] and Prove[AreParallel[p,q]] yield true, since a midline of a triangle will always be parallel to the appropriate side.

Note: See also ProveDetails command.