張景中院士主持開發的Z+Z智能教育平臺軟件——超級畫板除了具有幾何畫板的所有功能外,還基于我國數學家吳文俊先生所提出的數學機械化的思想,實現了幾何定理可讀性證明的可視化。下面將介紹如何利用超級畫板來真正地推導證明“五點共圓”,而更重要的是該證明的過程完全由計算機來完成。
一、作出五點共圓圖
1.用超級畫板的智能畫筆畫出首尾相連的五條線段AB、BC、CD、DE、EA。
2.繼續使用智能畫筆,將畫筆指向任意兩條線段的交點位置,當出現“相交”字樣時單擊鼠標,從而作出交點F、G、H、I、J。
3.依次選擇A、F、J三點,使用菜單命令“作圖∣圓和圓弧∣過三點的圓”,作出過A、F、J三點的圓。同樣的操作可分別作出過D、G、F,B、G、H,E、H、I,C、I、J的圓。
4.使用智能畫筆作出五個圓的另外一組交點K、L、M、N、P。問題即要證明下圖中的點K、L、M、N、P五點共圓。
二、機器自動證明問題
在完成上述作圖操作后,執行菜單命令“推理∣自動推理”,大約2秒鐘后(這個時間與所使用的計算機的配置有關),屏幕左側變為推理庫工作區:
用鼠標雙擊“共圓或圓上的點信息11條”字樣,會在推理庫工作區出現更多的信息。繼續雙擊最后一條信息“點K、L、M、N、P共圓”,逐步打開結論前的加號,可查看推理的依據,直到信息前的加號全部變為減號。最后鼠標右擊結論“點K、L、M、N、P共圓”,即可在作圖工作區出現“五點共圓問題”的完整推理過程:
參考文獻:
[1]王愛生.用幾何畫板證“五點共圓”[J].中學生數學,2002,9.
[2]李傳中,左傳波.超級畫板范例教程[M].北京:科學出版社,2004.
基金項目:魯東大學—煙臺市教育局校地聯合教學改革項目支持(課題編號412——20101206)。