（教育技术学专业论文）限制条件下的几何自动推理及应用研究.pdf

博士学位论文 d o c t o r a ld i s s e r 湖0 n 摘要 几何学具有悠久的历史，两千多年来积累下来的几何知识是人类的宝贵财富。其中，几何 证明是几何学的精华之一。几何题的证法，没有统一的方法可依循，有赖于个人的灵感和技巧， 一直是数学教学中的难点和重点内容。用机器来模仿人的思维活动，来帮助人证明几何命题， 是历史上一些卓越科学家的梦想，也是具有重要研究价值和应用价值的研究方向。吴文俊建立 的数学机械化方法，极大的推动了几何定理机器证明领域的研究。目前，基于不同推理算法的 自动推理系统已经出现，在科学研究和工程计算中发挥着重要的作用。 但是，几何定理自动推理领域中的丰富成果，在教育中并没有得到充分应用，其教育价值 远远没能得到充分体现。原因一方面在于中学教育阶段涉及到的几何知识比较初等，而现有的 几何自动推理方法给出的证明过程难于被中学生理解；另一方面，几何知识的教学又涉及语言 表达与作图、从图形发现问题、问题分析与解答等多个方面，不仅仅是单纯的几何定理机器证 明。面对中学几何教学的应用需求，几何自动推理的研究面临着中学几何知识范围、解答步骤 长度、推理时间和推理方法等多方面的限制。针对这些限制条件，本文开展了面向中学几何教 学的几何自动推理的研究工作，涉及几何自动推理在动态几何作图、几何问题生成、向量法解 题等方面的理论方法与应用，研究成果( 创新点) 包括以下几个方面： 第一：提出动态几何作图中的枢点概念，建立了以枢点为基础的动态几何机制，设计了包 括智能作图方法，语义作图方法和文本作图等几何作图方法。实现了相应的动态几何作图系统， 拓展了动态几何理论。 第二：提出并实现基于向量法的自动推理算法。该自动推理方法基于向量的回路特征，对 构造型交点类几何命题能迅速地给出可读的向量式证明，证明过程简洁优美。这种自动推理方 法能够在限制条件内能达到推理不动点，在构造型交点类的题目上表现出较高的效率。 第三：提出并实现了基于自动推理的几何问题自动生成与答案验证方法。以自动推理为基 础，设计了可以生成填空、判断、选择、计算和证明等多种题型的自动出题方法，并实现对用 户的解答进行实时验证。这种方法创新了几何学出题方式，提高了测试效率。 综合应用上述研究成果，实现了一个面向中学教学应用的几何自动推理原型系统，其主要 功能包括动态几何作图、几何自动推理和题目自动生成。这三种主要功能有机集成，可满足教 师课堂教学和学生课下自学的需求。 最后提出了值得进一步研究的问题和对此方向未来的展望。 关键词：几何自动推理；教育技术；动态几何；前推法；向量法；自动出题 a b s t r a c t w i 廿lal o n gh i s t o r y , t h ek n o w l e d g eo fg e o m e t r yi sav a l u a b l ew e a l t ho fm a n k i n d ，w h i c hh a s a c c u m u l a t e dt w ot h o u s a n dy e a r s i nw h i c h , t h ep r o o fo fg e o m e t r yi so n eo ft h ee l i t e s t h ep m v i n g m e t h o d sw i t hn ou n i f o r mm e t h o d sh a v eb e e nad i f f i c u l ta n dk e yc o n t e n ti nm a t h e m a t i c st e a c h i n g , w h i c hd e p e n do nt h ep e r s o n a li n s p i r a t i o na n ds k i l l s u s i n gm a f h i n e st om i m i ch u m a nt h i n k i n gt oh e l p p e o p l ep r o v eg e o m e 仃i cp r o p o s i t i o n si st h ed r e a mo f s o m eo ft h eo u t s t a n d i n gs c i e n t i s t si nh i s t o r y , b u t a l s oh a si m p o r t a n tv a l u eo fr e s e a r c ha n da p p l i c a t i o n w u - m e t h o dg r e a t l yc o n t r i b u t e st og e o m e t r y t h e o r e mp r o v i n gr e s e a r c hi nt h ef i e l d c u r r e n t l y , t h ea u t o m a t e dr e a s o n i n gs y s t e m sb a s e do nd i f f e r e n t r e a s o n i n ga l g o r i t h m sh a se m e 电e di ns c i e n t i f i cr e s e a r c ha n de n g i n e e r i n gc a l c u l a t i o n sa n di tp l a y sa n i m p o r t a n tr o l e h o w e v e r , t h er i c ha c h i e v e m e n t so ft h ef i e l do fa u t o m a t e dr e a s o n i n gi ng e o m e t r yt h e o r e mh a v e n o tb e e nf u l l ya p p l i e di ne d u c a t i o n , t h e i re d u c a t i o n a lv a l u ei sf a rf a i l e dt ob ef u l l yr e f l e c t e d t h e r e a s o ni st h a t , o i lt h eo n eh a n d , t h ，ek n o w l e d g eo fg e o m e t r yi ns e c o n d a r ye d u c a t i o ni se l e m e n t a r y c o m p a r e dt om a t h e m a t i c s ，t h eg i v e np r o c e s sb ye x i s t i n gm e t h o d so fa u t o m a t e dr e a s o n i n go fg e o m e t r y i ss od i f f i c u l tt h a ts t u d e n t sc o u l d n tu n d e r s t a n d o nt h et h eo t h e rh a n d , k n o w l e d g eo fg e o m e t r y t e a c h i n gi n v o l v e st h ee x p r e s s i o na n dc o n s t r u c t i o no fg e o m e t r y , g e n e r a t i n gg e o m e t r i cp r o b l e mf r o m g i v e nc o n s t r u c t i o n , a n a l y s i sa n ds o l v i n gf o rap r o b l e ma n do t h e ra s p e c t s ，n o tj u s tas i m p l eg e o m e t r i c t h e o r e mp r o v i n g f o rt h ea p p l i c a t i o nr e q u i r e m e n t so fg e o m e t r yt e a c h i n gi nh i 曲s c h o o l s ，t h es t u d yo f g e o m e t r ya u t o m a t e dr e a s o n m gf a c e st h er e s t r i c t i o n so f t h es c o p eo f g e o m e t r yk n o w l e d g e i i ls e c o n d a r y s c h o o l s ，t h el e n g t ho f w o r k i n gs t e p s ，t i m ea n dr e a s o n i n gm e t h o d s i nr e s p o n s et ot h e s el i m i t a t i o n s ，t h i s p a p e rc a r r i e do u tt h er e s e a r c ho na u t o m a t e dr e a s o n i n ga b o u tt h et e a c h i n go fg e o m e t r yi ns e c o n d a r y s c h o o l s ，w h i c hi n v o l v e st h et h e o r ya n da p p l i c a t i o no ft h ed y n a m i cg e o m e t r yc o n s t r u c t i o n , g e n e r a t i n g g e o m e t r yp r o b l e m , p r o b l e m - s o l v i n gw i t hv e c t o ra p p r o a c ha n do t h e ra s p e c t s ，t h er e s e a r c hr e s u l t sa n d i n n o v a t i o ni n c l u d et h ef o l l o w i n g ： f i r s t ：t h i sp a p e rp r o p o s e st h ep i v o tc o n c e p ti nd y n a m i cg e o m e t r yc o n s t r u c t i o na n dt h ed y n a m i c g e o m e t r ym e c h a n i s mb a s e do nt h ep i v o ti d e a s e v e r a lm e t h o d so f t h ed y n a m i cg e o m e t r i cc o n s t r u c t i o n b a s e do np i v o tc o n c e p th a v eb e e nd e s i g n e d , w h i c hi n c l u d et h em a n u a lm e t h o do fi n t e l l i g e n t c o n s t r u c t i o n , s e m a n t i cc o n s t r u c t i o na n dc o n s l n l c f i o nm e t h o do ft h et e x t t h ef u n c t i o no fd y n a m i c g e o m e t r i cc o n s t r u c t i o ni nap r o t o t y p es y s t e mh a sb e e ni m p l e m e n t e d , a n di te x t e n d st h et h o e r i e so f d y n a m i cg e o m e t r y s e c o n d ：t h ep a p e rp r o p o s e sa n di m p l e m e n t sa u t o m a t e dr e a s o n i n ga l g o r i t h m sb a s e dav e c t o r 博士学位论文 d 0 渤r a ld i s s e r t a t i o n m e t h o d t h em e t h o di sb a s e do nt h ec h a r a c t e r i s t i c so f t h ev e c t o rl o o p , w h i c hc a nq u i c k l yg e n e r a t et h e r e a d a b l ev e c t o r - p r o o fo fg i v e np r o p o s i t i o nw i t ht h ec o n s t r u c t e dt y p ea n di n t e r s e c t i o nc l a s s f o r s t u d e n t s ，a n dt h ep r o o fi ss i m p l ea n dr e a d a b l e t h i sm e q h o do fa u t o m a t e dr e a s o n m gc a na c h i e v ea f i x e dp o i n t , a n di ts h o w s h i g h e re f f i c i e n c yi nal a r g ec l a s so fs u b j e c t s t h i r d ：t h ep a p e rp r o p o s e sa n di m p l e m e n t sa l la u t o m a t e dm e t h o do fg e n e r a t i o na n dv e r i f i c a t i o n f o ra g i v e ng e o m e t r i cp r o p o s i t i o nb a s e do na u t o m a t e dr e a s o n i n g t h em e c h a n i s mo fm u l t i - k i n d so f q u e s t i o n sa n dv e r i f i c a t i o nb a s e do na u t o m a t e dr e a s o n i n ga r ec o n s u u c t e d i tc a ng e n e r a t es e v e r a lk i n d s o fe x e r c i s e ss u c ha sf i l l i n gi nt h eb l a n k , j u d g e m e n t , c h o o s e , c a l c u l a t i o na n dp r o o ew h i c hc a n c e r t i f i c a 把t h ep r o b l e mo fr e a l - t i m ea n s w e r sf o ru s e r s t h i sp m v i d e sas o l u t i o nf o rg e n e r a t i n g g e o m e t r ye x e r c i s e sa n di m p r o v e st h ee f f i c i e n c yf o rt e s t i n t e g r a t i n gt h ea p p l i c a t i o no f a b o v er e s e a r c hr e s u l t s , a na u t o m a t e dg e o m e t r yr e a s o n i n gp r o t o t y p e s y s t e mu n d e rc o n s t r a i n e dc o n d i t i o n sh a sb e e np r o g r a m m e di nt h i sp a p e r t h es y s t e mi sc o n c e r n e d w i t ht h el i m i t sa n dm e t h o d so ft h es c o p eo fg e o m e t r yk n o w l e d g ei nh i g hs c h o o l ，i t sm a i nf e a t u r e s i n c l u d e ：t h ed y n a m i cg e o m e t r yc o n s l r u c t i o n , a u t o m a t e dr e a s o n i n ga n da u t o m a t e dg e n e r a t i o no f g e o m e t r i ce x e r c i s e s t h eo r g a n i ci n t e g r a t i o no ft h et h r e em a i nf u n c t i o n sc o u l ds a t i s f yt h ec l a s s r o o m t e a c h i n gb yt e a c h e r sa n ds e l f - s t u d yc o u r s e sb ys t u d e n t s f i n a l l y , aq u e s t i o nw o r t h yo ff u r t h e rs t u d ya n df u t u r ep r o s p e c t sf o rt h i sd i r e c t i o na r ec o n c l u d e d k e y w e r d s ：g e o m e t r ya u t o m a t e dr e a s o n i n g ；e d u c a t i o n a lt e c h n o l o g y ；d y n a m i cg e o m e t r y ；f o r w a r d c h a i n i n gm e t h o d ；v e c t o ra p p r o a c h ；a u t o m a t e dg e n e r a t i n go fe x e r c i s e s l l i 博士学位论文 d o c t o r a ld i s s e r i o n 的对象是否是偶然关联的，或是有一个定理能判断它们是相同的【3 3 1 。 然而，自动习题生成很明显地依赖于认知能力的建模。这样的模型是缺少的，生成算法仅有 启发性的作用。在自动习题生成研究上的进展大部分是在那些有良好认知建模的领域，如m a t r i x c o m p l e t i o n l l l 川8 】，a n a l y t i c a lr e a s o n i n g t l l 9 1 。测试构造的理论中自动习题生成方法是如此重要， 它的题目设计有明显依赖的基础，如，e v i d e n c ec e n t e r e dd e s i g n 但c d ) 【1 2 0 1 。 本章从中学数学学科出发，以限制条件下的平面几何自动推理技术为基础，研究几何题目 的自动生成，为其它科目的题目生成研究提供借鉴和思路。 4 3 自动推理信息生成理论 由于中学几何内容的限制，自动推理所使用的推理引擎采用了中学几何学习所包含的公理、 定理、定义、性质等知识作为规则。当然，也包括在上一章里所提出的向量法。在这样的限制 条件下，推理引擎能够产生大量的几何信息，生成可读证明，达到推理不动点。 4 3 1 数据源信息 任何算法和生产机器都要有原材料可供加工，推理机器的运行也需要几何数据。由动态几 何软件提供图形接口，再转化为本推理引擎所使用的数据格式。本章以第3 章提到的方法来表 示推理数据源信息。 定义1 ：数据集在推理的过程中，需要用到各式各样的几何信息，每一种几何信息为了方 便检索和存储都需要集中存储在一个集合中，每一种这样的信息集合称为一个数据集。由于不 同信息的结构不同，每种信息的数据集的结构和大小也是不一样的。 定义2 ：几何信息库在一个推理系统中，需要多个数据集互相配合为推理提供数据，这些 数据集组织在一起就构成了几何信息库。信息库中的数据集是互异的，结构化的【1 2 。 几何信息库中有一系列的数据集，每次推理引擎运行之初，都必须要清空数据集，然后从 图形信息中导入数据，进行分析，数据信息分别存储相关对应的数据集中。 本章中的数据可以通过如下方式扩充： ( 1 ) 所有的已知条件的多种表达方式； ( 2 ) 几何命题中的可以推理得到的几何关系； ( 3 ) 使用其它方法得到的欧氏几何关系表达式，如向量法。为了建立更大的几何信息库， 应当积极扩大前推法中的规则和开发其它新方法。 定义3 ：推理引擎如同第3 5 节中的定义l 。 4 3 2 数据驱动机制 几何信息库中各个数据集会有一些数据，这些数据可以驱动相关类型的规则进行工作，得 6 3 博士学位论文 d o c t o r a ld i s s e r t a t l 0 n 出合理的新信息。有些数据暂时不存在，则不可以调用使用此数据作为输入信息的规则。数据 驱动机制1 2 2 1 可以使推理引擎避免做无用功，提高推理效率。 4 3 3 几何规则算法 平面几何中众多的定义、公理、定理、推论和公式等都是推理中需要用到的理论依据，都 应当归结为一条条的规则。 定义4 ：推理规则为了完成信息的推导，需要用到几何公理系统中的一些规则，如：公理， 定理，引理，性质，定义等，这些规则统称为推理规则。 一个推理规则在形式上也是一个h o r n 子句，它遵从如下形式 q ( 工) ：一只( 力，置( 工) ( 4 1 ) 意味着： 眦暑( 工) 丑( x ) ) jq ( 工) 】 ( 4 2 ) 其中，x 是出现在几何谓词暑( 力，丑o ) 和q ( x ) 中的点，而且暑( x ) ，丑o ) 和q ( 工) 分别 被称作规则的前提和结论。只有有限的h o r n 子旬出现在本文中。一般情况下，作为结果，不允 许有代数运算，这是因为代数运算实际上是符号运算，容易导致无穷的推理结果序列，因此， 要想达到推理不动点是很难的。 定义5 ：规则库多个推理规则按层次组织在一起，构成一个完备的几何推理系统，称之为 规则库。 规则库，这是推理引擎的根本。对于满足当前算法条件的规则，运用具体的规则，生成中 间信息。记录此中间信息，还有关于此规则的信息也应记录下来，存储于此类信息的数据表， 以供回溯时反推出推理过程。 为了加强推理引擎的效率，需要在其内部建立更加复杂和高效的推理规则。推理引擎使用 的规则有两类：一类是根据一个定理或公理制定一个推理规则，这种属于一般性的规则1 2 3 , 1 2 4 l 。 第二类是一些基本规则的组合。基于证明经验，这些组合在许多定理的证明中经常会用到。理 论上来说，这些组合的规则通过搜索基本规则能够自动被调用。但这个搜索过程是消耗时间的， 既然推理引擎在得到一个可用的规则之前必须遍历许多先行( 前提) 的规则，可以人工建立一 些复合规则，如下所示： 令d 作为某一数据集中的新信息，有一些规则会是： 尸 z q ，尸人zj q ( 4 3 ) 其中，p 是事实d 的谓词，夕是其它谓词的联结体集合。于是，可以构造一个新的复合规 则： p ( zj q ，zj q ) ( 4 4 ) 举例如下： 博士学位论文 d o c t o r a ld i s s e r 咖o n 厶l 爿一 县 厶? b - c l 3 ：a - b + c 岛是对规则工l 和岛的复合。这样仅使用厶就节约了一条规则的调用时间，提高了效率。 4 3 4 推理机制 推理引擎需要达到推理不动点，广度优先的前推法是本文的自然选择。几何规则是高度复 杂的，所有的谓词是互相调用，大部分的规则是非线性的。因此，为某些特殊规则设计更加专 业化的搜索策略是可行的。 一般来讲，广度优先的前推法搜索工作原理如下： 囤；r 削三r 一乒- k ( f i x p o i n t ) 其中，d 0 是几何命题的已知条件，r 是规则库。对于每一个r 中的r ，应用到d o 就会产生 一些新的事实。让d l 作为d o 和这些新产生信息的并集。重复上面的过程从d l 到d 2 ，以此类 推。在后面的某一个步骤，d k = d k + 1 ，就是说，达到了d o 和r 的不动点。如果规则库r 和信息 库d o 是有限的话，信息库中的不动点总是会达到的【m i 。 既然d l 包含d 0 作为它的子集，从d l 派生到d 2 显然重复了以前所有从d o 到d l 的推理。一 种s e m i n a i v ee v a l u a t i o n 方法被提出来解决这个问剐1 2 5 】。基本思想是输入事实规则中的谓词至 少有一个是新的，也就是d l - d o 中有信息。在s e m i - n a i v ee v a l u a t i o n 和所有的前推法搜索中，主 循环是搜索规则库r ，称这种策略为基于规则的策略。在这里，对每一种类型的信息d ，保存 一个相应的新信息数据集【1 6 1 。 定义6 ：中间信息推理引擎应用规则库中的规则由已知信息生成的新信息被称为中间信 息。它可以作为后来新信息的已知信息。 一般来讲，广度搜索的代价是非常昂贵的。然而，它的实现在几何推理中表现得很好。这 是由于：使用了结构化的数据集来减少几何信息库大小，减少内建于规则库内的规则数目。 推理引擎使用的规则库来自于两个方面：一方面是常见的解题方法( 如综合法，向量法等) 抽象为解题规律，将其算法化为相应的规则；另一方面是几何公理系统中的公理、定理等推理 规则。与规则库对应的是谓词库。为了识别和使用各种几何信息，谓词库中的谓词对应于推理 规则中的几何信息的种类。 已知的几种生成可读证明的几何推理软件，推理引擎使用前推法。然而，为了提高推理效 率，还可以适当使用后推法。从假设条件和结论同时出发，如果找到几何信息与结论有交集， 这样的交集信息即可使两种方法继续完成余下的推理。由于余下的推理可以省略，如果后推的 步数不多，就节约了推理的时间。这样的方法就是双向搜索法。用双向搜索法常常能够提高解 6 5 博士学位论文 d o c t o r a ld i s s e r t 棚o n 题效率。只使用前推法，通常也能够满足研究几何推理信息和命题的需求。 以动态几何图形作为输入，推理引擎提取几何信息存储进几何信息库。几何信息库是推理 引擎的数据服务中心。它既是推理规则驱动信息的来源，也是自动出题的资料来源。一个有趣 的事实是，应用规则的顺序是可由新信息的顺序所决定的。当然，用户可以指定谓词的重要级 别。对于经常使用的谓词，如，中点、平行、垂直等，设置高的优先级。在搜索中，程序会根 据优先级进行排序，高优先级会排在新信息的前面。用这种方式，规则的应用顺序会被自动调 整。否则就以规则的复杂程度排序调用。当然，应用推理规则得到的信息也存储在这个几何信 息库中。每次使用规则可得到新的信息，以备以后的规则使用。达到了推理不动点，推理引擎 即可结束推理。否则，继续进行推理。自动推理的推理机制如图4 1 所示。为进一步提高搜索 效率，推理引擎需要动态地更新和查询几何信息库。新信息一旦得到，就被存进信息库和立刻 被使用。 既然几何命题的假设信息是有限的，本文使用的也是一个有限的无符号运算的规则库，不 动点就会达到。很显然，不动点是唯一的，它并不依赖于搜索策略和应用规则库的顺序。 图4 1 可读证明的推理机制 博士学位论文 d o c t o r a ld i s s e r ，口1 0 n 4 3 5 推理链生成 定义6 ：推理链每一条中间信息都有其从初始条件出发，至推导到当前信息的一系列步骤， 称之为推理链。推理链如何生成是一个自动可读证明的关键所在。推理链可输出为可读证明过 程。对于一个证明过程来说，这个中间信息即是结论。 可读证明过程，关键在于跟踪几何信息库中一个给定中问信息的生成过程。由于这个原因， 当更新几何信息库中的一个信息时，把新信息追加在相应的数据集的末尾。同时，也需要保存 这样的信息，比如规则号和使用的源信息。几何信息库中一个信息的实际结构如下： r u l e , 刀? 巨d a t a 其中，r u l e 包含了获得信息所使用的规则，t y p e 则指的是用来获得这个信息的源信息 类型，d a t a 则是源信息在相应的数据集中的序号。 在前面提到过，对于几何信息库中的每一条信息，需要保存这个规则的名称，和驱动信息， 因此，每一个证明步骤都具有如下形式( 后面的向量法是一个特例) ： i n d e x t 】c 皿ji n d e x i n d e x ) 其中，i n d e x k 是c 所当前行的序号，c 是一个简单的中间信息或是已知信息，尼是c 生成 所使用的规则代号，后面的i n d e x m i n d e x k 依是这个当前规则使用的信息的编号。c 是根据下 面所描述的生成过程。这其实是一种后推法。 生成过程：为了找到上面l n d e x t 行的证明过程，需要先找到中间信息c ，至于c 所需要的 每一个i n d e x m ，要么是已知信息，要么是其它的中间信息。如果是已知信息，找出并记录。如 果它是一个是中间信息，则需要找到得到这个中间信息的推理过程，记录在本次推理的前面。 对于每一个这样的中间信息，重复同样的过程。不断在本证明前面插入新的信息。直到所有的 r 不再出现，即当前c 是已知信息。 将证明过程中用到的信息项都依次存储在一个链表中，可以根据这个链表整理证明过程。 使用方法如下： s 1 设置当前结论为当前信息项，将回溯队列清空，证明链表清空。 s 2 查找当前信息项的类型及原因信息序号，取出所使用的信息项，存入回溯队列中。 s 3 若队列不为空，取出并删除回溯队列的队头元素，记入证明链表中，并将其信息设置 为当前信息，转上一步；若队列为空，进入下一步。 s 4 将证明链表逆序整理，经过优化即为推理链。 注意：有些中间信息可能会用到多次，造成推理链的信息冗余。需要在证明完成后进行优 化。方法为消除重复的信息，多次引用重复信息的原始信息即可。i n d e x m i n d e x t 也会替换成相 应的信息在当前推理链中出现的序号。 如果某次推理产生的中间信息是几何信息库中已经存在的信息，那么这次推理就是冗余的。 6 7 博士学位论文 d o c t o r a ld i s s e r r a t i o n 对于提高搜索速度来说，冗余推理是一个巨大的负担。消除冗余信息作为一个研究的基本问题 被l w o s 提出1 1 2 6 1 。已经证实，在通常情况下，消除所有的冗余是不可能的1 1 2 7 l ，所以，最好的 方法是在设计时制定消除冗余的策略，避免用同样的信息多次驱动同一规则。 4 4 基于自动推理的几何自动出题方法 当几何信息的推理结束后，会有许多推理的几何中间信息出现，追踪这些信息就可以给出 解答过程，同时补充几何条件，自动生成完摧的几何题目。 4 4 1 题目条件的生成 定义8 ：自动出题是指利用计算机技术进行测试评估题目的自动生成，包括单个题目生成 与成套题目生成，又称之为题目自动生成。 本文中所指的是中学平面几何中单个题目的自动生成，还增加了验证功能。在限制条件下 的自动推理中，每一个图形相关中间信息的成立，需要推理链作为支撑，这项工作是由自动推 理引擎完成的。然后，只需要补充题目条件和目标信息就可以构成一个完整的题目。 每一个解题过程都是由已知条件开始的，并且中间也会不断使用别的生成信息。检查解题 过程，找出其中所有的已知条件，将其转换成标准的自然语言，按作图的顺利重新组合起来， 即成题目条件。需要指出的是，在一个平常的几何题目习惯用语中，要有相应的转换。比如， 一开始就要指明所处的几何环境：在三角形a b c 中，或在平行四边形a b c d 中等等。 4 4 2 目标信息的限制 定义9 ：目标信息在所有的中间信息中，如果有的信息被推理引擎生成推理链，或是作为 题目需要解答或求证的结论，称为目标信息。目标信息是针对一次具体的推理活动或是题目生 成而言，它是一个临时的结论。生成过程中许多复杂的中间信息容易被指定为目标信息。 但并不是所有的信息都适于作为目标信息来出题，有的是非常简单的，有的是中间数据， 有的信息超出用户的知识和理解范围。因此，选择哪些信息可以作为目标信息来生成题目也是 有限制的。目标信息的限制条件有： ( 1 ) 已知图形条件本身不能做为中间信息。由于所有的信息都会存储在一个几何信息库中， 条件信息和推理信息如果类型相同，也会存储在一个数据集中。所以作图信息有可能会被当作 中间信息，这样的题目是没有意义的。 ( 2 ) 对于某一中间信息解答所用的条件如果没有没有达到全部条件的一半以上，会过多地 浪费了图形中的已知几何元素或是几何关系，也是不符合出题规律的。也就是说，可以取原图 的一部分作为题图，并取有关的部分条件作为题目的前提进行出题。 ( 3 ) 证明中所用到的知识超出了当前阶段所学的几何知识范围，也是不可以用来出题的， 博士学位论文 d o c 蕾o r a l d i s s e r 嗍o n 因为它们超出了学生的知识范围的限制。 4 4 3 题型多样化 几何题目生成的类型是多样化的，有填空、判断、选择、计算和证明等多种类型。一般情 况下，要求证明几何元素之间关系的情况居多。如果目标信息是涉及到了数值计算，则可以出 成计算题的形式。为了增加多样性，当然还可以生成填空、判断或选择等形式。 图4 2 题型多样化 题目的多样化，可以满足出题人的不同的需要和爱好，有利于调整知识考察方式，提高知 识测试的灵活性。题目自动生成，也需要以交互的方式作调整，但在计算机的帮助下可以迅速 完成。创建一个习题有繁复的工作要做。一个习题包括一个反映习题的图形示例，一组用来完 成图形的工具集，和显示给学生的几何题目，答案的验证等。 一个中间信息可以生成各种题型的题目，虽然考察的内容是一致的，然而由于题型不同， 其设计思想也略有差别。 填空题的难度较小，是对推理链的改造。这种题型留出一些关键的知识点或是要考察的重 要规则的结论行，由学生填空。适用于考察对固定知识点的掌握程度。 判断题，根据推理链，对其中一些中间信息进行转换，设置适量的判断项，由此来锻炼学 生的判断能力。学生做这种题型的速度很快。这种题型难度小，有利于提高学生的快速判断能 力。 选择题，结合了填空题与判断题的特点，但也容易令粗心的同学发生错误的选择，这更需 要严密的推理与细心判断。 计算题的难度较大，会花费学生较多的时间，允许学生以各种技巧解题。 证明题是最常见也是较难的几何习题形式。生成的题目只需要给出假设条件和结论，没有 博士学位论文 d o c t o r a ld i s s e r r 纽o n 其它约束。这种题型允许学生以各种方法和技巧来解题，最大程度地让学生自由发挥各人的聪 明才智。 各种题型都有自己的特点，对于不同的知识点可以选择其中一种最合适的方式和需要来生 成相应的题目。 在课本中，一个证明中所有的几何元素一般被放进一个图形中。一个有辅助说明性质的图 形比起单独一个结构复杂的图形来说是更具有可读性。图形化显示解题过程中的几何元素有助 于加强理解。如，线段，角和圆在证明步骤中是经常出现的，只有当这个证明步骤被点击时才 会出现。当另一个与此无关的步骤被激活时，这些元素将会消失。不仅这些证明的每一行可以 被点击查看期待的动态效果，每行的一部分也可以被点击查看，如一行中的一个角z a b c ，是 可点击的，伴随着相应的可视化彩色效果。 4 4 4 多题型的生成与验证方法 测验是学习的一部分。一个好的客观性的测验能显示学习者的理解水平，而一个可靠的解 答验证是必须的，也是必要的。 ， 学生的解答是个人的思考过程，是对知识点的理解和运用。由于思维的差异，理解学生的 解答过程更是一个非常困难的工作。在计算机交互技术的辅助下可以跟踪学生的解答与思维过 程，从而判断解答是否正确。在一个学生解答完成给定的习题之后，就要开始验证学生的答案。 根据不同的题型，使用的验证方法也是不同的。 在自动推理的基础上，根据几何习题的常见题型的不同，本文设计了多题型的生成与验证 方法，如图4 3 所示。 图4 3 多题型的生成与验证方法 7 0 博士学位论文 d o c t o r a ld i s s e r t 明o n 由推理引擎对某一目标信息给出推理链，针对这个链中一些重要的知识点所在的行做处理， 保留为参考答案，并根据常见题的不同，生成题目。用户输入解答后，系统会根据结合预留的 参考答案进行验证，最后给出反馈。具体题型的生成如下： 填空题内容来自于一个特定目标信息的推理链。填空题的生成在推理链中根据知识点的重 要程度有选择地空出关键的条件或几个中间信息，作为空白，供用户填写。同时，保留这些空 白位置的原有字符串作为参考答案。验证时，通过比较相应位置用户的输入与参考答案，可得 答案对与错，给出判断结果。这种练习题特点是，可以给学生以提示，难度显然比证明题要小 一些，但可以考察指定的知识点。 为了加快做习题的速度，减轻学生的书写工作量，培养学生判断正误的能力，还可以把推 理链改造为判断题。判断题的生成是在推理链中，把一些重要的中间信息，替换成一些相似的 目标信息或者不变，供用户对这些重要信息进行判断正误，同时保留替换的结果作为参考答案。 验证时，同样是通过比较用户的选择与预留的参考答案进行比较，给出用户反馈结果。这种题 型以考察学生对中间信息及推理过程的理解，培养学生的判断力和直觉，自测对知识的掌握程 度。 选择题主要是给出正确选项和干扰项。选择题生成时，设置若干干扰项，分别是自动推理 出来的中间信息，如果是数值计算类，则设置为加减异号或数量加倍，如果是证明类，则设置 为将其中某个顶点进行相似代换。这样将其中的三项随机调整为错误的选项，一项保留正确的 选项即可。生成完毕，保留参考答案。验证时，对比用户的选项，不仅对正确选择给出肯定， 还对错误的选项给出对应的正确项。快速剔除干扰项是也是一项对学生判断能力的考察，学生 解答起来较为方便，同时也考察了多个知识点。 有一些结论为多项式类的题目可以出成计算题的形式。计算题生成时，由计算机判断结论 是否符合计算类型，这种类型表现为多项式的加减乘除等方面的运算。如果合适，则将推理链 作为计算过程设为参考答案。验证时，分析主要的中间数据与结论是否符合，根据符合程度给 出正确率。用户可以通过查看参考答案，分析自己的计算过程。当然，可以由用户采用多种方 法来完成，只要过程有理，结果正确即可。 题目生成后，还可以结合当前步骤和图形保存为图片，方便传播和教学使用。自动出题的 结果以文本形式或是x m l 形式保存，供用户进行二次加工或数据交流。 如果一个学生不能正确的理解问题，就非常有可能采取一个不适于本题的方法解答而导致 产生错误的答案。题目生成的质量不仅依赖于生成题目能够很好地考察知识点，也在于能够正 确地区分出用户的答案是否正确。计算与证明的答案验证准确率仍然有待进一步提高。 4 5 实例及分析 使用题目自动生成程序进行解答与验证不仅可以加强对几何知识的理解和学习，更可以将 7 1 博士学位论丈 i ) o c t ( ) r a l 。d i s s e r t a t i o n 看到和用到的知识以另外一种形式保存，方便交流和使用。 创建一个习题，计算机可以代替人做很多一i ：作。自动出题的设计不仅涉及输出普通文本的 i ：作，还包括反映习题的图形，图形条件的生成，结论的分步或整体证明，结论形式的多样化， 显示文本的输出等。 创建习题的操作过程是：由川户根据所要考察的知识点，在一个基丁枢点的动态几何图形 系统上画出覆盖知识点的图形，由推理引擎对所绘图形进行自动推理，推理中间信息显示在导 航信息树上。对于其中信息库的某一中问信息，系统会自动按照当前要证明的目标信息生成解 题过程，从解题过程中找山的已知条件。在优化推理链后，还要优化已知条件。将已知条件， 结论和图形组合在一起后，根据各种题型的特点和算法生成相应的几何题，题型多样。 在儿何中最常见的是要求证明几何关系成立的证明题。以上面的例1 为例，系统为结论生 成的证明过程的形式如卜图。 0 a b c d 是平行四边形( 已知) 1 b c i i d a ( r u l e 2 0 6 0 ) 2 么c f b = 9 0 0 0 ( 已知) 3 l a e d = 9 0 0 0 ( 已知) 4 b c = d a ( r u l e 2 0 60 ) 5 么c b d = 么a d b ( r u l e 0 2 21 ) 6 么a e d ：么c f b ( r u l e 0 0 623 ) 7 f c b 呈a e a d ( r u l e l 0 6456 ) 8 c f 上b d ( 已知) 9 a e 上b d ( 已知) 1 0 f c = e a ( r u l e l 0 97 ) 1 1 a e h c f