Difference between revisions of "ProveDetails Command"
From GeoGebra Manual
(Changes like for the Prove command) |
|||
Line 4: | Line 4: | ||
;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 [[Prove_Command|Prove]] command, but also returns some details of the result | + | 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 | ||
* 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. | ||
− | * 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, {" | + | * 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, {"DegeneratePolygon[A,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,{"AreEqual[A,B]"}}</nowiki>.This means that if the points ''A'' and ''B'' differ, then the midline ''DE'' of the triangle is parallel to the side ''AB''.</div>}} | |
It is possible that the list of the non-degeneracy conditions is not the simplest possible set. | It is possible that the list of the non-degeneracy conditions is not the simplest possible set. | ||
− | {{Note| See also [[ | + | {{Note| See also [[ProveDetails Command|ProveDetails]] command, [[Boolean values|Boolean values]] and [http://dev.geogebra.org/trac/wiki/TheoremProving technical details of the algorithms].}} |
Revision as of 11:24, 2 June 2012
This page is about a feature that is supported only in GeoGebra 5.0. |
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. |
- 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.
- 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, {"DegeneratePolygon[A,B,C,D]"}}. This means that if none of the conditions are true, then the statement will be true.
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,{"AreEqual[A,B]"}}.This means that if the points A and B differ, then the midline DE of the triangle is parallel to the side AB.It is possible that the list of the non-degeneracy conditions is not the simplest possible set.
Note: See also ProveDetails command, Boolean values and technical details of the algorithms.