2超级画板的自动推理功能.doc

超级画板的自动推理功能简介 张景中 彭翕成 武汉 华中师范大学教育信息技术工程研究中心 430079使用动态几何软件，可以在计算机屏幕上画出所谓的动态几何图形：在拖动图中某些点或某些线时，图形在变动中能保持当初作图时被赋予的几何属性不变。中点仍是中点，垂线仍是垂线，等等。通过几何图形的动态变化，可体现以前在纸上无法观测到的几何原理，使人能更直观地深刻理解图形中的几何规律，从而达到真正理解几何原理的目的。同时，也可利用动态几何提供的各种作图功能，根据所学的几何原理画出变化无穷的几何图形，真正体验几何的美妙，提高学生的学习兴趣和教师的教学效果。关于动态几何的机理，1中有比较详细地论述。第一个动态几何软件GSP2出现于1987年；到目前为止，全世界已经有几十种动态几何软件，其中广为人知的有2，3，4等。动态几何对教育的积极影响，已经成为国际教育界的共识。但数学教育不仅有几何，还有算术，代数和分析；几何也不仅仅是作图看图，还有推理和计算。为了满足数学教育的需求，人们希望动态几何软件能够集成更多的功能，并且希望使用起来更加容易和快捷。例如，在5和6中都提出了并致力于把几何作图和推理组合在一起的问题。在7中介绍了致力于把代数和分析功能和动态几何作图组合起来软件Geogrbra。在8中提出未来的数学软件应当更容易使用和更智能化。智能教育平台超级画板是一个集动态几何、符号运算、编程环境、自动推理等多项功能为一体的综合性平台，具有“人性化，智能化，可视化，动态化和程序化”等特点，对于上面的这些要求都作了考虑并尽可能地予以落实，而且还根据教学需要，增加了很多功能，详见文9。在谈谈计算机怎样解几何题一文中，我们介绍了计算机解几何题的相关知识，并举例说明了智能软件超级画板自动推理得到的证明和人工的传统风格的证明基本上是一致的。本文将列举更多实例，介绍超级画板的自动解题功能，也让大家了解一下现代信息技术的发展情况。 例1：如图1，在ABC中，F、G分别是DE、BC的中点，求。 求证：GFE = 90证明：0: DCBA1: BDC是直角三角形 (0)2: G是BC的中点3: BG = DG (2 1)4: BEAC5: BEC是直角三角形 (4)6: BG = EG (2 5)7: EG = DG (3 6)8: GDE是等腰三角形 (7)9: F是DE的中点10: DEGF (9 8)11: GFE = 90 (10) 图1 图2例2：如图2，在正方形ABCD中，AC和BD交于点E，点F是BD上一点，交AC于H，求证：。证明：0: ACDB1: DGAF2: 点F, E, G, H共圆 (0 1)3: AFB = GHC (2)4: DHA = GHC5: AFB = DHA (4 3)6: DEA = CED7: DE = AE8: AFEDHE (6 5 7)9: FE = EH (8) 例1和例2取自教科书的配套习题册，难度不是很大，但这种难度的题目正是广大中学生需要解决的。下面给出的例3、例4和例5难度则要大一些。例3：如图3，AD是ABC的中线，过DC上任意一点E作，与AC和AD延长线分别交于点F、G，交AB于点H，求证：BG = FH。（1990年四川省初中数学竞赛试题）证明：0: EFBA1: BFG = FBA (0)2: D是BC的中点3: BD = CD (2)4: HEAC5: AD/AI=CD/CE (4)6: AD/AI=BD/CE (3 5)7: AD/AG=BD/BE (0)8: AG/AI=BE/CE (6 7)9: AG/FG=GI/EG (4)10: AH/AI=EG/GI (0)11: AG/AI=FG/AH (9 10)12: AH/CE=FG/BE (8 11)13: AH/BH=CE/BE (4)14: BH = FG (12 13)15: BFGFBH (1 14)16: BG = FH (15) 图3 图4例4：如图4，设凸四边形ABCD的对角线交于点E。ABE和CDE的外接圆交于E、F两点，ADE和BCE的外接圆交EF直线于G、H两点，求证：F是GH的中点。（2006年女子奥林匹克试题）证明：0: CBD = CHG1: HFC = BDC2: BCDHCF (0 1)3: BD/CD=FH/CF (2)4: FBA = HEC5: FDC = HEC6: FDC = FBA (4 5)7: AFB = CED8: CFD = CED9: CFD = AFB (7 8)10: ABFCDF (6 9)11: AB/AF=CD/CF (10)12: AB/AF=BD/FH (3 11)13: ADB = AGH14: DBA = GFA15: ABDAFG (13 14)16: AB/AF=BD/FG (15)17: FG = FH (12 16)18: F是GH的中点 (17)例5：如图5，在中，过A、B、C三点作圆交BD于E，过B、C、D三点作圆交CA延长线于F。求证：。 例5 证明：0: 点B, C, D, F共圆1: BFC = BDC (0)2: ABCD是平行四边形3: ABCD (2)4: DBA = BDC (3)5: DBA = BFC (1 4)6: 点A, B, C, E共圆7: AEB = FCB (6)8: ABEBFC (5 7)9: AB/BE=BF/CF (8)10: DBF = DCF (0)11: BAC = DCF (3)12: BAC = DBF (10 11)13: FCB = FDB (0)14: ABCBFD (12 13)15: AB/AC=BF/BD (14)16: AC/BD=BE/CF (9 15)此题是数学通报2007年第7期数学问题解答栏目的问题1683。原证法用到三角形相似和托勒密定理，而托勒密定理是现在的初中生不太熟悉的，超级画板自动生成的证明只用到了三角形相似，而且证明过程也比原作者提供的证明简单。这说明计算机自动生成的证明完全可以和人工证明相媲美。众所周知，有一些几何题，如果要求纯几何证明，中间不用代数运算的话，证明过程会变得相当复杂。很多数学爱好者即使用代数计算证明出题目之后，还是希望找到纯几何证明。而超级画板所提供的恰恰是纯几何证明，如果嫌其过程繁琐，可以在看懂证明思路之后，再作简化。因为计算机解题“规规矩矩，相当老实”，此时就需要再加工。用超级画板推导例6和例7，证明较长，但经过笔者的加工，可得到较精简的证法（由于加工后的证法不具一般性，此处省略）。例6：如图6，已知CH是RtABC的高（C= 90），且与角平分线AM，BN分别交于P，Q两点。QN，PM的中点分别是E，F。证明：。（第52届白俄罗斯数学奥林匹克（决赛A类） 图6 图7例7：如图7，圆和圆相交于B、C两点，且BC是圆的直径，过点C作圆的切线，交圆于另一点A，连接AB交圆于另一点E，连接CE并延长，交圆于点F。设点H为线段AF上的任意一点，连接HE并延长，交圆于点G，连接BG并延长与AC的延长线交于点D，求证：（2002年中国女子数学奥林匹克）。例8：如图8，作出五角星ABCDE，产生5个交点G、H、I、J、F；再分别作AGF、DHG、BIH、EJI、CFJ的外接圆；这5个圆生成5个新的交点M、N、P、K、L；求证：M、N、P、K、L五点共圆。 图8例8是一道经典的平面几何问题，难度较大。江泽民主席在澳门视察工作时，曾给中学生出过这道题。从证明的结构图来看，要证五点共圆，只需证两次四点共圆。根据结构图，我们可以比较容易地整理出证明过程。辅助线在证明几何题中所起的作用是不言而喻。但添加辅助线属于人的高级智慧，需要“灵机一动”，目前的计算机在这一点上还属于很初级的水平，但我们也在作一些尝试和努力，而且已经有了初步成果，否则很多题目是不可能解答出来的。譬如，在推导例6和例8的过程中，超级画板会自动弹出一个对话框“DO you append auxiliary-line？（需要添加辅助线么？）”，此时选择“（是（Y）”计算机就会自动添加一些可能的辅助线。有时，一些题目用自动推理不能直接到位，但并不能因此就否定自动推理。我们可以将已经推导出的一些信息加工整理，进行交互性解题。下面给出这样的两个例子。例9：如图9，已知ABD中，两高AF、DC交于点G，ABCD，点E是AB中点。求证：。此题用超级画板自动推理不能直接到位。但可推导出，将与其他已知条件输入程序区，最后输入需要计算的，执行之后即可得结果（图10），这说明超级画板的符号运算功能对自动推理起到了很大的帮助。 图9 图10 笔者的朋友在上海介绍超级画板的时候，一位老师提出了下面这个问题。例10：如图11，已知ABCD为菱形，点E为BC延长线上的一点，连接并延长ED使之与BA直线交于点F，点G是AE和FC的交点。求证：。 图11证明：0: AB = AC1: AB/AF=DE/DF2: AC/AF=DE/DF (0 1)3: BC = AC (0)4: BC/CE=DF/DE5: AC/CE=DF/DE (3 4)6: AC/AF=CE/AC (2 5)7: ECA = CAF8: ACEFAC (7 6)9: AEB = FCA (8)10: AEB = EAD11: FCA = EAD (10 9)12: DAF = ACB13: FCB = EAF (11 12)14: BAE+EAF = 18015: BAE+FCB = 180 (13 14)经尝试发现直接推导不能实现，但可以推导出。我们将之与已知条件结合起来，轻松解出。需要说明的是，我国自主研发的智能教育平台系列产品的自动推理功能相当强大，在全世界都属于领先水平；不单是本文所介绍的解决平面几何问题，还可以解决解析几何，立体几何问题以及三角函数化简求值问题。而另一方面，由于从计算机的发明到现在也只有几十年的时间，人工智能的发展还处于起步阶段。尽管在人工智能的各个分支中，计算机解几何题的研究相对完善一些，但还有大量的工作等着我们去做。至于自动推理功能会给中学数学教学带来什么新的变化，我们将另撰他文探讨。参考文献：1 Ulrich Kortenkamp. Foundations of Dynamic Geometry. Federal Institute of Technology Zurich, Dipl -Math Swiss, 1999. 2 Nicholas Jackiw. The Geometers Sketchpad. Key Curriculum Press, Berkeley, 19911995. 3 Jean-Marie Laborde and Franck Bellemain. Cabri-Geometry II. Texas Instruments, 19931998. Copyright Texas Instruments and Universite Joseph Fourier, CNRS.4 Jurgen Richter-Gebert and Ulrich Kortenkamp. The interactive geometry software Cinderella. Book & CD-ROM, Springer-Verlag, Berlin Heidelberg New York, 1999. First commercial release of the Cinderella software.5 Kortenkamp, U. and J. Richter-Gebert, Using automatic theorem proving to improve the usability of geometry software, in: Mathematical User Interfaces, 2004.6 Sean Wilson and Jacques D. Fleuriot, Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs, Email: sean.wilsoned.ac.uk , jacques.fleurioted.ac.uk7