高中平面几何 [基于超级画板的平面几何自动推理]

　　摘要：如何利用计算机进行几何定理的自动证明，是学术界长期研究的课题。本文从直接启动自动推理、增加条件或结论的推理以及设置推理规则的推理三个方面对张景中院士领衔开发的Z+Z智能教育平台——超级画板软件的功能展开论述，并举例介绍三种方法的操作过程。
　　关键词：超级画板；平面几何；自动推理
　　中图分类号：G642.3 文献标识码：A 文章编号：1674-9324（2012）07-0177-02
　　数学机械化研究，是在初等几何定理的机器证明研究方面取得突破的。以中学课程中的几何为例，－个定理的证明，往往要经过冥思苦想，奇巧构思，无章可循地添加辅助线，迂回曲折地给出证明。这确实难坏了很多人。因此，如何利用计算机进行几何定理的自动证明，就成为学术界长期研究的课题。张景中院士领衔开发的Z+Z智能教育平台——超级画板，就是基于数学机械化的思想，充分利用几何定理及其证明的理论与算法的最新技术，结合现代化的教育思想，将自动推理这一科学技术领域最前沿的成果成功地应用于数学教学之中，将几何定理的可读性证明转化为可视化的产物，为基础数学教育改革注入了新的活力。本文就平面几何的自动推理展开论述，介绍超级画板的这一功能。
　　一、直接启动“自动推理”
　　对于一些较简单的题目，在作好图形后直接执行“推理→自动推理”命令，计算机推理结束后，会将所有得到的与图形有关的结论以信息树的形式显示在工作区的推理库中。其信息量是非常大的，有时是上百条甚至几百条。我们可从列举的信息中选出与题目问题有关的信息。这个过程不但可以系统复习学过的数学知识，而且可以学习如何从庞杂的信息中筛选有用的信息。所以超级画板的自动推理功能是学生学习的得力助手。
　　例1 设任意△ABC的三边中点D、E、F组成△DEF，证明CFDE是平行四边形。
　　（1）依题意画图，如图1所示。
　　图1 图2
　　（2）单击“推理→自动推理”，工作区自动变为“推理库”。
　　（3）寻找有用信息：“推理库”第一行显示“共258条非平凡信息”，从下面的信息中找到“平行四边形信息共3条”，打开前面的“+”，找到“CFDE是平行四边形”，打开前面以及下面的“+”，出现图2的信息。
　　（4）打印证明过程：从图2的信息中已经明白证明方法，右键单击图2中的“EFGH是平行四边形”，在作图工作区打印出证明过程。
　　在例1的推理过程中，计算机是根据作图过程中所产生的几何关系进行推理，而题目中的几何关系是非常多的，因此计算机推出了很多关系任我们选择。所以说，超级画板不仅可替我们做题，而且为我们提供除解题之外的其他信息。
　　二、增加条件或结论
　　像例1那样有明显特征的题目，能找到我们需要的“平行四边形”信息。但对于难一点的题目，计算机可能找不到我们需要的信息，这时可以手工增加辅助条件，也就是告诉计算机需要增加的条件或所要证明的结论，计算机将增加的辅助条件当作已知条件进行推理。
　　例2 在四边形ABCD中，∠A=90°，AD=4，连接BD，BD⊥CD，∠ADB=∠C，若F是BC边上一动点，则DF长的最小值是多少？
　　先画出图形如图3所示，如果直接单击“推理→自动推理”，推理库中没有我们需要的“线段值”的信息。因为计算机不知道我们要求它计算线段DF的值，所以直接启动自动推理功能没法解决，需要给计算机提供已知条件和结论，再启动自动推理功能。过程如下：（1）单击“推理→添加辅助条件或结论”，在弹出的“增加条件或结论对话框”中，增加第一个条件“∠A=90°”：在条件类型框中选择“角的值”；选择对象为“点B、A、D”； 将编辑表达式“（anglevalue B A D）”修改为“（anglevalue B A D 90）”。（2）增加第二个条件“AD=4”：条件类型选择“线段的值”；选择对象为“点A、D”；将编辑表达式“（segmentvalue A D）”修改为“（segmentvalue A D 4）”。（3）增加第三个条件“BD⊥CD”：条件类型选择“直线垂直”；选择对象为“点B、D、C、D”。（4）增加第四个条件“∠ADB=∠C”：条件类型选择“角相等”；选择对象为“点A、D、B、B、C、D”。（5）增加第五个条件“DF⊥BC”（因为垂直时距离最短）：条件类型选择“直线垂直”；选择对象为“点D、F、B、C”。（6）增加结论“DF的值”：结论类型选择“线段的值”；选择对象为“点D、F”。（7）单击“推理→自动推理”，则推理库中有“线段的值”信息，打开它前面的“+”，有“DF=4”的结论。打开它前面和下面所有的“+”，就是结论“DF=4”的推理依据（图4）。
　　图3 图4
　　从图3可以看出，AD与DF画得并不相等，但计算机还是推出了它们相等。这说明我们画图并不需要特别精细，只要图形大致类似，计算机会结合我们给定的辅助条件和结论进行智能推理，这为我们省去了很多时间。
　　三、设置推理规则和方法
　　超级画板自动推理的依据是初中平面几何的所有公理和定理。这就有一个问题，即平面几何知识没学完，如果不告诉计算机学习进度的话，它会用到四边形、相似形、解直角三角形甚至圆的知识来解题。所以需要告诉计算机必须用什么知识来解题。
　　例3 在梯形ABCD中，AB∥CD，若EA=EB，EC=ED，问梯形ABCD是等腰梯形吗？（1）依题意画图，如图5所示。（2）设置推理规则：单击“推理|设置推理规则”，在弹出的设置推理规则对话框中，选择“四边形” 。（3）增加已知和结论：单击“推理/添加辅助条件或结论”，在弹出的对话框中，①选择条件类型“直线平行”，选择对象“点C、D、A、B”；②选择条件类型“线段相等”，选择对象“点E、A、E、B”；③再选择对象“点E、C、E、D”；④选择结论类型“等腰梯形”，选择对象“点C、D、A、B”。（4）推理：单击“推理/自动推理”，计算机将推理步骤列出。从中找到“等腰梯形信息共1条”，打开下面的所有“+”，就是需要的执果索因的证明过程（图6）。
　　图5 图6
　　利用超级画板中的自动推理技术，把中学数学教师从繁重的备课任务中解放出来，也给了学生自主学习的机会，学生可以在家里利用计算机帮助自己找到合适的解题方法。这样，教师教得幸福，学生学得快乐，达到共赢的效果。