Difference between revisions of "Prove Command"
From GeoGebra Manual
m (Indentation removed) |
|||
| Line 2: | Line 2: | ||
{{command|logical}} | {{command|logical}} | ||
{{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.}} | {{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.}} | ||
| − | ;Prove[ <Boolean Expression> ]: Returns if the result of the automated proof is true in general. | + | ;Prove[ <Boolean Expression> ]: Returns if the result of the automated proof is true or false in general. |
| − | GeoGebra decides if a [[Manual:Boolean_values|boolean expression]] is true or not by using numerical computation. With the Prove command it is also possible to check a statement | + | Normally GeoGebra decides if a [[Manual:Boolean_values|boolean expression]] is true or not by using numerical computation. With the Prove command it is also possible to check a statement using [[w:Symbolic_computation|symbolic computation]] to determine whether the result is ''true'' or ''false'' in general. If the calculations cannot determine the answer, the result is ''undefined''. |
{{example| 1=<div>We define three free points, <code><nowiki>A=(1,2)</nowiki></code>, <code><nowiki>B=(3,4)</nowiki></code>, <code><nowiki>C=(5,6)</nowiki></code>. Now <code><nowiki>AreCollinear[A,B,C]</nowiki></code> yields ''true'', since a numerical check is used for this single case, but <code><nowiki>Prove[AreCollinear[A,B,C]]</nowiki></code> yields ''false'', since the three points are in general not collinear, when we drag the free points.</div>}} | {{example| 1=<div>We define three free points, <code><nowiki>A=(1,2)</nowiki></code>, <code><nowiki>B=(3,4)</nowiki></code>, <code><nowiki>C=(5,6)</nowiki></code>. Now <code><nowiki>AreCollinear[A,B,C]</nowiki></code> yields ''true'', since a numerical check is used for this single case, but <code><nowiki>Prove[AreCollinear[A,B,C]]</nowiki></code> yields ''false'', since the three points are in general not collinear, when we drag the free points.</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 both <code><nowiki>p∥q</nowiki></code> and <code><nowiki>Prove[p∥q]</nowiki></code> yield ''true'', since a midline of a triangle will always be parallel to the appropriate side.</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 both <code><nowiki>p∥q</nowiki></code> and <code><nowiki>Prove[p∥q]</nowiki></code> yield ''true'', since a midline of a triangle will always be parallel to the appropriate side.</div>}} | ||
{{Note| See also [[Manual:ProveDetails_Command|ProveDetails]] command and [[Manual:Boolean_values|Boolean values]].}} | {{Note| See also [[Manual:ProveDetails_Command|ProveDetails]] command and [[Manual:Boolean_values|Boolean values]].}} | ||
Revision as of 09:07, 1 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. |
- Prove[ <Boolean Expression> ]
- Returns if the result of the automated proof is true or false in general.
Normally GeoGebra decides if a boolean expression is true or not by using numerical computation. With the Prove command it is also possible to check a statement using symbolic computation to determine whether the result is true or false in general. If the calculations cannot determine the answer, the result is undefined.
Example:
We define three free points,
A=(1,2), B=(3,4), C=(5,6). Now AreCollinear[A,B,C] yields true, since a numerical check is used for this single case, but Prove[AreCollinear[A,B,C]] yields false, since the three points are in general not collinear, when we drag the free points.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 both p∥q and Prove[p∥q] yield true, since a midline of a triangle will always be parallel to the appropriate side. Note: See also ProveDetails command and Boolean values.
