Difference between revisions of "Prove Command"
From GeoGebra Manual
m (Text replace - ";(.*)\[(.*)\]" to ";$1($2)") |
(Do not embed example) |
||
| (One intermediate revision by one other user not shown) | |||
| Line 2: | Line 2: | ||
;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 | + | {{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 | + | {{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. See also [https://www.geogebra.org/m/vhZETdtd interactive version of this example]. |
| − | |||
</div>}} | </div>}} | ||
{{Note| See also [[ProveDetails Command|ProveDetails]] command, [[Boolean values|Boolean values]], [https://github.com/kovzol/gg-art-doc/tree/master/pdf/english.pdf GeoGebra Automated Reasoning Tools: A Tutorial] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} | {{Note| See also [[ProveDetails Command|ProveDetails]] command, [[Boolean values|Boolean values]], [https://github.com/kovzol/gg-art-doc/tree/master/pdf/english.pdf GeoGebra Automated Reasoning Tools: A Tutorial] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} | ||
Latest revision as of 19:36, 8 April 2024
- 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 command AreCollinear(A,B,C) yields true, since a numerical check is used on the current coordinates of the points. Using Prove(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 both p∥q and Prove(p∥q) yield true, since a midline of a triangle will always be parallel to the appropriate side. See also interactive version of this example.
Note: See also ProveDetails command, Boolean values, GeoGebra Automated Reasoning Tools: A Tutorial and technical details of the algorithms.
