[1]WU W. On the decision problem and the mechanization of theorem-proving in elementary geometry[J]. Science China: Mathematics, 1978, 21(2): 159-172.
[2]CHOU S C. Proving and discovering theorems in elementary geometries using Wu's method[D]. Austin: University of Texas, 1985.
[3]KAPUR D. Using Grbner bases to reason about geometry problems [J]. Journal of Symbolic Computation, 1986, 2(4): 399-408.
[4]KAOUR D, SAXENA T, YANG L. Algebraic and geometric reasoning using dixon resultant[C]// Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation. New York: ACM, 1994: 99-107.
[5]HONG J. Can we prove geometry theorem by computing an example[J]. Science China: Series A, 1986, 16(3): 234-243.(洪加威.能用例证法来证明几何定理吗[J].中国科学: A辑, 1986, 16(3): 234-243.)
[6]DENG M. The parallel numerical method of proving the constructive geometric theorem[J]. Chinese Science Bulletin, 1989, 34(31): 1066-1070.
[7]ZHANG J, YANG L, DENG M. The parallel numerival methods in mechanical theorem proving[J]. Theoretical Computer Science, 1990, 74(3): 253-271.
[8]YANG L, ZHANG J, LI C. A prover for parallel numerical verification to a class of constructive geometirc theorems[J]. Journal of Guangzhou University: Nature Science Edition, 2002, 1(3): 29-34.
[9]HOU X. Proving by examples[C]// Mathematics Mechanization and Application. London: Academic Press, 2000:231-251.
[10]ZHANG J. How does computer solve geometry problems: talking about automated reasoning [M]. Guangzhou: Jinan University Press, 2000.(张景中.计算机怎样解几何题:谈谈自动推理[M].广州: 暨南大学出版社, 2000.)
[11]CHOU S-C, GAO X-S, ZHANG J-Z. Machine proofs in geometry [M]. Singapore: World Scientific,1994.
[12]YANG L, GAO X S, CHOU S-C, et al. Automated proving and discovering of theorems in non-Euclidean geometries[C]// Automated Deduction in Geometry. Berlin: Springer-Verlag, 1998: 171-188.
[13]LI C, RUAN W, ZHANG L, et al. Mathmatical theory of computer algebra system [M]. Beijing: Tsinghua University Press, 2010. (李超,阮威,张龙,等. 计算机代数系统的数学原理[M]. 北京: 清华大学出版社, 2010.)
[14]CARR FERRO G, GALLO G, GENNARO R. Probabilistic verification of elementary geometry statements[C]// Workshop on Automated Deduction in Geometry. Berlin: Springer-Verlag, 1997, 1360: 87-101.
[15]SCHWARTZ J T. Fast probabilistic algorithms for verification of polynomical identities[J]. Journal of Association for Computing Machinery, 1980, 27(4): 701-717.
[16]BROWNAWELL W D. Bounds for the degrees in the Nullstellensatz[J]. Annals of Mathematics, 1987, 126:577-591.
[17]KOLLAR J. Sharp effective Nullstellensatz[J]. Journal of the American Mathematical Society, 1988, 1(4): 963-975.
[18]GALLO G, MISHRA B. Efficient algorithm and bounds for Wu-Ritt characteristic sets[J]. Progress in Mathematics, 1990, 94: 119-142.
[19]GALLO G, MISHRA B. Wu-Ritt characteristic sets and their complexity[J]. Mathematics and Theoretical Computer Science, 1991, 6: 111-136.
[20]TULONE D, YAP C, LI C. Randomized zero testing of radical expression and elementary geometry theorem proving [C]// Proceedings of the 3rd International Workshop on Automated Deduction in Geometry. Berlin: Springer, 2001: 58-82.
[21]Index of /exact/core[EB/OL].[2013-10-10].http: //cs.nye.edu/exact/cpre/.
[22]YANG L, ZHANG J, HOU X. Nonlinear algebraic equations and theorem machine prove [M]. Shanghai: Shanghai Scientific and Techincal Publishers, 1996. (杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明[M].上海:上海科技教育出版社,1996.)
[23]WANG D, YANG L, LI Z. Selected lectures in symbilc computation [M]. Beijing: Tsinghua University Press, 2003.(王东明, 杨路, 李志斌.符号计算选讲[M].北京:清华大学出版社, 2003.)
[24]CHOU S-C. An indroduction to Wu's method for mechanical theorem proving in geometry[J]. Journal of Automate Reasoning, 1988,4(3):237-267.
[25]CHOU S-C. Mechanical geometry theorem proving [M]. Dordrecht: Reidel Publishing Company, 1988.
[26]WANG D. A new theorem discovered by computer prover [J]. Journal of Geometry, 1989, 36(1/2): 173-182. |