ProveDetails Command

Warning:

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

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 behind may confirm or disprove the statement, basically the proof 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 behind, 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 is unknown: GeoGebra has no built-in logic to handle this situation.
• 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[AreParallel[p,q]] returns {true,{"AreCollinear[A,B,C]"}}.This means that if the triangle ABC is non-degenerate, then its midline DE is parallel to the side AB.

It is possible that the list of the non-degeneracy conditions is not the most simple set of the sufficient conditions for confirming the statement. GeoGebra can only claim that by assuming the returned non-degeneracy conditions, the statement will surely be true.

Note: See also Prove command.