Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
(TRAC-5362) |
(command syntax: changed [ ] into ( )) |
||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
<noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}} | <noinclude>{{Manual Page|version=5.0}}</noinclude>{{command|logical}} | ||
| − | ;ProveDetails | + | ;ProveDetails( <Boolean Expression> ): Returns some details of the result of the automated proof. |
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]]: | 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. | * 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: '''{false}''', if the statement is not true in general. | ||
| − | * A list with one element: '''{true}''', if the statement is always true. | + | * 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 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. | * 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| 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 <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 ''AB'' be the segment ''a'', and define <code><nowiki>C=MidPoint | + | :{{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>}} |
| − | :{{example| 1=<div>Let ''AB'' be the segment ''a'', and define <code><nowiki>l=Line | + | :{{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].}} |
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). 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.
