Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
(remove warning) |
|||
Line 1: | Line 1: | ||
<noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}}{{betamanual|version=5.0}} | <noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}}{{betamanual|version=5.0}} | ||
− | |||
;ProveDetails[ <Boolean Expression> ]: Returns some details of the result of the automated proof. | ;ProveDetails[ <Boolean Expression> ]: Returns some details of the result of the automated proof. | ||
Revision as of 10:48, 5 September 2014
This page is about a feature that is supported only in GeoGebra 5.0. |
- 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 some so-called non-degeneracy conditions, if the statement is true under certain conditions, e.g. {true, {"AreCollinear[A,B,C],AreEqual[C,D]"}}. This means that if none of the conditions are true, then the statement will be true.
- A list {true,{"..."}}, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.
- 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 ifProveDetails[p∥q]
returns {true,{"AreEqual[A,B]"}}, it 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. For the above example, the simplest set would be the empty set.
Note: See also Prove command, Boolean values and technical details of the algorithms.