Prove Command

Warning:

This GeoGebra command is heavily under construction. Expect to encounter various problems when trying it out. The syntax or the output of this command may be subject to change.

Prove[ <Boolean Expression> ]

Returns if the result of the automated proof is true or false in general.

Normally GeoGebra decides if a boolean expression is true or not by using numerical computation. With the Prove command it is also possible to check a statement using symbolic computation to determine whether the result is true or false in general. If the calculations cannot determine the answer, the result is undefined.

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 p∥q and Prove[p∥q] yield true, since a midline of a triangle will always be parallel to the appropriate side.

Note: See also ProveDetails command and Boolean values.