Difference between revisions of "Prove Command"
From GeoGebra Manual
(Applet added) |
|||
Line 1: | Line 1: | ||
− | <noinclude>{{Manual Page|version=5.0}}</noinclude>{{betamanual|version=5.0}} | + | <noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}}{{betamanual|version=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.}} | {{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 whether the given boolean expression is true or false in general. | ;Prove[ <Boolean Expression> ]: Returns whether the given boolean expression is true or false in general. | ||
Normally, GeoGebra decides whether a [[Boolean_values|boolean expression]] is true or not by using numerical computations. However, the Prove command uses [[w:Symbolic_computation|symbolic methods]] to determine whether a statement is ''true'' or ''false'' in general. If GeoGebra cannot determine the answer, the result is ''undefined''. | Normally, GeoGebra decides whether a [[Boolean_values|boolean expression]] is true or not by using numerical computations. However, the Prove command uses [[w:Symbolic_computation|symbolic methods]] to determine whether a statement is ''true'' or ''false'' in general. If GeoGebra 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>. The command <code><nowiki>AreCollinear[A,B,C]</nowiki></code> yields ''true'', since a numerical check is used on the current coordinates of the points. Using <code><nowiki>Prove[AreCollinear[A,B,C]]</nowiki></code> you will get ''false'' as an answer, since the three points are not collinear in general, i.e. when we change the 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>. The command <code><nowiki>AreCollinear[A,B,C]</nowiki></code> yields ''true'', since a numerical check is used on the current coordinates of the points. Using <code><nowiki>Prove[AreCollinear[A,B,C]]</nowiki></code> you will get ''false'' as an answer, since the three points are not collinear in general, i.e. when we change the 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. | + | :{{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. |
<ggb_applet width="525" height="366" version="5.0" id="40121" enableRightClick="false" showAlgebraInput="false" enableShiftDragZoom="false" showMenuBar="false" showToolBar="false" showToolBarHelp="true" enableLabelDrags="false" showResetIcon="false"/> | <ggb_applet width="525" height="366" version="5.0" id="40121" enableRightClick="false" showAlgebraInput="false" enableShiftDragZoom="false" showMenuBar="false" showToolBar="false" showToolBarHelp="true" enableLabelDrags="false" showResetIcon="false"/> | ||
</div>}} | </div>}} | ||
{{Note| See also [[ProveDetails Command|ProveDetails]] command, [[Boolean values|Boolean values]] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} | {{Note| See also [[ProveDetails Command|ProveDetails]] command, [[Boolean values|Boolean values]] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} |
Revision as of 12:22, 22 July 2014
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 whether the given boolean expression is true or false in general.
Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the Prove command uses symbolic methods to determine whether a statement is true or false in general. If GeoGebra cannot determine the answer, the result is undefined.
- Example:We define three free points,
A=(1,2)
,B=(3,4)
,C=(5,6)
. The commandAreCollinear[A,B,C]
yields true, since a numerical check is used on the current coordinates of the points. UsingProve[AreCollinear[A,B,C]]
you will get false as an answer, since the three points are not collinear in general, i.e. when we change the 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 bothp∥q
andProve[p∥q]
yield true, since a midline of a triangle will always be parallel to the appropriate side.
Note: See also ProveDetails command, Boolean values and technical details of the algorithms.