Příkaz PodrobnostiDukazu

PodrobnostiDukazu( <Booleovský výraz> )

Poskytne detailnější informace o výsledku automatického důkazu obecné pravdivosti tvrzení vloženého ve formě booleovského výrazu, tj. výrazu nabývajícího hodnoty true nebo false.

Normálně GeoGebra rozhoduje o pravdivosti booleovského výrazu, tj. zda je jeho hodnota true nebo false, pomocí numerického výpočtu. Příkaz PodrobnostiDukazu však pro vyhodnocení toho, zda má vložený booleovský výraz hodnotu true nebo false, používá symbolické metody výpočtu. Zabývá se tak obecnou platností vlastnosti, které se výraz týká. Příkaz funguje stejně jako příkaz Dokazat, akorát navíc vypíše nějaké detailnější informace o svém výsledku formou seznamu takto:

  • Prázdný seznam {}, pokud GeoGebra nemůže určit odpověď.

  • Seznam s jedním prvkem: {false}, pokud tvrzení není obecně pravdivé.

  • Seznam s jedním prvkem: {true}, pokud je předmětné tvrzení vždy pravdivé (ve všech případech, na které může být daný obrázek modifikován).

  • Seznam s více prvky, konkrétně obsahující booleovskou hodnotu true spolu s dalším seznamem pro tzv. nedegenerativní podmínky (non-degeneracy conditions), pokud je tvrzení pravdivé za určitých podmínek, např. {true, {"JsouKolinearni(A,B,C),JsouTotozne(C,D)"}}. Konkrétně to znamená, že pokud není splněna žádná z uvedených podmínek (a obrázek může být sestrojen), předmětné tvrzení je pravdivé.

  • A list {true,{"…​"}}, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.

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.

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.

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.

Viz též příkaz Dokazat, Pravdivostní hodnoty a článek GeoGebra Automated Reasoning Tools: A Tutorial a technical details of the algorithms.