Difference between revisions of "ProveDetails Command"

Latest revision as of 10:37, 11 October 2017

ProveDetails( <Boolean Expression> ): Returns some details of the result of the automated proof.

Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the ProveDetails command uses symbolic methods to determine whether a statement is true or false in general. This command works like the Prove command, but also returns some details of the result as a list:

An empty list {} if GeoGebra cannot determine the answer.
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 (in all cases when the diagram can be constructed).
A list with more elements, containing the boolean value true and another list for some so-called non-degeneracy conditions, if the statement is true under certain conditions, e.g. {true, {"AreCollinear(A,B,C),AreEqual(C,D)"}}. This means that if none of the conditions are true (and the diagram can be constructed), then the statement will be true.
A list {true,{"..."}}, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.

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 ProveDetails(p∥q) returns {true}, which means that if the diagram can be constructed, then the midline DE of the triangle is parallel to the side AB.

Example:

Let AB be the segment a, and define C=MidPoint(A,B), b=PerpendicularBisector(A,B), D=Intersect(a,b). Now ProveDetails(C==D) returns {true,{"AreEqual(A,B)"}}: it means that if the points A and B differ, then the points C and D will coincide.

Example:

Let AB be the segment a, and define l=Line(A,B). Let C be an arbitrary point on line l, moreover let b=Segment(B,C), c=Segment(A,C). Now ProveDetails(a==b+c) returns {true,{"a+b==c", "b==a+c"}}: it means that if neither a+b=c, nor b=a+c, then a=b+c.

It is possible that the list of the non-degeneracy conditions is not the simplest possible set. For the above example, the simplest set would be the empty set.

@@ 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}}
+;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 [[Manual:Prove_Command|Prove]] command, but also returns some details of the result of the automated proof. Since the computations behind may confirm or disprove the statement, basically the proof 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 behind, or if it would be too time consuming to complete the computation.
+Normally, GeoGebra decides whether a [[Boolean_values|boolean expression]] is true or not by using numerical computations. However, the ProveDetails command uses [[w:Symbolic_computation|symbolic methods]] to determine whether a statement is true or false in general. This command works like the [[Prove_Command|Prove]] command, but also returns some details of the result as a [[Lists|list]]:
+* An empty list '''{}''' if GeoGebra cannot determine the answer.
-The return value of this command is always a list:
+* A list with one element: '''{false}''', if the statement is not true in general.
-* An empty list ({}) if the proof is unknown: GeoGebra has no built-in logic to handle this situation.
+* A list with one element: '''{true}''', if the statement is always true (in all cases when the diagram can be constructed).
-* A list with one element: {''false''}, if the statement is not true in general.
+* A list with more elements, containing the boolean value ''true'' and another list for some so-called ''non-degeneracy conditions'', if the statement is true under certain conditions, e.g. {true, {"AreCollinear(A,B,C),AreEqual(C,D)"}}. This means that if none of the conditions are true (and the diagram can be constructed), then the statement will be true.
-* A list with one element: {''true''}, if the statement is always true.
+* A list '''{true,{"..."}}''', if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.
-* 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}</nowiki>, which means that if the diagram can be constructed, 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[AreParallel[p,q]]</nowiki></code> returns <nowiki>{true,{"AreCollinear[A,B,C]"}}</nowiki>.This means that if the triangle ''ABC'' is non-degenerate, then its midline ''DE'' is parallel to the side ''AB''.</div>}}
+:{{example| 1=<div>Let ''AB'' be the segment ''a'', and define <code><nowiki>C=MidPoint(A,B)</nowiki></code>, <code><nowiki>b=PerpendicularBisector(A,B)</nowiki></code>, <code><nowiki>D=Intersect(a,b)</nowiki></code>. Now <code><nowiki>ProveDetails(C==D)</nowiki></code> returns <nowiki>{true,{"AreEqual(A,B)"}}</nowiki>: it means that if the points ''A'' and ''B'' differ, then the points ''C'' and ''D'' will coincide.</div>}}
-It is possible that the list of the non-degeneracy conditions is not the most simple set of the sufficient conditions for confirming the statement. GeoGebra can only claim that by assuming the returned non-degeneracy conditions, the statement will surely be true.
+:{{example| 1=<div>Let ''AB'' be the segment ''a'', and define <code><nowiki>l=Line(A,B)</nowiki></code>. Let ''C'' be an arbitrary point on line ''l'', moreover let <code><nowiki>b=Segment(B,C)</nowiki></code>, <code><nowiki>c=Segment(A,C)</nowiki></code>. Now <code><nowiki>ProveDetails(a==b+c)</nowiki></code> returns <nowiki>{true,{"a+b==c", "b==a+c"}}</nowiki>: it means that if neither <math>a+b=c</math>, nor <math>b=a+c</math>, then <math>a=b+c</math>.</div>}}
-{{Note| See also [[Manual:Prove_Command|Prove]] command.}}
+It is possible that the list of the non-degeneracy conditions is not the simplest possible set. For the above example, the simplest set would be the empty set.
+{{Note| See also [[Prove Command|Prove]] 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].}}

Difference between revisions of "ProveDetails Command"

Latest revision as of 10:37, 11 October 2017

ProveDetails

Command Categories (All commands)