Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
m (Typo fix) |
(add link to gg-art-doc) |
||
| Line 12: | Line 12: | ||
:{{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>}} | :{{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>}} | ||
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. | 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]] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} | + | {{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].}} |
Revision as of 09:31, 27 March 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]. NowProveDetails[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]. NowProveDetails[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 letb=Segment[B,C],c=Segment[A,C]. NowProveDetails[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.
Note: See also Prove command, Boolean values, GeoGebra Automated Reasoning Tools: A Tutorial and technical details of the algorithms.
