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. Příkladem takového výstupu je seznam {true, {"JsouKolinearni(A,B,C),JsouTotozne(C,D)"}}, jehož význam je takový, že pokud není splněna žádná z uvedených podmínek "JsouKolinearni(A,B,C),JsouTotozne(C,D)" (a příslušná geometrická konfigurace může být zobrazena), předmětné tvrzení je pravdivé.

  • Seznam ve tvaru {true,{"…​"}}, pokud je tvrzení pravdivé za určitých podmínek, které však nelze z nějakých důvodů vyjádřit člověku srozumitelnou formou.

Nechť jsou pro trojúhelník s vrcholy A, B, C definovány body D=StredSoumernosti(B,C), E=StredSoumernosti(A,C) a přímky p=Primka(A,B), q=Primka(D,E). Potom příkaz PodrobnostiDukazu(p∥q) vrátí {true}, což znamená, že pokud lze sestrojit obrázek, střední příčka DE uvažovaného trojúhelníku je rovnoběžná se stranou AB.

Pro úsečku AB označenou a definujme C=StredSoumernosti(A,B), b=OsaUsecky(A,B), D=Prusecik(a,b). Nyní příkaz PodrobnostiDukazu(C==D) vrátí {true,{"JsouTotozne(A,B)"}}, což znamená, že pokud jsou body A a B různé, potom body C a D splývají, tj. jsou totožné.

Spolu s úsečkou AB označenou a je definována přímka l=Line(A,B). Nechť C je libovolný bod na přímce l, pro který jsou definovány úsečky b=Segment(B,C), c=Segment(A,C). Potom příkaz ProveDetails(a==b+c) vrátí {true,{"a+b==c", "b==a+c"}}, což znamená, že pokud neplatí a+b=c, ani b=a+c, potom je pravda, že a=b+c.

Může se stát, že uvedený seznam nedegenerativních podmínek není nejjednodušší možný.

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