ProveDetails コマンド

ProveDetails( <論理式> )

自動証明の結果に関するいくつかの詳細を返す．

通常、GeoGebraは数値計算を用いて論理式 論理式が 真 か 偽 かを判断する．しかし，ProveDetailsコマンドはhttps://en.wikipedia.org/wiki/Symbolic_computation[記号演算(英文)]を使用して，一般にステートメントが真か偽かを判断する．このコマンドはProve コマンドと同様に機能するが，結果の詳細をリストとして返す：

  • GeoGebraが答えを決定できない場合は，空のリスト \{}．

  • 一つの要素を持つリスト: {false}．ステートメントが 一般的には真ではない 場合．

  • 一つの要素を持つリスト: {true}．ステートメントが 常に真 である場合 (図形が構築可能なすべての場合において)．

  • 特定の条件下でステートメントが真である場合， true の論理値といわゆる 非退化条件 のリストを含む要素がより多いリストを返す．例えば，\{true, \{"AreCollinear(A,B,C),AreEqual(C,D)"}}のようなリストである．これは，条件のいずれも真でない場合（そして図形が構築できる場合），命題は真となることを意味する．

  • リスト\{true,\{"…​"}} は，ステートメントが特定の条件下で真であるが，これらの条件が何らかの理由で人間が読める形に変換できない場合．

線分 AB を a とし，l=Line(A,B)`を定義する．C を直線 l 上の任意の点とし，さらにb=Segment(B,C), `c=Segment(A,C) とする．P`ProveDetails(a==b+c)` を実行すると \{true,\{"a+b==c", "b==a+c"}}が返される．これは、 \(a+b=c\)でも\(b=a+c\)でもない場合，つまり\(a+b=c\)や\(b=a+c\)のいずれの条件も満たされない場合には，\(a=b+c\)となることを意味する．

線分ABを aとし，C=MidPoint(A,B), b=PerpendicularBisector(A,B), D=Intersect(a,b)`と定義する．ここでProveDetails(C==D)` は \{true,\{"AreEqual(A,B)"}}を返す：点 A と点 B が異なれば，点 C と点 D は一致することを意味する．

頂点 A, B, Cを持つ三角形を定義し,D=MidPoint(B,C), E=MidPoint(A,C), p=Line(A,B), q=Line(D,E)`と定義する．ProveDetails(p∥q)` を実行すると {true} が返され、これは図が描ける場合、中点をむずぶ線分 DE は辺 AB に平行であることを意味する．

非退化条件のリストが最も単純な集合でない可能性がある．上記の例では，最も単純な集合は空集合になる．

こちらも参照： Prove コマンド， 真偽値, GeoGebra Automated Reasoning Tools: A Tutorial （英文）， technical details of the algorithms（英文）．