Difference between revisions of "Prove Command"

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.

@@ Line 1: / Line 1: @@
-<noinclude>{{Manual Page|version=5.0}}</noinclude>{{betamanual|version=5.0}}
+<noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}}
-{{command|logical}}
+;Prove( <Boolean Expression> ): Returns whether the given boolean expression is true or false in general.
-{{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.}}
+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''.
-;Prove[ <Boolean Expression> ]: Returns if the result of the automated proof is true under certain conditions.
+{{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. See also [https://www.geogebra.org/m/vhZETdtd interactive version of this example].
-GeoGebra uses several methods to decide if a boolean expression is true or not in general. This means that if we change the free points to a different set of positions, a boolean expression may still be true in most cases (e.g. when no triplets of the the free points are collinear). When the boolean expression is evaluated only once, a numerical computation is used, but a general answer (a so-called decision) needs further testing.
+</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].}}
-The decision method is based on symbolic calculations in GeoGebra, which usually require heavy computations. Hence the details of these computations are hidden, and the output is a simple ''true'' or ''false'': true when the computations assure that the statement is surely true under certain conditions, and false when the statement is false in most cases. If the calculations cannot give an exact answer, the result is ''undecided''.
-:{{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>}}
-{{Note| See also [[Manual:ProveDetails_Command|ProveDetails]] command.}}

Difference between revisions of "Prove Command"

Latest revision as of 19:36, 8 April 2024

Prove

Command Categories (All commands)