Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
m (Link to Prove command) |
(Adding ProveDetails) |
||
| Line 1: | Line 1: | ||
<noinclude>{{Manual Page|version=5.0}}</noinclude>{{betamanual|version=5.0}} | <noinclude>{{Manual Page|version=5.0}}</noinclude>{{betamanual|version=5.0}} | ||
{{command|logical}} | {{command|logical}} | ||
| − | ;ProveDetails[ <Boolean Expression> ] | + | ;ProveDetails[ <Boolean Expression> ]: Returns some details of the result of the automated proof. |
| − | |||
| − | + | This command works like the [[Manual:Prove_Command|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 is also true. | ||
| + | :{{example| 1=<div>Let us define a triangle with vertices ''A'', ''B'' and ''C'', and define <code><nowiki>D=MidPoint[B,C]</nowiki></code>, <code><nowiki>E=MidPoint[A,C]</nowiki></code>, <code><nowiki>p=Line[A,B]</nowiki></code>, <code><nowiki>q=Line[D,E]</nowiki></code>. Now <code><nowiki>ProveDetails[AreParallel[p,q]]</nowiki></code> returns <nowiki>{true,{"AreCollinear[A,B,C]"}}</nowiki>.This means that if the triangle ''ABC'' is non-degenerate, then its midline ''DE'' is parallel to the side ''AB''.</div>}} | ||
| + | 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 [[Manual:Prove_Command|Prove]] command.}} | {{Note| See also [[Manual:Prove_Command|Prove]] command.}} | ||
Revision as of 13:59, 17 May 2012
 |
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.
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 is also 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]. NowProveDetails[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.
