Polecenie UdowodnijSzczegółowo

UdowodnijSzczegółowo( <Wyrażenie logiczne> )

Returns some details of the result of the automated proof.

Zazwyczaj GeoGebra decyduje, czy dane wyrażenie logiczne (boolowkie) jest prawdziwe, czy fałszywe, używając obliczeń numerycznych. Jednak polecenie UdowodnijSzczegółowo wykorzystuje metody symboliczne o określenia, czy dane stwierdzenie jest ogólnie prawdziwe czy fałszywe. To polecenie działa podobnie jak polecenie Udowodnij, ale dodatkowo zwraca szczegóły wyniku w postaci listy:

  • Pustą listę {}, jeśli GeoGebra nie może określić odpowiedzi.

  • Listę z jednym elementem: {false}, jeśli stwierdzenie nigdy nie jest prawdziwe.

  • Listę z jednym elementem: {true}, jeśli stwierdzenie jest zawsze prawdziwe (we wszystkich przypadkach, gdy konstrukcja jest możliwa).

  • Listę z większą liczbą elementów, zawierającą wartość logiczną true oraz inną listę tzw. warunków niedegeneracji (nieosobliwych), jeśli stwierdzenie jest prawdziwe tylko pod pewnymi warunkami, np. {true, {"SąWspółliniowe(A,B,C),SąRówne(C,D)"}}. Oznacza to, że jeśli żaden z warunków nie jest spełniony (i konstrukcja jest możliwa), to stwierdzenie będzie prawdziwe.

  • Listę {true,{"…​"}}, jeśli stwierdzenie jest prawdziwe pod pewnymi warunkami, ale z jakichś powodów tych warunków nie da się zapisać w sposób czytelny dla człowieka.

Zdefiniujmy trójkąt o wierzchołkach A, B i C. Niech D=PunktŚrodkowy(B,C), E=PunktŚrodkowy(A,C), p=Prosta(A,B), q=Prosta(D,E). Wówczas UdowodnijSzczegółowo(p∥q) zwraca {true}, co oznacza, że jeśli konstrukcja jest możliwa, to prosta DE jest równoległa do boku AB.

Dany jest odcinek AB o nazwie a. Zdefiniujmy C=PunktŚrodkowy(A,B), b=SymetralnaOdcinka(A,B), D=Przecięcie(a,b). Wówczas UdowodnijSzczegółowo(C==D) zwraca {true,{"SąRówne(A,B)"}}: oznacza to, że jeśli punkty A i B są różne, to punkty C i D będą się pokrywać.

Dany jest odcinek AB o nazwie a. Zdefiniujmy l=Prosta(A,B). Niech C będzie dowolnym punktem na proste l, dodatkowo niech b=Odcinek(B,C), c=Odcinek(A,C). Wówczas UdowodnijSzczegółowo(a==b+c) zwraca {true,{"a+b==c", "b==a+c"}}: oznacza to, że jeśli nie zachodzą równości \(a+b=c\) i \(b=a+c\), prawdziwa jest równość \(a=b+c\).

Możliwe jest, że lista warunków niedegeneracji nie jest najprostsza z możliwych. Dla powyższego przykładu najprostszym zestawem byłby zbiór pusty.