限制条件下的几何自动推理及应用研究
|
摘要
几何学具有悠久的历史,两千多年来积累下来的几何知识是人类的宝贵财富。其中,几何证明是几何学的精华之一。几何题的证法,没有统一的方法可依循,有赖于个人的灵感和技巧,一直是数学教学中的难点和重点内容。用机器来模仿人的思维活动,来帮助人证明几何命题,是历史上一些卓越科学家的梦想,也是具有重要研究价值和应用价值的研究方向。吴文俊建立的数学机械化方法,极大的推动了几何定理机器证明领域的研究。目前,基于不同推理算法的自动推理系统已经出现,在科学研究和工程计算中发挥着重要的作用。
但是,几何定理自动推理领域中的丰富成果,在教育中并没有得到充分应用,其教育价值远远没能得到充分体现。原因一方面在于中学教育阶段涉及到的几何知识比较初等,而现有的几何自动推理方法给出的证明过程难于被中学生理解；另一方面,几何知识的教学又涉及语言表达与作图、从图形发现问题、问题分析与解答等多个方面,不仅仅是单纯的几何定理机器证明。面对中学几何教学的应用需求,几何自动推理的研究面临着中学几何知识范围、解答步骤长度、推理时间和推理方法等多方面的限制。针对这些限制条件,本文开展了面向中学几何教学的几何自动推理的研究工作,涉及几何自动推理在动态几何作图、几何问题生成、向量法解题等方面的理论方法与应用,研究成果(创新点)包括以下几个方面：
第一：提出动态几何作图中的枢点概念,建立了以枢点为基础的动态几何机制,设计了包括智能作图方法,语义作图方法和文本作图等几何作图方法。实现了相应的动态几何作图系统,拓展了动态几何理论。
第二：提出并实现基于向量法的自动推理算法。该自动推理方法基于向量的回路特征,对构造型交点类几何命题能迅速地给出可读的向量式证明,证明过程简洁优美。这种自动推理方法能够在限制条件内能达到推理不动点,在构造型交点类的题目上表现出较高的效率。
第三：提出并实现了基于自动推理的几何问题自动生成与答案验证方法。以自动推理为基础,设计了可以生成填空、判断、选择、计算和证明等多种题型的自动出题方法,并实现对用户的解答进行实时验证。这种方法创新了几何学出题方式,提高了测试效率。
综合应用上述研究成果,实现了一个面向中学教学应用的几何自动推理原型系统,其主要功能包括动态几何作图、几何自动推理和题目自动生成。这三种主要功能有机集成,可满足教师课堂教学和学生课下自学的需求。
最后提出了值得进一步研究的问题和对此方向未来的展望。
With a long history, the knowledge of geometry is a valuable wealth of mankind, which has accumulated two thousand years. In which, the proof of geometry is one of the elites. The proving methods with no uniform methods have been a difficult and key content in mathematics teaching, which depend on the personal inspiration and skills. Using machines to mimic human thinking to help people prove geometric propositions is the dream of some of the outstanding scientists in history, but also has important value of research and application. Wu-method greatly contributes to geometry theorem proving research in the field. Currently, the automated reasoning systems based on different reasoning algorithms has emerged in scientific research and engineering calculations and it plays an important role.
However, the rich achievements of the field of automated reasoning in geometry theorem have not been fully applied in education, their educational value is far failed to be fully reflected. The reason is that, on the one hand, the knowledge of geometry in secondary education is elementary compared to mathematics, the given process by existing methods of automated reasoning of geometry is so difficult that students couldn't understand. On the the other hand, knowledge of geometry teaching involves the expression and construction of geometry, generating geometric problem from given construction, analysis and solving for a problem and other aspects, not just a simple geometric theorem proving. For the application requirements of geometry teaching in high schools, the study of geometry automated reasoning faces the restrictions of the scope of geometry knowledge in secondary schools, the length of working steps, time and reasoning methods. In response to these limitations, this paper carried out the research on automated reasoning about the teaching of geometry in secondary schools, which involves the theory and application of the dynamic geometry construction, generating geometry problem, problem-solving with vector approach and other aspects, the research results and innovation include the following:
First:this paper proposes the pivot concept in dynamic geometry construction and the dynamic geometry mechanism based on the pivot idea. Several methods of the dynamic geometric construction based on pivot concept have been designed, which include the manual method of intelligent construction, semantic construction and construction method of the text. The function of dynamic geometric construction in a prototype system has been implemented, and it extends the thoeries of dynamic geometry.
Second:the paper proposes and implements automated reasoning algorithms based a vector method. The method is based on the characteristics of the vector loop, which can quickly generate the readable vector-proof of given proposition with the constructed type and intersection class for students, and the proof is simple and readable. This method of automated reasoning can achieve a fixed point, and it shows higher efficiency in a large class of subjects.
Third:The paper proposes and implements an automated method of generation and verification for a given geometric proposition based on automated reasoning. The mechanism of multi-kinds of questions and verification based on automated reasoning are constructed. It can generate several kinds of exercises such as filling in the blank, judgement, choose, calculation and proof, which can certificate the problem of real-time answers for users. This provides a solution for generating geometry exercises and improves the efficiency for test.
Integrating the application of above research results, an automated geometry reasoning prototype system under constrained conditions has been programmed in this paper. The system is concerned with the limits and methods of the scope of geometry knowledge in high school, its main features include:the dynamic geometry construction, automated reasoning and automated generation of geometric exercises. The organic integration of the three main functions could satisfy the classroom teaching by teachers and self-study courses by students.
Finally, a question worthy of further study and future prospects for this direction are concluded.
但是,几何定理自动推理领域中的丰富成果,在教育中并没有得到充分应用,其教育价值远远没能得到充分体现。原因一方面在于中学教育阶段涉及到的几何知识比较初等,而现有的几何自动推理方法给出的证明过程难于被中学生理解；另一方面,几何知识的教学又涉及语言表达与作图、从图形发现问题、问题分析与解答等多个方面,不仅仅是单纯的几何定理机器证明。面对中学几何教学的应用需求,几何自动推理的研究面临着中学几何知识范围、解答步骤长度、推理时间和推理方法等多方面的限制。针对这些限制条件,本文开展了面向中学几何教学的几何自动推理的研究工作,涉及几何自动推理在动态几何作图、几何问题生成、向量法解题等方面的理论方法与应用,研究成果(创新点)包括以下几个方面：
第一：提出动态几何作图中的枢点概念,建立了以枢点为基础的动态几何机制,设计了包括智能作图方法,语义作图方法和文本作图等几何作图方法。实现了相应的动态几何作图系统,拓展了动态几何理论。
第二：提出并实现基于向量法的自动推理算法。该自动推理方法基于向量的回路特征,对构造型交点类几何命题能迅速地给出可读的向量式证明,证明过程简洁优美。这种自动推理方法能够在限制条件内能达到推理不动点,在构造型交点类的题目上表现出较高的效率。
第三：提出并实现了基于自动推理的几何问题自动生成与答案验证方法。以自动推理为基础,设计了可以生成填空、判断、选择、计算和证明等多种题型的自动出题方法,并实现对用户的解答进行实时验证。这种方法创新了几何学出题方式,提高了测试效率。
综合应用上述研究成果,实现了一个面向中学教学应用的几何自动推理原型系统,其主要功能包括动态几何作图、几何自动推理和题目自动生成。这三种主要功能有机集成,可满足教师课堂教学和学生课下自学的需求。
最后提出了值得进一步研究的问题和对此方向未来的展望。
With a long history, the knowledge of geometry is a valuable wealth of mankind, which has accumulated two thousand years. In which, the proof of geometry is one of the elites. The proving methods with no uniform methods have been a difficult and key content in mathematics teaching, which depend on the personal inspiration and skills. Using machines to mimic human thinking to help people prove geometric propositions is the dream of some of the outstanding scientists in history, but also has important value of research and application. Wu-method greatly contributes to geometry theorem proving research in the field. Currently, the automated reasoning systems based on different reasoning algorithms has emerged in scientific research and engineering calculations and it plays an important role.
However, the rich achievements of the field of automated reasoning in geometry theorem have not been fully applied in education, their educational value is far failed to be fully reflected. The reason is that, on the one hand, the knowledge of geometry in secondary education is elementary compared to mathematics, the given process by existing methods of automated reasoning of geometry is so difficult that students couldn't understand. On the the other hand, knowledge of geometry teaching involves the expression and construction of geometry, generating geometric problem from given construction, analysis and solving for a problem and other aspects, not just a simple geometric theorem proving. For the application requirements of geometry teaching in high schools, the study of geometry automated reasoning faces the restrictions of the scope of geometry knowledge in secondary schools, the length of working steps, time and reasoning methods. In response to these limitations, this paper carried out the research on automated reasoning about the teaching of geometry in secondary schools, which involves the theory and application of the dynamic geometry construction, generating geometry problem, problem-solving with vector approach and other aspects, the research results and innovation include the following:
First:this paper proposes the pivot concept in dynamic geometry construction and the dynamic geometry mechanism based on the pivot idea. Several methods of the dynamic geometric construction based on pivot concept have been designed, which include the manual method of intelligent construction, semantic construction and construction method of the text. The function of dynamic geometric construction in a prototype system has been implemented, and it extends the thoeries of dynamic geometry.
Second:the paper proposes and implements automated reasoning algorithms based a vector method. The method is based on the characteristics of the vector loop, which can quickly generate the readable vector-proof of given proposition with the constructed type and intersection class for students, and the proof is simple and readable. This method of automated reasoning can achieve a fixed point, and it shows higher efficiency in a large class of subjects.
Third:The paper proposes and implements an automated method of generation and verification for a given geometric proposition based on automated reasoning. The mechanism of multi-kinds of questions and verification based on automated reasoning are constructed. It can generate several kinds of exercises such as filling in the blank, judgement, choose, calculation and proof, which can certificate the problem of real-time answers for users. This provides a solution for generating geometry exercises and improves the efficiency for test.
Integrating the application of above research results, an automated geometry reasoning prototype system under constrained conditions has been programmed in this paper. The system is concerned with the limits and methods of the scope of geometry knowledge in high school, its main features include:the dynamic geometry construction, automated reasoning and automated generation of geometric exercises. The organic integration of the three main functions could satisfy the classroom teaching by teachers and self-study courses by students.
Finally, a question worthy of further study and future prospects for this direction are concluded.
引文
[1]Wen-Tsun Wu. On the decision problem and the mechanization of theorem-proving in elementary geometry[J]. Scientia Sinica,1978,21:159-172.
[2]吴文俊.几何定理机器证明的基本原理(初等几何部分)[M].北京：科学出版社,1984.8：280.
[3]S. C. Chou,X. S. Gao,J. Z. Zhang. Automated generation of readable proofs with geometric invariants.1. Multiple and shortest proof generation[J]. Journal of Automated Reasoning,1996,17(3): 325-347.
[4]S. C. Chou,X. S. Gao,J. Z. Zhang. Automated generation of readable proofs with geometric invariants.2. Theorem proving with full-angles[J]. Journal of Automated Reasoning,1996,17(3): 349-370.
[5]Ralph E F.. The use of geometry and proportional reasoning techniques at the US Department of Agriculture[J]. Teaching Mathematics and its Applications,2006,25(1):1.
[6]Bernd F., Geoff S., Stephan S.. Empirically successful automated reasoning:applications issue[J]. Journal of Automated Reasoning,2006,37(1).
[7]J. Harrison. A short survey of automated reasoning[J]. Algebraic Biology,2007:334-349.
[8]MMP-数学机械化自动推理平台.http://www.mmrc.iss.ac.cn/mmp/.
[9]H.Wang. Toward mechanical mathematics[J]. IBM Journal of research and development,1960, 4(1):2-22.
[10]刘江.逻辑学推理和论证[M].第二版.广州：华南理工大学出版社,2010.
[11]D. Kapur. Automated geometric reasoning:Dixon resultants, Grobner bases, and characteristic sets[J]. Automated Deduction in Geometry,1997:1-36.
[12]Chou Shang-Ching. Mechanical Geometry Theorem Proving[M]:D.Reidel Publishing Company, 1988.
[13]S.C. Chou, W.F. Schelter, J.G Yang. An algorithm for constructing Grobner bases from characteristic sets and its application to geometry[J]. Algorithmica,1990,5(1):147-154.
[14]B. Kutzler, S. Stifter. A geometry theorem prover based on Buchberger's algorithm[C],8th International Conference on Automated Deduction Lecture Notes in Computer Science.1986: 693-694.
[15]高小山,张景中,周咸青.几何专家[J].北京：中国少年儿童出版社,1998.
[16]S. C. Chou, X. S. Gao, J. Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Automated Reasoning,2000,25(3):219-246.
[17]Jing Zhong Zhang, Shang Ching Chou, Xiao Shan Gao. Automated Production of Traditional Proofs for Theorems In Euclidean Geometry-the hilbert intersection point theorems[J]. Annals of Mathematics and Artifical Intelligence,1995,13:109-137.
[18]J.-Z. Zhang, L. Yang, X.-S. Gao, et al. Automated production of readable proofs for geometry theorems[J]. Chinese Journal Of Computers,1995,18(5):14.
[19]张景中,高小山,周咸青.基于前推法的几何信息搜索系统[J].计算机学报,1996,19(10)：721-727.
[20]江建国.iGeo_智能几何软件的定理证明器[D].成都：中国科学院成都计算机应用研究所,2006.4：202.
[21]潘斌,郭红霞.几何定理机器证明的并行前向推理[J].华南理工大学学报(自然科学版),2008(04).
[22]郭四稳.基于数据库技术的自动推理系统[D].成都：四川大学,2001.
[23]邹宇.几何代数基础与质点几何的可读机器证明[D].广州：广州大学,2010.5.
[24]郑焕.SGARP:可由用户持续发展的几何自动推理平台[D].广州：广州大学,2011：134.
[25]Gao Xiao-shan, Lin Qiang. MMP/Geometer-a software package for automated gemetry reasoning[M]. Berlin:Springer.2004:44-66.
[26]GeoProof. http://home.gna.org/geoproof/.
[27]The Interactive Geometry Software Cinderella.http://www.cinderella.de/tiki-index.php.
[28]OpenMath. http://www.openmath.org/.
[29]Singular. http://www.singular.uni-kl.de/.
[30]嘉科平面几何. http://down.itl68.com/283/284/45098/index.shtml.
[31]超级画板.http://www.zplusz.org/.
[32]高小山,王定康,裘宗燕.方程求解与机器证明--基于MMP的问题求解[M].北京：科学出版社,2006.9.
[33]Ulrich H. Kortenkamp. Foundations of dynamic geometry[D]. Zurich,Switzerland:Swiss Federal Institute of Technology,1999:15-114.
[34]Y. Bertot, F. Guilhot, L. Pottier. Visualizing geometrical statements with GeoView[C], International Workshop, UITP'03,2003:32.
[35]The Riaca OpenMath Library. http://www.riaca.win.tue.nl.
[36]G. Pfister G.-M. Greuel, and H. Schonemann. A Computer Algebra System for Polynomial Computations[J]. Centre for Computer Algebra, University of Kaiserslautern, http://www.singular.uni-kl.de.,2001.
[37]The Geometer's Sketchpad. http://dynamicgeometry.com/.
[38]张景中.几何定理机器证明20年[J].科学通报.1997,42(21)：2248-2260.
[39]段敏.创新平面几何试题并能自动推理的《数学实验室--平面几何》[J].合肥教学学院学报,2002,19(2)：5-8.
[40]Jing Zhong Zhang, Lu Yang, Mike Deng. The parallel numerical method of mechanical theorem proving[J]. Theoretical computer science,1990,74(3):253-271.
[41]张景中,杨路,高小山.几何定理可读证明的自动生成[J].计算机学报,1995,18(5)：380-393.
[42]Cabri Ⅱ Plus-http://www.cabri.com/cabri-2-plus.html.
[43]蒋鲲.几何自动作图[M].哈尔滨：哈尔滨工业大学出版社,2007.
[44]高小山,蒋鲲.几何约束求解研究综述[J].计算机辅助设计与图形学学报,2004,16(4)：385-396.
[45]高小山,黄磊东,蒋鲲.求解几何约束问题的几何变换法[J].中国科学(E辑),2001,31(2)：182-192.
[46]蒋鲲,高小山,岳晶岩.参数化模型欠、过和完整约束的判定算法[J].软件学报,2003,14(12)：2092-2097.
[47]J. Escribano, F. Botana, M. A. Abanades. Adding remote computational capabilities to Dynamic Geometry Systems[J]. Math. Comput. Simul.,2010,80(6):1177-1184.
[48]C.a.R. http://zirkel.sourceforge.net/.
[49]Euklid. http://www.dynageo.com/.
[50]GCLC/WinGCLC. http://poincare.matf.bg.ac.rs/-janicic//gclc/.
[51]Geometry Epressions. http://www.geometryexpressions.com/.
[52]The Geometric Supposer. http://www.cet.ac.il/math-international/software5.htm.
[53]GeoGebra. http://www.geogebra.org/cms/index.php?lang=zh.
[54]Java Geometry Expert. http://www.cs.wichita.edu/-ye/.
[55]S. S. Choi-Koh. A Student's Learning of Geometry Using the Computer[J]. Journal of Educational Research,1999,92(5):301-311.
[56]R. Sommer, G Nuckols. A proof environment for teaching mathematics[J]. Journal of Automated Reasoning,2004,32(3):227-258.
[57]M. Isiksal, P. Askar. The effect of spreadsheet and dynamic geometry software on the achievement and self-efficacy of 7th-grade students[R]. Educ. Res.,2005,47(3):333-350.
[58]Jing Zhong Zhang, Hui Ming Xiong, Xing Cheng Peng. Free Software SSP for Teaching Mathematics[J]. Symbolic computation and Education,2007.
[59]B. Guven, T. Kosa. The effect of dynamic geometry software on student mathematics teachers' spatial visualization skills[J]. Turk. Online J. Educ. Technol.,2008,7(4):100-107.
[60]吴文渊,曾振柄,符红光.基于Ontology的平面几何知识库设计[J].计算机应用.2002,22(3)：10-14.
[61]钟秀琴,符红光,余莉等.基于本体的几何学知识获取及知识表示[J].计算机学报,2010,33(1)：167-174.
[62]余莉,符红光.基于自然语言处理的计算机几何作图[J].计算机应用,2005,25(1)：7-10.
[63]Qiang Ge, Xicheng Peng, Mao Chen. Introduction to retrieval knowledge using intelligent education software[C]. The 2nd International Symposium on Knowledge Acquisition and Modeling,2009:148-151.
[64]郭四稳.基于动态作图的化学符号编辑系统[J].广州大学学报：自然科学版,2006.12,5卷(6期)：19-22.
[65]Wu WenTen. Mathematics Mechanization. Kluwer:Science Prss,2000.
[66]B. Kutzler. Algebraic approaches to automated geometry theorem proving[J]. Ph. I) thesis, RISC-Linz, Johannes Kepler University, Austria,1988.
[67]产生式.http://baike.baidu.com/view/1308820.htm.
[68]何援军.计算机图形学[M].第二版.北京：机械工业出版社.2009：16.
[69]Mark de Berg, Otfried Cheong, Marc van Kreveld, et al计算几何：算法与应用[M].北京：清华大学出版社,Springer,2009:19.
[70]张景中,彭翕成.动态几何教程[M].北京：科学出版社,2007.9.
[71]Geometry Expressions Homepage, http://www.geometryexpressions.com/.
[72]郑逢斌.计算机理解自然查询语言的研究和实现[D].成都：西南交通大学,2004.
[73]朱创录.基于语义Web的自动推理技术研究[D].西安：西北大学,2006.4.
[74]刘伟,符红光,佘莉.基于语义的几何知识库搜索引擎的设计与实现[J].计算机应用,2007,27(6)：76-78.
[75]杨宗凯.国家高技术研究发展计划(863计划)课题自验收报告：知识浓缩与融合关键技术研究[R].武汉：华中师范大学,2011：10-12.
[76]边肇祺.模式识别[M].第二版.北京：清华大学出版社,2000.
[77]张景中,江春莲,彭翕成.《动态几何》课程的开设在数学教与学中的价值[J].数学教育学报,2007,16(3)：5.
[78]张景中,彭翕成.三款数学教育软件的比较与设计思想分析[J].中国电化教育,2010(276)：107-113.
[79]人民教育出版社,课程教材研究所,中学数学课程教材研究开发中心.数学(2)[M].第二版.北京：人民教育出版社,2007：39-144.
[80]Arthur J. Nevins. Plane Geometry Theorem Proving Using Forward Chaining[J]. Artifical Ingelligence,1974, Volume 6, Issue 1:P303-338.
[81]Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang. Automated geometry theorem proving by vector calculation [J]. Proceedings of the 1993 international symposium on Symbolic and algebraic computation,1993, ACM New York, NY, USA:284-291.
[82]S. Stifter. Geometry theorem proving in vector spaces by means of Grobner bases[C]. the 1993 International Symposium on Symbolic and Algebraic Computation,1993:301-310.
[83]孙熙椿.几何定理计算机证明[M].北京：科学出版社,2007：11.
[84]I.M. Yaglom.九种平面几何[M].上海上海科学技术出版社,1955-1956：358.
[85]张顺燕.推理与证明[M].北京：高等教育出版社,2006：167-168.
[86]张景中,彭翕成.论向量法解几何问题的基本思路[J].数学通报,2008,47(2)：6-10.
[87]张景中,彭翕成.论向量法解几何问题的基本思路(续)[J].数学通报.2008,47(3)：31-36.
[88]陈胜利.向量与平面几何证题[M].北京：中国文史出版社,2003：33.
[89]张景中,彭翕成.绕来绕去的向量法[M].北京：科学出版社,2010.9：287.
[90]人民教育出版社,课程教材研究所,中学数学课程教材研究开发中心.数学(4)[M].第三版.北京：人民教育出版社,2007：73-122.
[91]周培德.计算几何：算法设计与分析[M].第三版.北京：清华大学出版社,2008：41.
[92]余祥宣,崔国华,邹海明.计算机算法基础[M].第三版.武汉：华中科技大学出版社,2006：130.
[93]彭翕成.向量解题应该重视回路[J].数学教学,2008(6).
[94]张惠英,王申怀,王培甫等.向量及其应用[M].高等教育出版社.2005.
[95]袁桐.重视“向量方法”[J].数学教学,2007,2007(7)：37-41.
[96]张景中.新概念几何[M].北京：中国少年儿童出版社,2002.1.
[97]John R. Anderson. Tuning of Search of the Problem Space for Geometry Proofs[C]. Proceedings of IJCAI,1981.
[98]I. I. Bejar. Generative response modeling:Levering the computer as a test delivery (Research Report RR-96-13)[R]. Princeton, NJ:Educational Testing Service.,1996.
[99]I. I. Bejar. Generative testing:from conception to implementation[C]. In S.H. Irvine & P. Kyllonen (Eds), Item generation for test development (pp.199-218). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[100]R. M Meisner, R. Luecht, M. D. Reckase. The comparability of the statistical characteristics of test items generated by computer algorithms[R]. (ACDT Research Report Series No.93-9) Iowa City,IA:The American College Testing Program,1993.
[101]D.a Roozemond. Proving Statements in Planar Geometry and Cinderella[R],2003.
[102]S. H. Irvine, P. (Eds.). Kyllonen. Item Generation for test development[J]. Mahwah, NJ:Lawrence Earlbaum Associates, Inc.,2002.
[103]程蕾,王泽兵,冯雁.具有自学习功能的自动出题系统[J].计算机工程与设计,2003,24(8)：91-93.
[104]董敏,霍剑青,王晓蒲.基于自适应遗传算法的智能组卷研究[J].小型微型计算机系统,2004,25(1)：82-85.
[105]孟朝霞.基于自适应免疫遗传算法的智能组卷[J].计算机工程,2008,34(14)：203-206.
[106]符丽萍.Authorware中基于文本文件的自动出题系统[J].电脑知识与技术.2009,5(14)：3693-3694.
[107]R.K.Hambleton. Theory, methods, and practices in testing for the 21st century [J]. PSICOTHEMA,2004,16(4):696-701.
[108]丁向民,顾明霞.多项选择题自动生成技术综述[J].现代计算机,2009,2009(307)：36-39.
[109]C.J.Poel, S.D.Weatherly. A Cloze Look at Placement Testing[J]. Shiken:JALT(Japanese Assoc.for Language Teaching)Testing&Evaluation SIG Newsletter,1997,1(1):4-10.
[110]S Seneff. Lee. Automatic Generation of Cloze Items for Prepositions[J]. In Interspeech-2007, 2007:2173-2176.
[111]iGeom. http://www.ime.usp.br/～leo/matica/igeom/.
[112]S. Isotani, L. D. O. Brandao. An algorithm for automatic checking of exercises in a dynamic geometry system:iGeom[J]. Computers & Education,2008,51(3):1283-1303,
[113]R. Grothman. CAR-Compass And Rules[M],1999.
[114]J. T. Schwartz. Probabilistic algorithms for verification of polynomial identities[J]. Journal of the ACM,1980,27(4):701-717.
[115]S. E. Embretson. Psychometric models for learning and cognitive processes[J]. In N. Frederiksen,R. J. Mislevy, & et-al (Eds.), Test theory for a new generation of tests (pp.125-150) Hillsdale,NJ:Lawrence Erlbaum Associates.,1993.
[116]S. E. Embretson. A cognitive design system approach to generating valid tests:Application to abstract reasoning[J]. Psychological Methods,1998(3):380-396.
[117]S.E.Embretson. Generating items during testing:Psychometric issues and models. [J]. Psychometrika,1999,64(4):407-433.
[118]S. E. Embretson. Generating abstract reasoning items with cognitive theory[J]. In S. H. Irvine & P. Kyllonen (Eds), Item generation for test development (pp.219-250). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[119]S. Newstead, P. Bradon, S. Handley, et al. Using the psychology of reasoning to predict the difficulty of analytical reasoning items[M]. In S. Irvine & P. Kyllonen (Eds.), Item generation for test development. Mahwah, NJ:Lawrence Earlbaum Associates,2002.
[120]R. J. Mislevy, L. S. Steinberg, R. G Almond. On the roles of task model variables in assessment design[J]. in S. Irvine & P. Kyllonen (Eds.), Item generation for test development (pp.97-128). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[121]萨师煊,王珊.数据库系统概论[M].北京：高等教育出版社,2000：461.
[122]George F.Luger,史忠植,张银奎.人工智能：复杂问题求解的结构和策略[M].原书第五版.北京：机械工业出版社,2006.
[123]Shang-Ching Chou, Xiao-shan Gao, Jing-zhong Zhang. Machine Proofs in Geometry:Automated Production of Readable Proofs for Geometry Theorems[M]. Singapore:World Scientific,1994.
[124]S. C. Chou, X. S. Gao, J. Z. Zhang. Automated production of traditional proofs for constructive geometry theorems[C]. Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science,1993.1993:48-56.
[125]F. Bancilhon, R. Ramakrishnan. An amateur's introduction to recursive query processing strategies[C]. in C. Zanioilo (ed.), Proc. of ACM SIGMOD Conference, New York,1986: 16-52.
[126]L. Wos. Automated Reasoning:33 Basic Research Problems[J]. Prentice Hall, Englewood Cliffs, NJ 07632(USA),1988:319.
[127]R. Helm. On the elimination of redundant derivations during execution[C]. Proceedings of the 1990 North American conference on Logic programming, MA, USA,1990:551-568.
[128]Michael Sipser,唐常杰,陈鹏等.计算理论导引[M].原书第二版.北京：机械工业出版社,2006：187.
[129]吴文俊.王者之路：机器证明及其应用[M].长沙：湖南科学技术出版社,1999：195.
[130]张景中,葛强,彭翕成.教育技术研究要深入学科[J].电化教育研究,2010.2(总202期)：8-13.
[131]H. Gelernter. Realization of a geometry-theorem proving machine[J]. Computers & thought,New York:McGraw-Hill.1963:134-152.
[132]张景中.数学机械化与现代教育技术[J].信息技术教育,2003.2003(1)：34-37.
[133]李传中,张景中.智能知识平台的构想及其实现[J].世界科技研究与发展.2001,23(6)：1-6.
[134]张景中.论知识服务体系中的智能知识平台[J].华中师范大学学报(自然科学版),2005.12,39(4).
[135]齐治昌.软件工程[M].第二版.北京：高等教育出版社,2004：129.
[136]侯俊杰.深入浅出MFC[M].第二版.武汉：华中科技大学,2001：49.
[137]姚领田,高守传.MFC窗口程序设计[M].北京：中国水利水电出版社,2007：35.
[138]Roger S. Pressman,梅宏(译).软件工程：实践者的研究方法[M].原书第五版.北京：机械工业出版社.2002：35.
[139]周鸣扬,赵景亮.精通GDI+编程[M].北京：清华大学出版社,2003：474.
[140]Mahesh Chand,韩江(等译).GDI+图形程序设计[M].北京：电子工业出版社,2006：40.
[141]张景中,彭翕成.自动推理及其在数学教育中的应用[J].数学教育学报,2008.8,17.4.
[142]Z. Ye, S. C. Chou, X. S. Gao. Visually Dynamic Presentation of Proofs in Plane Geometry Part 1. Basic Features and the Manual Input Method[J]. Journal of Automated Reasoning,2010,45(3): 213-241.
[143]Z. Ye, S. C. Chou, X. S. Gao. Visually Dynamic Presentation of Proofs in Plane Geometry Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method[J]. Journal of Automated Reasoning,2010,45(3):243-266.
[2]吴文俊.几何定理机器证明的基本原理(初等几何部分)[M].北京：科学出版社,1984.8：280.
[3]S. C. Chou,X. S. Gao,J. Z. Zhang. Automated generation of readable proofs with geometric invariants.1. Multiple and shortest proof generation[J]. Journal of Automated Reasoning,1996,17(3): 325-347.
[4]S. C. Chou,X. S. Gao,J. Z. Zhang. Automated generation of readable proofs with geometric invariants.2. Theorem proving with full-angles[J]. Journal of Automated Reasoning,1996,17(3): 349-370.
[5]Ralph E F.. The use of geometry and proportional reasoning techniques at the US Department of Agriculture[J]. Teaching Mathematics and its Applications,2006,25(1):1.
[6]Bernd F., Geoff S., Stephan S.. Empirically successful automated reasoning:applications issue[J]. Journal of Automated Reasoning,2006,37(1).
[7]J. Harrison. A short survey of automated reasoning[J]. Algebraic Biology,2007:334-349.
[8]MMP-数学机械化自动推理平台.http://www.mmrc.iss.ac.cn/mmp/.
[9]H.Wang. Toward mechanical mathematics[J]. IBM Journal of research and development,1960, 4(1):2-22.
[10]刘江.逻辑学推理和论证[M].第二版.广州：华南理工大学出版社,2010.
[11]D. Kapur. Automated geometric reasoning:Dixon resultants, Grobner bases, and characteristic sets[J]. Automated Deduction in Geometry,1997:1-36.
[12]Chou Shang-Ching. Mechanical Geometry Theorem Proving[M]:D.Reidel Publishing Company, 1988.
[13]S.C. Chou, W.F. Schelter, J.G Yang. An algorithm for constructing Grobner bases from characteristic sets and its application to geometry[J]. Algorithmica,1990,5(1):147-154.
[14]B. Kutzler, S. Stifter. A geometry theorem prover based on Buchberger's algorithm[C],8th International Conference on Automated Deduction Lecture Notes in Computer Science.1986: 693-694.
[15]高小山,张景中,周咸青.几何专家[J].北京：中国少年儿童出版社,1998.
[16]S. C. Chou, X. S. Gao, J. Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Automated Reasoning,2000,25(3):219-246.
[17]Jing Zhong Zhang, Shang Ching Chou, Xiao Shan Gao. Automated Production of Traditional Proofs for Theorems In Euclidean Geometry-the hilbert intersection point theorems[J]. Annals of Mathematics and Artifical Intelligence,1995,13:109-137.
[18]J.-Z. Zhang, L. Yang, X.-S. Gao, et al. Automated production of readable proofs for geometry theorems[J]. Chinese Journal Of Computers,1995,18(5):14.
[19]张景中,高小山,周咸青.基于前推法的几何信息搜索系统[J].计算机学报,1996,19(10)：721-727.
[20]江建国.iGeo_智能几何软件的定理证明器[D].成都：中国科学院成都计算机应用研究所,2006.4：202.
[21]潘斌,郭红霞.几何定理机器证明的并行前向推理[J].华南理工大学学报(自然科学版),2008(04).
[22]郭四稳.基于数据库技术的自动推理系统[D].成都：四川大学,2001.
[23]邹宇.几何代数基础与质点几何的可读机器证明[D].广州：广州大学,2010.5.
[24]郑焕.SGARP:可由用户持续发展的几何自动推理平台[D].广州：广州大学,2011：134.
[25]Gao Xiao-shan, Lin Qiang. MMP/Geometer-a software package for automated gemetry reasoning[M]. Berlin:Springer.2004:44-66.
[26]GeoProof. http://home.gna.org/geoproof/.
[27]The Interactive Geometry Software Cinderella.http://www.cinderella.de/tiki-index.php.
[28]OpenMath. http://www.openmath.org/.
[29]Singular. http://www.singular.uni-kl.de/.
[30]嘉科平面几何. http://down.itl68.com/283/284/45098/index.shtml.
[31]超级画板.http://www.zplusz.org/.
[32]高小山,王定康,裘宗燕.方程求解与机器证明--基于MMP的问题求解[M].北京：科学出版社,2006.9.
[33]Ulrich H. Kortenkamp. Foundations of dynamic geometry[D]. Zurich,Switzerland:Swiss Federal Institute of Technology,1999:15-114.
[34]Y. Bertot, F. Guilhot, L. Pottier. Visualizing geometrical statements with GeoView[C], International Workshop, UITP'03,2003:32.
[35]The Riaca OpenMath Library. http://www.riaca.win.tue.nl.
[36]G. Pfister G.-M. Greuel, and H. Schonemann. A Computer Algebra System for Polynomial Computations[J]. Centre for Computer Algebra, University of Kaiserslautern, http://www.singular.uni-kl.de.,2001.
[37]The Geometer's Sketchpad. http://dynamicgeometry.com/.
[38]张景中.几何定理机器证明20年[J].科学通报.1997,42(21)：2248-2260.
[39]段敏.创新平面几何试题并能自动推理的《数学实验室--平面几何》[J].合肥教学学院学报,2002,19(2)：5-8.
[40]Jing Zhong Zhang, Lu Yang, Mike Deng. The parallel numerical method of mechanical theorem proving[J]. Theoretical computer science,1990,74(3):253-271.
[41]张景中,杨路,高小山.几何定理可读证明的自动生成[J].计算机学报,1995,18(5)：380-393.
[42]Cabri Ⅱ Plus-http://www.cabri.com/cabri-2-plus.html.
[43]蒋鲲.几何自动作图[M].哈尔滨：哈尔滨工业大学出版社,2007.
[44]高小山,蒋鲲.几何约束求解研究综述[J].计算机辅助设计与图形学学报,2004,16(4)：385-396.
[45]高小山,黄磊东,蒋鲲.求解几何约束问题的几何变换法[J].中国科学(E辑),2001,31(2)：182-192.
[46]蒋鲲,高小山,岳晶岩.参数化模型欠、过和完整约束的判定算法[J].软件学报,2003,14(12)：2092-2097.
[47]J. Escribano, F. Botana, M. A. Abanades. Adding remote computational capabilities to Dynamic Geometry Systems[J]. Math. Comput. Simul.,2010,80(6):1177-1184.
[48]C.a.R. http://zirkel.sourceforge.net/.
[49]Euklid. http://www.dynageo.com/.
[50]GCLC/WinGCLC. http://poincare.matf.bg.ac.rs/-janicic//gclc/.
[51]Geometry Epressions. http://www.geometryexpressions.com/.
[52]The Geometric Supposer. http://www.cet.ac.il/math-international/software5.htm.
[53]GeoGebra. http://www.geogebra.org/cms/index.php?lang=zh.
[54]Java Geometry Expert. http://www.cs.wichita.edu/-ye/.
[55]S. S. Choi-Koh. A Student's Learning of Geometry Using the Computer[J]. Journal of Educational Research,1999,92(5):301-311.
[56]R. Sommer, G Nuckols. A proof environment for teaching mathematics[J]. Journal of Automated Reasoning,2004,32(3):227-258.
[57]M. Isiksal, P. Askar. The effect of spreadsheet and dynamic geometry software on the achievement and self-efficacy of 7th-grade students[R]. Educ. Res.,2005,47(3):333-350.
[58]Jing Zhong Zhang, Hui Ming Xiong, Xing Cheng Peng. Free Software SSP for Teaching Mathematics[J]. Symbolic computation and Education,2007.
[59]B. Guven, T. Kosa. The effect of dynamic geometry software on student mathematics teachers' spatial visualization skills[J]. Turk. Online J. Educ. Technol.,2008,7(4):100-107.
[60]吴文渊,曾振柄,符红光.基于Ontology的平面几何知识库设计[J].计算机应用.2002,22(3)：10-14.
[61]钟秀琴,符红光,余莉等.基于本体的几何学知识获取及知识表示[J].计算机学报,2010,33(1)：167-174.
[62]余莉,符红光.基于自然语言处理的计算机几何作图[J].计算机应用,2005,25(1)：7-10.
[63]Qiang Ge, Xicheng Peng, Mao Chen. Introduction to retrieval knowledge using intelligent education software[C]. The 2nd International Symposium on Knowledge Acquisition and Modeling,2009:148-151.
[64]郭四稳.基于动态作图的化学符号编辑系统[J].广州大学学报：自然科学版,2006.12,5卷(6期)：19-22.
[65]Wu WenTen. Mathematics Mechanization. Kluwer:Science Prss,2000.
[66]B. Kutzler. Algebraic approaches to automated geometry theorem proving[J]. Ph. I) thesis, RISC-Linz, Johannes Kepler University, Austria,1988.
[67]产生式.http://baike.baidu.com/view/1308820.htm.
[68]何援军.计算机图形学[M].第二版.北京：机械工业出版社.2009：16.
[69]Mark de Berg, Otfried Cheong, Marc van Kreveld, et al计算几何：算法与应用[M].北京：清华大学出版社,Springer,2009:19.
[70]张景中,彭翕成.动态几何教程[M].北京：科学出版社,2007.9.
[71]Geometry Expressions Homepage, http://www.geometryexpressions.com/.
[72]郑逢斌.计算机理解自然查询语言的研究和实现[D].成都：西南交通大学,2004.
[73]朱创录.基于语义Web的自动推理技术研究[D].西安：西北大学,2006.4.
[74]刘伟,符红光,佘莉.基于语义的几何知识库搜索引擎的设计与实现[J].计算机应用,2007,27(6)：76-78.
[75]杨宗凯.国家高技术研究发展计划(863计划)课题自验收报告：知识浓缩与融合关键技术研究[R].武汉：华中师范大学,2011：10-12.
[76]边肇祺.模式识别[M].第二版.北京：清华大学出版社,2000.
[77]张景中,江春莲,彭翕成.《动态几何》课程的开设在数学教与学中的价值[J].数学教育学报,2007,16(3)：5.
[78]张景中,彭翕成.三款数学教育软件的比较与设计思想分析[J].中国电化教育,2010(276)：107-113.
[79]人民教育出版社,课程教材研究所,中学数学课程教材研究开发中心.数学(2)[M].第二版.北京：人民教育出版社,2007：39-144.
[80]Arthur J. Nevins. Plane Geometry Theorem Proving Using Forward Chaining[J]. Artifical Ingelligence,1974, Volume 6, Issue 1:P303-338.
[81]Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang. Automated geometry theorem proving by vector calculation [J]. Proceedings of the 1993 international symposium on Symbolic and algebraic computation,1993, ACM New York, NY, USA:284-291.
[82]S. Stifter. Geometry theorem proving in vector spaces by means of Grobner bases[C]. the 1993 International Symposium on Symbolic and Algebraic Computation,1993:301-310.
[83]孙熙椿.几何定理计算机证明[M].北京：科学出版社,2007：11.
[84]I.M. Yaglom.九种平面几何[M].上海上海科学技术出版社,1955-1956：358.
[85]张顺燕.推理与证明[M].北京：高等教育出版社,2006：167-168.
[86]张景中,彭翕成.论向量法解几何问题的基本思路[J].数学通报,2008,47(2)：6-10.
[87]张景中,彭翕成.论向量法解几何问题的基本思路(续)[J].数学通报.2008,47(3)：31-36.
[88]陈胜利.向量与平面几何证题[M].北京：中国文史出版社,2003：33.
[89]张景中,彭翕成.绕来绕去的向量法[M].北京：科学出版社,2010.9：287.
[90]人民教育出版社,课程教材研究所,中学数学课程教材研究开发中心.数学(4)[M].第三版.北京：人民教育出版社,2007：73-122.
[91]周培德.计算几何：算法设计与分析[M].第三版.北京：清华大学出版社,2008：41.
[92]余祥宣,崔国华,邹海明.计算机算法基础[M].第三版.武汉：华中科技大学出版社,2006：130.
[93]彭翕成.向量解题应该重视回路[J].数学教学,2008(6).
[94]张惠英,王申怀,王培甫等.向量及其应用[M].高等教育出版社.2005.
[95]袁桐.重视“向量方法”[J].数学教学,2007,2007(7)：37-41.
[96]张景中.新概念几何[M].北京：中国少年儿童出版社,2002.1.
[97]John R. Anderson. Tuning of Search of the Problem Space for Geometry Proofs[C]. Proceedings of IJCAI,1981.
[98]I. I. Bejar. Generative response modeling:Levering the computer as a test delivery (Research Report RR-96-13)[R]. Princeton, NJ:Educational Testing Service.,1996.
[99]I. I. Bejar. Generative testing:from conception to implementation[C]. In S.H. Irvine & P. Kyllonen (Eds), Item generation for test development (pp.199-218). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[100]R. M Meisner, R. Luecht, M. D. Reckase. The comparability of the statistical characteristics of test items generated by computer algorithms[R]. (ACDT Research Report Series No.93-9) Iowa City,IA:The American College Testing Program,1993.
[101]D.a Roozemond. Proving Statements in Planar Geometry and Cinderella[R],2003.
[102]S. H. Irvine, P. (Eds.). Kyllonen. Item Generation for test development[J]. Mahwah, NJ:Lawrence Earlbaum Associates, Inc.,2002.
[103]程蕾,王泽兵,冯雁.具有自学习功能的自动出题系统[J].计算机工程与设计,2003,24(8)：91-93.
[104]董敏,霍剑青,王晓蒲.基于自适应遗传算法的智能组卷研究[J].小型微型计算机系统,2004,25(1)：82-85.
[105]孟朝霞.基于自适应免疫遗传算法的智能组卷[J].计算机工程,2008,34(14)：203-206.
[106]符丽萍.Authorware中基于文本文件的自动出题系统[J].电脑知识与技术.2009,5(14)：3693-3694.
[107]R.K.Hambleton. Theory, methods, and practices in testing for the 21st century [J]. PSICOTHEMA,2004,16(4):696-701.
[108]丁向民,顾明霞.多项选择题自动生成技术综述[J].现代计算机,2009,2009(307)：36-39.
[109]C.J.Poel, S.D.Weatherly. A Cloze Look at Placement Testing[J]. Shiken:JALT(Japanese Assoc.for Language Teaching)Testing&Evaluation SIG Newsletter,1997,1(1):4-10.
[110]S Seneff. Lee. Automatic Generation of Cloze Items for Prepositions[J]. In Interspeech-2007, 2007:2173-2176.
[111]iGeom. http://www.ime.usp.br/～leo/matica/igeom/.
[112]S. Isotani, L. D. O. Brandao. An algorithm for automatic checking of exercises in a dynamic geometry system:iGeom[J]. Computers & Education,2008,51(3):1283-1303,
[113]R. Grothman. CAR-Compass And Rules[M],1999.
[114]J. T. Schwartz. Probabilistic algorithms for verification of polynomial identities[J]. Journal of the ACM,1980,27(4):701-717.
[115]S. E. Embretson. Psychometric models for learning and cognitive processes[J]. In N. Frederiksen,R. J. Mislevy, & et-al (Eds.), Test theory for a new generation of tests (pp.125-150) Hillsdale,NJ:Lawrence Erlbaum Associates.,1993.
[116]S. E. Embretson. A cognitive design system approach to generating valid tests:Application to abstract reasoning[J]. Psychological Methods,1998(3):380-396.
[117]S.E.Embretson. Generating items during testing:Psychometric issues and models. [J]. Psychometrika,1999,64(4):407-433.
[118]S. E. Embretson. Generating abstract reasoning items with cognitive theory[J]. In S. H. Irvine & P. Kyllonen (Eds), Item generation for test development (pp.219-250). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[119]S. Newstead, P. Bradon, S. Handley, et al. Using the psychology of reasoning to predict the difficulty of analytical reasoning items[M]. In S. Irvine & P. Kyllonen (Eds.), Item generation for test development. Mahwah, NJ:Lawrence Earlbaum Associates,2002.
[120]R. J. Mislevy, L. S. Steinberg, R. G Almond. On the roles of task model variables in assessment design[J]. in S. Irvine & P. Kyllonen (Eds.), Item generation for test development (pp.97-128). Mahwah, NJ:Lawrence Earlbaum Associates.,2002.
[121]萨师煊,王珊.数据库系统概论[M].北京：高等教育出版社,2000：461.
[122]George F.Luger,史忠植,张银奎.人工智能：复杂问题求解的结构和策略[M].原书第五版.北京：机械工业出版社,2006.
[123]Shang-Ching Chou, Xiao-shan Gao, Jing-zhong Zhang. Machine Proofs in Geometry:Automated Production of Readable Proofs for Geometry Theorems[M]. Singapore:World Scientific,1994.
[124]S. C. Chou, X. S. Gao, J. Z. Zhang. Automated production of traditional proofs for constructive geometry theorems[C]. Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science,1993.1993:48-56.
[125]F. Bancilhon, R. Ramakrishnan. An amateur's introduction to recursive query processing strategies[C]. in C. Zanioilo (ed.), Proc. of ACM SIGMOD Conference, New York,1986: 16-52.
[126]L. Wos. Automated Reasoning:33 Basic Research Problems[J]. Prentice Hall, Englewood Cliffs, NJ 07632(USA),1988:319.
[127]R. Helm. On the elimination of redundant derivations during execution[C]. Proceedings of the 1990 North American conference on Logic programming, MA, USA,1990:551-568.
[128]Michael Sipser,唐常杰,陈鹏等.计算理论导引[M].原书第二版.北京：机械工业出版社,2006：187.
[129]吴文俊.王者之路：机器证明及其应用[M].长沙：湖南科学技术出版社,1999：195.
[130]张景中,葛强,彭翕成.教育技术研究要深入学科[J].电化教育研究,2010.2(总202期)：8-13.
[131]H. Gelernter. Realization of a geometry-theorem proving machine[J]. Computers & thought,New York:McGraw-Hill.1963:134-152.
[132]张景中.数学机械化与现代教育技术[J].信息技术教育,2003.2003(1)：34-37.
[133]李传中,张景中.智能知识平台的构想及其实现[J].世界科技研究与发展.2001,23(6)：1-6.
[134]张景中.论知识服务体系中的智能知识平台[J].华中师范大学学报(自然科学版),2005.12,39(4).
[135]齐治昌.软件工程[M].第二版.北京：高等教育出版社,2004：129.
[136]侯俊杰.深入浅出MFC[M].第二版.武汉：华中科技大学,2001：49.
[137]姚领田,高守传.MFC窗口程序设计[M].北京：中国水利水电出版社,2007：35.
[138]Roger S. Pressman,梅宏(译).软件工程：实践者的研究方法[M].原书第五版.北京：机械工业出版社.2002：35.
[139]周鸣扬,赵景亮.精通GDI+编程[M].北京：清华大学出版社,2003：474.
[140]Mahesh Chand,韩江(等译).GDI+图形程序设计[M].北京：电子工业出版社,2006：40.
[141]张景中,彭翕成.自动推理及其在数学教育中的应用[J].数学教育学报,2008.8,17.4.
[142]Z. Ye, S. C. Chou, X. S. Gao. Visually Dynamic Presentation of Proofs in Plane Geometry Part 1. Basic Features and the Manual Input Method[J]. Journal of Automated Reasoning,2010,45(3): 213-241.
[143]Z. Ye, S. C. Chou, X. S. Gao. Visually Dynamic Presentation of Proofs in Plane Geometry Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method[J]. Journal of Automated Reasoning,2010,45(3):243-266.