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 in general.

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 in general, by changing the free points to different sets of positions. GeoGebra then tries to use different built-in theoretical methods to decide the statement automatically. The output is a simple true or false: true when the underlying computations assure that the statement is true in general, and false when the statement is false in most cases. If the calculations cannot give an exact answer, the result is undecided.

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.