The Automated Geometry Reasoning Network Based on Equivalent Class Reasoning
JIANG JianGuo1,2, ZHANG JingZhong1
1.Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610041 2.School of Mathematics, Liaoning Normal University, Dalian 116029
Abstract To improve the reasoning efficiency of the inference engine, a new inference engine, namely automated geometry reasoning network is presented, into which the Rete pattern matching algorithm and the equivalent class reasoning technique are integrated. The new inference engine is implemented with Lisp and tested with more than 50 nontrivial geometry theorems. The experimental results show that it is more efficient.
[1] Wu W T. On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry. Scientia Sinica, 1978, 21: 157-179 [2] Chou S C. Proving Elementary Geometry Theorems Using Wu’s Algorithm // Bledsoe W W, Loveland D W, eds. Automated Theorem Proving: After 25 Years. AMS Contemporary Mathematics Series, 1984, 29: 243-286 [3] Chou S C, Gao X S, Zhang J Z. Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. Singapore, Singapore: World Scientific, 1994 [4] Chou S C, Gao X S, Zhang J Z. A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 2000, 25(3): 219-246 [5] Zhang Jinzhong, Gao Xiaoshan, Chou Xianqing. The Geometry Information Search System by Forward Reasoning. Chinese Journal of Computers, 1996, 19(10): 721-727 (in Chinese) (张景中,高小山,周咸青. 基于前推法的几何信息搜索系统. 计算机学报, 1996, 19(10): 721-727) [6] Chou S C, Gao X S. Automated Reasoning in Geometry // Robinson A, Voronkov A, eds. Handbook of Automated Reasoning. Amsterdam, Netherlands: Elsevier Science, 2001: 708-749 [7] Gao Xiaoshan, Zhang Jinzhong, Chou Xianqing. Geometry Expert. Beijing, China: China Children’s Press, 1998 (in Chinese) (高小山,张景中,周咸青. 几何专家. 北京: 中国少年儿童出版社, 1998) [8] Li Chuanzhong, Zhang Jinzhong. Super Sketchpad (Version 2.0). Beijing, China: Beijing Normal University Press, 2004 (in Chinese) (李传中,张景中. 超级画板(V2.0). 北京: 北京师范大学出版社, 2004) [9] Noboru M, Kurt V. GRAMY: A Geometry Theorem Prover Capable of Construction. Journal of Automated Reasoning, 2004, 32(1): 3-33 [10] Gelernter H, Hansen J R, Loveland D W. Empirical Explorations of the Geometry Theorem-Proving Machine // Feigenbaum E, Feldman J, eds. Computers and Thought. New York, USA: McGraw-Hill, 1963: 153-163 [11] Nevins A J. Plane Geometry Theorem Proving Using Forward Chaining. Artificial Intelligence, 1975, 6(1): 1-23 [12] Forgy C L. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence, 1982, 19(1): 17-37
2006, Vol. 19 
