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

电脑

z+z超级画板

先来举一个例子：在z+z超级画板界面作正方形ABCD，F、J分别在AD、CD上，且∠FBJ=45°，BF、BJ与AC交于K、L，M为FJ中点。求证：KM⊥LM。待整个图形作好以后，点击“推论”——“自动推理”；稍等一会，右边的推理区就会出现一大堆推理结果。

怎么选出自己感兴趣的推理内容呢？我们的题目是要证明两个线段互相垂直，所以找“垂直”的部分；可以看到，垂直信息共14条；点开左边的“+”号，发现第9条就是我们的目标——KM⊥LM；如果看不懂结论是怎么来的，可以继续打开结论前面的“+”号，直到弄明白了为止！

试着推广上面的结论！给定矩形ABCD，E在AD上，F在CD上，BE、BF交AC于G、H，GJ与CD垂直，HK与AD垂直，GJ与HK交于L，I为EF中点。求证：B、I、L共线！

超级画板不给力，虽然给出了将近1500条“不平凡结论”，但却没有给出B、I、L共线的结论！这说明，自动推理功能并非是一把解决几何问题的万能钥匙！

再来尝试一些简单结论。三角形三条中线共点：△ABC三边中点分别是D、E、F，设AD交BF于H；求证：E、H、C共线。三角形三个顶点到对边的垂线共点：△ABC，AJ⊥BC，CK⊥AB，AJ交CK于L；求证：BL⊥AC。超级画板给出的推理过程还是很详细的！