Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
| Line 4: | Line 4: | ||
;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. | ||
| − | This command works like the [[ | + | This command works like the [[Prove_Command|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: | The return value of this command is always a list: | ||
| − | * An empty 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: | + | * A list with one element: '''{false}''', if the statement is not true in general. |
| − | * A list with one element: | + | * 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. | * 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| 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[p∥q]</nowiki></code> returns <nowiki>{true,{"AreEqual[A,B]"}}</nowiki>.This means that if the points ''A'' and ''B'' differ, then the midline ''DE'' of the triangle is parallel to the side ''AB''.</div>}} | :{{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[p∥q]</nowiki></code> returns <nowiki>{true,{"AreEqual[A,B]"}}</nowiki>.This means that if the points ''A'' and ''B'' differ, then the midline ''DE'' of the triangle is parallel to the side ''AB''.</div>}} | ||
| − | It is possible that the list of the non-degeneracy conditions is not the | + | It is possible that the list of the non-degeneracy conditions is not the simplest possible set. |
{{Note| See also [[Prove_Command|Prove]] command.}} | {{Note| See also [[Prove_Command|Prove]] command.}} | ||
Revision as of 10:57, 2 June 2012
 |
This page is about a feature that is supported only in GeoGebra 5.0. |
 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]. NowProveDetails[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.
