ProveDetails 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.

ProveDetails[ <Boolean Expression> ]

Returns some details of the result of the automated proof.

Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the ProveDetails command uses symbolic methods to determine whether a statement is true or false in general. This command works like the Prove command, but also returns some details of the result as a list:

• An empty list {} if GeoGebra cannot determine the answer.
• A list with one element: {false}, if the statement is not true in general.
• A list with one element: {true}, if the statement is always true.
• A list with more elements, containing the boolean value true and another list for the so-called non-degeneracy conditions, if the statement is true under certain conditions, e.g. {true, {"DegeneratePolygon[A,B,C,D]"}}. This means that if none of the conditions are true, then the statement will be true.

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 ProveDetails[p∥q] returns {true,{"AreEqual[A,B]"}}.This means that if the points A and B differ, then the midline DE of the triangle is parallel to the side AB.

It is possible that the list of the non-degeneracy conditions is not the simplest possible set.

Note: See also ProveDetails command, Boolean values and technical details of the algorithms.