超级画板自动推理功能初探

1、先来举一个例子：

在z+z超级画板界面作正方形ABCD，F、J分别在AD、CD上，且∠FBJ=45°，BF、BJ与AC交于K、L，M为FJ中点。求证：KM⊥LM。

待整个图形作好以后，点击“推论”——“自动推理”；

稍等一会，右边的推理区就会出现一大堆推理结果。

2、怎么选出自己感兴趣的推理内容呢？

我们的题目是要证明两个线段互相垂直，所以找“垂直”的部分；

可以看到，垂直信息共14条；

点开左边的“+”号，发现第9条就是我们的目标——KM⊥LM；

如果看不懂结论是怎么来的，可以继续打开结论前面的“+”号，直到弄明白了为止！

3、试着推广上面的结论！

给定矩形ABCD，E在AD上，F在CD上，BE、BF交AC于G、H，

GJ与CD垂直，HK与AD垂直，GJ与HK交于L，I为EF中点。

求证：B、I、L共线！

4、超级画板不给力，虽然给出了将近1500条“不平凡结论”，但却没有给出B、I、L共线的结论！

这说明，自动推理功能并非是一把解决几何问题的万能钥匙！

5、再来尝试一些简单结论。

三角形三条中线共点：

△ABC三边中点分别是D、E、F，设AD交BF于H；求证：E、H、C共线。

三角形三个顶点到对边的垂线共点：

△ABC，AJ⊥BC，CK⊥AB，AJ交CK于L；求证：BL⊥AC。

超级画板给出的推理过程还是很详细的！