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.

This command works like the Prove command, but also returns some details of the result of the automated proof. Since the computations used by GeoGebra may confirm or disprove the statement, the result can be true, false or unknown: in the last case GeoGebra cannot decide if the statement is true or false in general. Such problems can occur when the statement cannot be proven by the methods used by GeoGebra, or if it would be too time consuming to complete the computation.

The return value of this command is always a list:

• An empty list {} if the proof failed: GeoGebra has no built-in logic to handle this situation, or the computation has run out of time.
• 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, {"AreCollinear[A,B,C]", "AreCollinear[A,B,D]", "AreCollinear[A,C,D]", "AreCollinear[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 Prove command.