Wu W T. On the Decision Problem and the Mechanization ofTheorem 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
Li Chuanzhong, Zhang Jinzhong. Super Sketchpad (Version 2.0). Beijing, China: Beijing Normal University Press, 2004 (in Chinese) (李传中,张景中. 超级画板(V2.0). 北京: 北京师范大学出版社, 2004)
[9]
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
[10]
Nevins A J. Plane Geometry Theorem Proving Using Forward Chaining. Artificial Intelligence, 1975, 6(1): 1-23
[11]
Forgy C L. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence, 1982, 19(1): 17-37
[12]
Noboru M, Kurt V. GRAMY: A Geometry Theorem Prover Capable of Construction. Journal of Automated Reasoning, 2004, 32(1): 3-33