ProveDetails 命令
- ProveDetails( <Boolean Expression> )
-
返回自动证明结果的一些详细信息。
通常，GeoGebra 通过数值计算来判断一个 Boolean_values 是否为真。然而，ProveDetails 命令使用 符号方法 来确定一个命题在一般情况下是真还是假。此命令的作用类似于 Prove 命令，但还会将结果的一些详细信息作为 Lists :
-
返回。一个空列表 {} ，如果 GeoGebra 无法确定答案。
-
包含一个元素的列表： {false} ，如果该命题在一般情况下不成立。
-
包含一个元素的列表： {true} ，如果该命题始终为真（在可以构造图形的所有情况下）。
-
一个包含更多元素的列表，其中包含布尔值 真 以及另一个包含某些所谓 非退化 条件 ，如果该命题在某些条件下为真，例如 {true, {"AreCollinear(A,B,C),AreEqual(C,D)"}}。 这意味着如果所有条件都不为真（且可以构造图形），那么该命题将为 真。
-
一个列表 {true,{"…"}} ，如果该命题在某些条件下为真，但由于某些原因这些条件无法转换为人类可读的形式。
让我们定义一个顶点为
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
.
设
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
将重合。
设
AB
为线段
a
，并定义
l=Line(A,B)
。设
C
为直线 上的任意一点
l
，此外设
b=Segment(B,C)
,
c=Segment(A,C)
。现在
ProveDetails(a==b+c)
返回 {true,{"a+b==c", "b==a+c"}}：这意味着如果既不满足 \(a+b=c\)，也不满足 \(b=a+c\)，则 \(a=b+c\)。
非退化条件列表可能不是最简集合。对于上述示例， 最简集合将是空集。
|
另请参阅 Prove 命令， Boolean_values , GeoGebra 自动推理工具：教程 和 算法的技术细节 . |