（课程与教学论专业论文）基于前向推理的平面解析几何计算器.pdf

摘要 摘要 几何定理机器证明近3 0 年来取得了一系列令人瞩目盼研究成果，尤其是计算机自动 推理可读证明的突破，使几何定理机器证明的研究成果进入实用性阶段，成为计算机辅 助教学的有力工具，如z + z 智能教育软件系列的平面几何、三角函数、超级 画板等软件。 高中平面解析几何的几何信息多，计算复杂，重复计算工作量大，这都给学生学习 造成了一定的困难。目前常用的计算器多用于数值计算和简单的符号运算，其功能远不 能满足处理解析几何问题的要求。因此，笔者提出并实现了基于前向推理的平面解析几 何计算器。本计算器主要用于平面解析几何方面的推理与演算。 本文第一章简要地回顾了机器证明的发展历程，介绍了智能教育软件的研究现状， 并对本文的工作做了阐述。 第二章详细介绍了系统的实现基础，包括系统实现的环境、代数式系统的实现、谓 词与操作符的选择和测试系统。 第三章详细介绍了笔者的工作思路。第一节介绍了系统实现策略；第二节到第五节 对本系统的系统工作流程、系统解题流程和系统的结构作了具体分析，其中在系统的结 构分析中详细介绍了系统在程序实现中计算信息库部分的四个类：引理类、信息类、计 算类和计算对话框类；第六节举例说明操作符的实现。 第二章和第三章是全文的核心部分。 第四章介绍了计算器的使用并举例说明。 第五章对本文工作的成果和意义加以总结，并指出笔者今后的研究方向。 关键词：自动推理：计算器；谓词：操作符 a b s t r a c t i nt h ef i e l do fm a c h i n e p r o v i n g f o r g e o m e t r yt h e o r e m s ，p e o p l e h a v em a d eg r e a t a c h i e v e m e n t sd u r i n gt h ep a s t3 0y e a r s e s p e c i a l l ya f t e rt h eb r e a k t h r o u g ho fr e a d a b l ep r o v i n g f o rg e o m e t r yt h e o r e m s ，t h ef r u i t so ft h er e s e a r c ho nt h e p r o o f sf o r t h eg e o m e t r yt h e o r e m sh a v e b e e np u ti n t ou s e t h e yb e c o m ei m p o r t a n tt o o l si nc o m p u t e r - a i d e di n s t r u c t i o n ，s u c ha st h e p l a n e g e o m e t r y ，t r i g o n o m e t r i c f u n c t i o na n d s u p e r s k e t c h p a d ，w h i c hb e l o n g t oz + z i n t e l l i g e n te d u c a t i o n a ls o f t w a r e i nt h ep r o c e s so fs t u d y i n gt h ep l a n ea n a l y t i cg e o m e t r yf o rh i g hm i d d l es c h o o ls t u d e n t s ， t h e r ea r em u c hi n f o r m a t i o no f g e o m e t r y ，b o t hh e a v ya n dc o m p l e xc a l c u l a t i o n s ，w h i c hm a k e s t h e mf e e lm o r e d i f f i c u l t l y h o w e v e rn o w a d a y st h en o r m a lc a l c u l a t o ri sa l w a y sb e i n gu s e di n n u m e r a lc a l c u l a t i o na n ds y m b o l so p e r a t i o n ，w h i c hi sn o te n o u g hf o rs o l v i n gt h ep r o b l e mo f a n a l y t i cg e o m e t r y - s ot h ea u t h o rp u t sf o r w a r dt h ec a l c u l a t o ro f p l a n ea n a l y t i cg e o m e t r yf r o m a u t o m a t i cr e a s o n i n g ，w h i c hb a s e so nt h ef o r w a r d r e a s o n i n g t h ec a l c u l a t o rc a l lb ew i l d l yu s e d i nr e a s o n i n ga n d f i g u r i n g i n p l a n ea n a l y t i cg e o m e t r y i nc h a p t e ro n e ，t h ea u t h o rr e v i e w st h em a c h i n e r yd e m o n s t r a t i o na n di n t r o d u c e st h e s t a t u so f i n t e l l i g e n ts o f t w a r e i nc h a p t e rt w ot h ea u t h o ri n t r o d u c e st h eb a s eo f s y s t e m ，w h i c hi n c l u d e st h er e a l i z a t i o n o fc i r c u m s t a n c e ，t h er e a l i z a t i o no f a l g e b r as y s t e m ，t h es e l e c t i o no fp r e d i c a t e sa n do p e r a t i o n a l s y m b o l s ，a n dt h et e s t i n go fs y s t e m i n c h a p t e rt h r e et h ea u t h o ri n t r o d u c e sh i st h i n k i n gp a r t i c u l a r l y i ns e c t i o no n e ，t h e a u t h o ri n t r o d u c e st h es t r a t e g i e so fs y s t e mr e a l i z a t i o n ；f r o ms e c t i o nt w ot os e c t i o nf i v et h e a u t h o ra n a l y s e st a c t i c a lr e a l i z a t i o no f s y s t e m ，f l o wc h a r to fs y s t e mw o r k i n ga n df l o wc h a r to f s o l v i n gs y s t e m i na n a l y s i s o f s y s t e m sf r a m e w o r k , t h ea u t h o ri n t r o d u c e s f o u rc l a s s e s ： c l e m m a , c i n f o ，c c a l c u l a t ea n dc c a l c u l a t o r d l g s e c t i o ns i xd e m o n s t r a t e st h er e a l i z a t i o no f o p e r a t i o n a ls y m b o l s t h e c h a p m r t w oa n d c h a p t e r t h r e ea r et h ek e r n e lo ft h i sa r t i c l e i nc h a p t e rf o u rt h ea u t h o ri n t r o d u c e st h ec a l c u l a t o ra n d g i v e ss o m ee x a m p l e s i nc h a p t e rf i v et h ea u t h o rs u m m a r i z e st h e p r o d u c t i o na n ds i g n i f i c a n c ea b o u tt h ea r t i c l e ， a n d g i v e ss o m es u g g e s t i o n sf o rr e s e a r c h k e y w o r d s ：a u t o m a t i c r e a s o n i n g ；c a l c u l a t o r ；p r e d i c a t e ；o p e r a t i o n a ls y m b o l t t t 广州大学学位论文原刨性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指 导下，独立进行研究工作所取得的成果。除文中已经注明引 用的内容外，本论文不含任何其他个人或集体已经发表或撰 写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已在文中以明确方式标明。本人完全意识到本声明的法律 后果由本人承担。 学位论文作者签名：礴鼹 日期：7 。口了年占月砂日 广州大学学位论文版权使用授权书 本人授权广州大学有权保留并向国家有关部门或机构送 交论文的复印件和磁盘，允许论文被查阅和借阅。本人授权 广州大学可以将学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存、汇 编学位论文。( 保密的学位论文在解密后适用本授权书) 7 l 学位论文作者签名：端、尊日期：瓣g 月三日 导师签餐圈李。计日期一礴月j 日 第一章绪论 第一章绪论 1 1 几何机器证明研究概况 用机械的方法解决千变万化的几何问题，曾是历史上一些卓越科学家的梦想，他们 在这条道路上进行了艰辛的探索。 用一个固定的章法解决一类问题，这是数学机械化的基本思想口1 。能不能有一个办 法，把许多证明题转变成有一定章法可循的计算和推理，这样，便人人都能证几何题了。 这种愿望由来已久。但直到十七世纪，法国数学家笛卡尔( d e s c a r t e s ) 创立了解析几何， 使初等几何问题代数化，把无章可循的几何证明题纳入了有一定规范形式的代数框架， 为后来的几何定理机器证明打下了基础。德国数学家莱布尼兹( l e i b n i z ) 曾有过“计算 机器”的设想，并为此研究过逻辑，设计并造出了能做乘法的“计算机”。二十世纪初， 德国大数学家希尔伯特( h i l b e r t ) 在他的名著几何基础中提供对某一类几何命题的 机械化解题方法。 电子计算机的出现，大大加快了数学机械化研究的进程，也促进了几何问题求解机 械化的研究m 。波兰数学家塔斯基在1 9 5 0 年证明了一个引人注目的定理：“一切初等几 何和初等代数命题构成的命题类，是可判定的“1 ，。塔斯基( t a r s k i ) 的证明是构造性 的。也就是说，他确实提出了一套能判定任一个初等几何或初等代数命题的机械化方法。 遗憾的是这个计算复杂度太大了，即使使用高速的计算机也不可能在合理的时间内证明 稍微复杂点的几何定理。 塔斯基的办法是：先利用笛卡尔坐标把几何问题化为代数问题，再用代数方法来解 决问题。以此为线，发展了几何问题机器证明的代数方法。1 9 7 5 年，考林斯( c o l l i n s ) 提出了“柱面代数分解方法”，比塔斯基的方法效率提高了很多，但在计算机上还只能 解决稍微复杂点的几何问题。笛卡尔塔斯基考林斯，这是用代数方法寻求几何 问题机械化求解的一条发展线路。 而另一条线路是试图把解决几何问题的传统综合方法机械化。这条线路是格兰特 ( g e l e r n t e r ) 在1 9 5 9 年发表的一篇论文中提出来的伫】。它是从结论出发进行推计算的 方法。1 9 7 5 年，奈文斯( n a i v i n sa j ) 又提出了更有效的前推搜索法。这种方法又叫 基于前向推理的平面解析几何计算器 做逻辑方法，或叫做人工智能方法。该方法的优点是能产生传统风格的证明，但由于搜 索的空间过大的问题，未能形成有效的算法。 在几何问题求解机械化研究举步维艰的3 0 多年的时间里，数学机械化的研究和应用 在总体上还是有了长足的进展。计算机原来只会进行数值计算，到2 0 世纪6 0 年代中期， 用它也能进行符号计算了。 数学机械化的发展为几何解题机械化研究提供了广阔的发展空间。中国在这方面有 了重大的突破。1 9 7 7 年，我国著名的数学家吴文俊院士在中国科学杂志上发表了题 为“初等几何判定问题与机械化证明h 的论文，提出了一个证明等式型初等几何定理 的新的代数方法。这个方法虽然不能证明几何不等式，但在证明等式型几何定理时的效 率比使用以前的方法高得多。1 9 8 4 年，中国留美学者周咸青在他的博士论文中将这种方 法叫做“吴法”眦9 1 ”1 ，并列举了他基于吴法所编写的程序证明的1 3 0 个非平凡的几何定 理。不久，他又在他的一本专著中列出了用吴法证明的5 1 2 个几何定理。吴法从此在国 际自动推理研究领域广为传播，并使几何定理机器证明的代数方法的研究空前活跃起来。 吴法的成功，使在计算机自动推理的研究中曾经最不成功的几何定理的机器证明成为最 成功的领域。 1 9 9 2 年，中科院院士张景中先生访问美国进行合作研究期间，将他以前提出的系统 的面积解题方法和消点算法结合起来，应用于几何定理机器证明的研究，使几何定理可 读证明的自动推理这个三十年来进展甚小的难题得到突破。在和周咸青、高小山的合作 研究中，形成了消点算法，并用l i s p 编写了程序实现算法，在n e x t 工作站上产生了4 0 0 多条非平凡的几何定理的可读性证明。从而使几何定理可读机器证明取得了突破性的进 展。 1 9 9 7 年以后，张景中院士将其多年的研究成果，应用到我国的中小学数学教育事业 中。他带领广州大学计算机教育软件研究所开发了z + z 系列智能教育软件，开辟了几何 定理的可读性机器证明应用的新领域智能教育软件。 1 2 智能教育软件的研究现状 进入二十一世纪，随着计算机技术的飞速发展和家用电脑的日益普及，利用计算机 进行辅助教学也逐渐成为一种趋势。于是在国内形成了一个广阔的教育软件的市场，吸 引了众多的软件开发人员和企业投入到教育软件的研发行列。教育软件的市场出现了前 2 第一章绪论 所未有的繁荣。但同时这也带来了教育软件产品质量的良莠不齐，特别是真正的高质量 的智能教育软件甚少。一些企业只注重眼前的利益，其产品不能真正和学科特点相结合， 相当一部分只是属于“课本搬家”和“题库”式的软件。这其实也就是将知识从一种载 体机械地转移到另一种载体上，并不能利用计算机进行个性化教学。 同时，由于许多教育软件开发者对教育理论的研究，导致当前教育软件的应用无法 达到理想的效果。问题突出表现在以下几个方面：交互性、动态性和智能性不强，未能 真正与学科特点相结合，制作不够精细，使用复杂等。随着硬件技术、现代网络技术、 人工智能技术、多媒体技术和教育技术等的不断发展，新一代的智能教育软件已经崭露 头角了。 张景中院士提出的独具特色的“智能教育平台”的概念和理论。将自动推理理论应 用到了智能教育软件的研究和应用上，并进行了大量的教学实践。近几年来，针对目前 教育市场对智能教育软件的迫切需求，张景中院士带领研究人员开发了z + z 系列软件平 台2 1 ，如超级画板软件嘲就是近期由张景中院士、李传中副研究员开发的z + z 智能 教育平台的系列之一。这种新型的智能教育软件的特色在于：( 1 ) 与题库、课件资源库 不同，它所包含的学科内涵资源是即时生成的，并且提供了资源加工和创作的工具，使 教师和学生有广阔的发挥空间，体现了智能教育软件的动态性和智能性特点；( 2 ) 与国 内外常见的多媒体可见开发平台不同，它能够从学科专业的层面支持教学的全过程，而 非一个多媒体的编辑器，真正的结合其学科特点；( 3 ) 与国外的数学解题软件、几何作 图软件不同，它能提供自动推理、计算、逻辑动画生成、程序编写环境及符号运算等丰 富的功能： ( 4 ) z + z 系列智能教育软件操作简单，易学易用，既能应用于教师的教学也 适用于学生的自学。由此看来，智能教育软件的发展将为教育事业的发展提供更广阔的 空问。 1 3 本文的工作 目前现有的智能软件实现的计算机的自动推理，是用户输入题目，再选择选择自动 推理，然后就等着计算机给出答案。在整个计算过程中用户都无法了解系统是如何工作， 题目是如何被求解出来的。能否有一个系统能让用户“随心所欲”地运用规则一步一步 地解决问题，就像一个计算器那样，用户可以自己选择运算数值和运算符进行运算，宜 到算出整个算式的值。于是笔者从普通计算器出发，采用计算机自动推理中的前向推理 基于前向推理的平面解析几何计算器 技术尝试实现一个功能更强大的计算器。 高中平面解析几何课程有以下几个特点：几何信息多，计算复杂，重复计算工作量 大。一个数学题目的解法可以是多样的，但重要的是培养学生的学习方法和解题能力。 比如：己知两点的坐标，求两点间的距离，这完全可以由两点间的距离公式直接计算出 来。此时，知道使用两点间距离公式去求解比具体的计算过程更重要。于是笔者以平面 解析几何为内容去研究实现这样的一个基于前向推理的计算器。 本文重在研究基于前向推理的平面解析几何计算器的设计与实现。计算器的基本计 算功能的实现采用了自动推理领域的前向推理技术，能进行平面解析几何范围的计算。 本款计算器的运算符是平面解析几何中的定义、定理和公式等。除了能进行单步的计算 外，还能进行多步计算来解决一个完整的平面解析几何问题，从题目所给出的条件出发， 通过使用计算器中的运算符解出该题目的答案。除了能进行计算外，本款计算器还具有 解题功能。 这样的一个计算器在学生的学习中可以帮助学生减少重复计算的计算量。对于一个 问题，使用本款计算器可以使用不同的方法进行计算，从而激发学生的学习兴趣。同时， 教师也可以使用本计算器进行课后备课和课堂教学。本计算器是一款应用于平面解析几 何学习和辅助教学的智能教育软件。 本文第一章简要地回顾了机器证明的发展历程，介绍了智能教育软件的研究现状， 并对本文的工作做了阐述。 第二章详细介绍了系统的实现基础，包括系统实现的环境、代数式系统的实现、谓 词与操作符的选择和测试系统。 第三章详细介绍了笔者的工作思路。第一节介绍了系统实现策略；第二节到第五节 对本系统的系统工作流程、系统解题流程和系统的结构作了具体分析，其中在系统的结 构分析中详细介绍了系统在程序实现中计算信息库部分的四个类：引理类、信息类、计 算类和计算对话框类；第六节举例说明了操作符的实现。 第四章介绍了计算器的使用并举例说明。 第五章对本文工作的成果和意义加以总结，并指出笔者今后的研究方向。 1 4 本章小结 机器证明的发展经历了一个艰辛的探索过程，并在中外很多科学家的不懈努力下取 4 第一章绪论 得了很大的突破。智能教育软件是机器证明的实际应用领域之一。目前大多数的智能教 育软件强调的只是多媒体在计算机辅助教学中的应用，没能真正结合学科及课程的特点， 不能体现智能教育软件的交互性、智能性、实用性强等的特点。 考虑到智能软件要真正做到与学科课程相结合，体现交互性、智能型和实用性等特 点。根据高中平面解析几何课程的几何信息多，计算复杂，重复计算工作量大等这些特 点，笔者提出了基于前向推理的平面解析几何计算器。本计算器在学生的学习中可以帮 助学生减少重复计算的计算量。并通过运用不同方法解题，激发学生的学习兴趣。同时， 教师也可以使用本计算器进行课后备课和课堂教学。 第二章系统实现的基础 第二章系统实现的基础 2 1 系统实现的环境 平面解析几何计算器的系统( 以下简称本系统) 是基于m i c r o s o f tv i s u a lc + + 6 0 环境开发完成的。v i s u a lc + + 是支持面向对象的程序设计方法( o o p - - o b j e c t o r i e n t e d p r o g r a m m i n g ) ，支持m f c ( m i c r o s o f tf o u n d a t i o nc l a s s ) 类库的编程环境，有强大的集成 开发环境，可用于开发各类应用程序，功能十分强大，是目前比较流行的编程环境之一。 本系统包含三个大的系统模块，分别是：代数式系统模块、计算信息库系统模块和 用于外部信息输入及测试系统模块。 这三个模块都在m f c 类库中使用了集合类来定义数据结构。集合类是用来处理一组 数据对象或标准数据类型变量的c + + 类。每个集合类的对象都是一个独立的对象。类成 员函数可以作用于此集合内的所有元素。 根据对象在集合类中的组织和存储方式，在盯c 类库中用户可自定义集合类为模板 类。有三种模板类型：链表模板类( c t y p e d p t r l i s t ) 、数组模板类( c t y p e d p t r a r r a y ) 、 映射模板类( c t y p e d p t r m a p ) 1 4 1 。根据编程的实际需要，选择适当的模板类型。本系统 选择了链表模板类c t y p e d p t r l i s t 作为数据的存储方式。 类c t y p e d p t r l i s t 为类c p t r l i s t 的对象提供了一个类型安全的“包装”。当使用 c t y p e d p t r l i s t 而不是c o b l i s t 或c p t r l i s t 的时候，c + + 类型检查工具可帮助消除不匹 配的指针类型引发的错误。另外，c t y p e d p t r l i s t 包装实现了许多在使用c o b l i s t 或 c p t r l i s t 是要实现的强制转换。因为所有的c o b l i s t 或c p t r l i s t 函数都是内联函数， 所以使用这个链表模板类不会明显地影响代码的大小和速度。 链表模板类提供了一个动态大小的存储空间。链表通过a d d h e a d 或a d d t a i l 将一个 元素( 或一个数组中的所有元素) 添加到链表的头部或尾部；用g e t h e a d 或g e t t a i l 来 返回链表的头或尾元素；用g e t n e x t 获取当前的下一个元素；用g e t a t 获取在一个给定 位置的元素；用r e m o v e h e a d 或r e m o v e t a i l 从链表的头部或尾部删除元素。 下面是系统中的代数式系统模块使用自定义链表模板类的例子： 定义继承于c o b l i s t 的链表模板类c l t e m l i s t 基于前向推理的平面解析几何计算器 t y p e d e fc t y p e d p t r l i s t c i t e m l i s t ： 创建c l t e m l i s t 的对象，用于存储代数式的每一项i t e m c i t e m l i s tm i t e m l i s t ； 创建c i t e m 类的对象 c i t e m * p i t e m = n e wc l t e m ( s l t e m ) ： 将p l t e m 添加到链表的后面 m _ i t e m l i s t a d d t a i l ( p i t e m ) ： 2 2 代数式系统的实现 因为平面解析几何中有大量的四则运算、代数式运算、方程求解和变量代换等。所 以本系统需要一个能满足平面解析几何范围内运算要求的代数式系统，能够处理的问题 包含：判断表达式对错、去除表达式中的空格，采用递归将表达式分成项和因子，去除 项中的括号、判断表达式是否多项式、合并同类项、计算最大公约数、将表达式展开、 变量的替换、给出指定变量的系数或次数、给定变量的值计算多项式、解方程，等等。 于是笔者设计实现了一个代数式系统，以实现上述功能。代数式系统的实现是实现本系 统的基础部分。 代数表达式由表达式、项、因子组成，其中项分成分子项和分母项，因子分成数字、 变量、代数式和函数。 其数据结构可描述为： 代数式( a l g e b r a ) ：= 项( i t e m ) 们t e m ，= 恶鬻瑟 f a c t o r 卜巨兰， f 数字 其中，( 1 ) 数字：实数；( 2 ) 变量：简单的变量，如x ，y ，a ，b 等；( 3 ) 代数式：+ 扫) 5 或 x + z 等；( 4 ) 函数：一些初等函数，参数五，屯，是一些代数式，如s i n ( 2 x ) ，l o g ( a ，b + x ) 等。下图是代数表达式的数据结构图2 1 。 图2 1 代数表达式结构图 f i g u r e2 - 1f r a m em a po fa l g e b r ae x p r e s s i o n 代数式系统的程序采用m i c r o s o f tv i s u a lc 十+ 的m f c 类库编写实现。程序的实现设 计了四个类：e m g e b r a 类、c 1 t e m 类、c f a c t o r 类和e v a r i a b l e y a l u e 类。四个类的作用 和定义如下： 1 c a l g e b r a 类的作用是：取到输入的表达式，检测表达式是否合法( 输入错误、括 号匹配等) ，然后将合法的表达式按“+ ”号或“”号分解成项( i t e m ) 存入链表中。 下面是e a l g e b r a 类的变量定义和一些函数定义。 c l a s sc a l g e b r a ：p u b l i cc o b j e c t t p r o t e c t e d ： c s t r i n gm _ s e r r m s g ： 错误的信息 b o o lmb e r r o r ：是否出错 c l t e m l i s tmi t e m l i s t ：存储代数式的每一项i t e m v o i ds t r i n g t o i t e m l i s t ( c o n s tc s t r i n g & s e x p r ，c s t r i n g l i s t & i t e m l i s t ) ： 把表达式放入表中 b o o ls e t i t e m ( c o n s tc s t r i n g & s i t e m ) ： v o i di t e m s o r t ( c l t e m l i s t & i t e m l i s t ) ：对每一项进行排序 p u b l i c ： c i t e m l i s t * g e t l t e m l i s t0 r e t u r n & m _ i t e m l i s t ：) ： b o o li s e r r o r ( ) r e t u r nm _ b e r r o r ；)判代数式是否出错 c s t r i n gg e t e r r o r m s g0 ：返回异常信息 s t a t i ci n tb r a c k e t m a t c h p o s ( c o n s tc s t r i n g & s i t e m ，i n tn p o s ) ： 判断括号是否匹配 s t a t i cb o o li s n u m b e r ( e o n s t c s t r i n g & s n u m ，c o e f f t y p e & n n u m ) ： 丢掉项中的括号 b o o li s o n e l t e m ( ) e o n s t r e t u r nm _ i t e m l i s t g e t c o u n t 0 = = l ：) ： 判断表达式是否只有一项 v o i dd i v i d e b r a c k e t ( ) ：去除括号 v o i dc o m b i n e s a m e i t e m ( ) ：合并同类项 i n tb i g c o m d i v ( i n tn n u m ，i n tn d e n ) ：计算最大公约数 c a l g e b r a ( ) ： c a l g e b r a ( c o n s tc s t r i n g & s t r ) ：构造函数1 c a l g e b r a ( c o n s tc a l g e b r a & a 1 ) ；构造函数2 v i r t u a l c a l g e b r a ( ) ： c s t r i n gt o s t r i n g0c o n s t ：连成串 以下为对表达式的一些基本操作 v o i de x p a n d ( ) ：表达式的展开 v o i ds u b s t ( c o n s tc s t r i n g & s v a r ，c o n s tc a l g e b r a & a 1 ) ：变量的替换 v o i dg e t v a r i a b l e ( c s t r i n g l i s t & v a r l i s t ) ：取得表达式中的变量，将 其放入一链表中 b o o li s p o l y ( c o n s tc s t r i n g & s y a r ) c o n s t ：判断表达式是否多项式 b o o li s v a r i a b l e ( c o n s tc s t r i n g & s y a r ) ； 判断变量是否在表达式中 i n td e g r e e ( c o n s tc s t r i n g & s v a r ) ： 指给定变量的指数 c a l g e b r ac o e f f ( c o n s tc s t r i n g & s v a r ， c o n s t i n t & n d e g r e e ) ： 指给定变量的系数 b o o li s o n e t i m e ( c o n s t c s t r i n g & s v a r l ，c o n s tc s t r i n g & s y a r 2 ) ： 1 n 第二章系统实现的基础 判断多项式是否一次多项式 b o o l i s t w o t i m e ( c o n s tc s t r i n g & s v a r l ，c o n s tc s t r i n g & s v a r 2 ) 判断多项式是否一次多项式 c a l g e b r ag e t t w o c o e f f ( c o n s tc s t r i n g & s v a r l ，e o n s tc s t r i n g & s v a r 2 ， c o n s ti n t & n d e g r e e l ，c o n s ti n t & n d e g r e e 2 ) ： 取出二元多项式的二元系数 d o u b l eg e t g a l u e ( c m a p s t r i n g t o o b & v a r l i s t ) ： 映射表中取值 j 下面以c a l g e b r a 类的将表达式分解成项存入到链表的函数s t r i n g t o i t e m l i s t ( ) 为例来说明如何把我们输入的表达式拆项并放入项的链表中。 v o i dc a l g e b r a ：s t r i n g t o i t e m l i s t ( c o n s tc s t r i r l g s e x p r ，c s t r i n g l i s t & i t e m l i s t ) i n tn f r o m = 0 ： 第一项的首位置在0 处 i n tn l e n = s e x p r g e t l e n g t h 0 ：表达式的长度 f o r ( i n ti = o ：i c 。 定义2 3 在进行计算时，选择的条件满足某条操作符，此时将这些条件的谓词放入 信息库中，称为组对。满足此种组对的操作符就是组对条件。有时满足某条操作符的条 件很多，要选择适当的条件进行组对。 2 3 1 谓词的表示和选择 在进行计算时首先要合理的选择一些谓词，谓词的选取应尽量能反映平面解析几何 命题中的事实。谓词数目的多少也直接影响本系统的计算能力。但也并非越多越好。谓 词的表示和选择要结合学科课程的特点，本系统目前用了变量v a r i a b l e 、线段长度 l e n g t h 、点p o i n t 等共3 2 个谓词。表2 - 1 是详细列出了本系统所选取的谓词。 表2 - i 谓词选取表 t a b l e2 1p r e d i c a t e ss e l e c t i o n 序号谓词意义 1v a r i a b l e变量 2 l e n g t h线段长度 3p c l i n t点 4 e q u a l o f s e g m e n t线段相等 5p o i n t o n l i n e点在直线上 6r a t i o o f p o i n t点的定比分比 7m i d p o i n t线段中点 8c o n c l i n e点共线 9t g c e n t r e三角形的重心 i 0 s e g m e n t r a t i o线段成比例 l l e q u a t i o n方程 1 2l i n e 直线 1 3 l i n e s u p e r p o s直线重合 1 4l i n e p a r a l l e l 直线平行 1 5l i n e v e r t i c a l 直线垂直 1 6 l i n e a n g l e直线的夹角 基于前向推理的平面解析几何计算器 续表2 - i 1 7l i n e i n t e r s e c t线相交 1 8p o i n t l i n e d i s t a n c e点到直线的距离 1 9p a r a l l e l d i s t a n c e平行线间的距离 2 0c i r c l e 圆 2 1 l i n e c i r c l e t a n g e n c y直线与圆相切 2 2 e 1 1 i p s e椭圆 2 3 h y p e r b o l a双曲线 2 4p a r a b o l a 抛物线 2 5p o i n t o n c i r c l e 点在圆上 2 6p o i n t o n e l 1i p s e 点在椭圆上 2 7 p o i n t o n h y p e r b o l a点在双曲线上 2 8p o i n t o n p a r a b o l a 点在抛物线上 2 9 c i r c l e t a n g e n c y圆和圆相切 3 0f l a t m o v e 平移 3 1p a r a m e t e r 参数 3 2p o l a r c o o r d i n a t e s 极坐标 本系统目前共用了3 2 个谓词，但这些谓词不足以能够表达所有的情况。比如直线就 有很多情况。本系统把所有的直线情况都用谓词l i n e 来表示，为了减少谓词的个数又用 一个枚举变量m _ n c o o r c o u n t 来在谓词中更细的区分谓词的情况，使本系统的结构更紧 凑。下表2 - 2 列出了谓词直线( l i n e ) 表述的直线的情况，用枚举类型来区分直线情况。 表2 - 2 谓词l i n e 表述的直线类型 t a b l e2 - 2t y p eo fp r e d ic a t el i n e 序号变量的枚举值 谓词l i n e 表述的直线类型 1 0 或2 0直线的斜率 2 1 或2 l 直线的倾斜角 3 2 或2 2 直线在x 轴上的截距 1 8 第二章系统实现的基础 续表2 - 2 43 或2 3直线在y 轴上的截距 54 或2 4 直线的一般方程式方程 65 或2 5 直线的点斜式方程 76 或2 6 直线的两点式方程 87 或2 7 直线的斜截式方程 98 或2 8 直线的截距式方程 1 09 或2 9 直线的参数方程 除了直线( l i n e ) 以外，还有需要通过一个枚举变量来细分谓词类型的还有：圆 ( c i r c l e ) 、椭圆( e l l i p s e ) 、抛物线( p a r a b o l a ) 、参数( p a r a m e t e r ) 。 2 3 2 操作符的表示和选择 本系统的操作符是高中平面解析几何中的公理、定义、定理、引理、公式等。本系 统采用的是前向推理策略，也就是根据已知条件，找到合适的操作符，然后进行计算， 得到结果。 前向推理策略可用符号表示为：i f t h e n ， 其中i f 语句部分确定了这个操作符可以被采用的先决条件，t h e n 语句部分描述使用这 条操作符所得出的结果。如果某个操作符被选用，则表示其前提条件已经被满足，从而 就可以对条件进行计算了。下面给出了本系统所用的有向线段和定比分点部分的操作符： 操作0 ：求两点间距离 操作1 ：由定义球分比 操作2 ：中点坐标公式列方程 操作3 ：已知重心，确定重心的分比 操作4 ：线段的比例方程 操作5 ：此操作没有实现 操作7 ：已知分比，列方程 操作8 ：线段相等，列方程 基于前向推理的平面解析几何计算器 说明：这里有部分操作符是空的，是因为按高中平面解析几何教材内容而定，留有 一些空的操作符，以便以后增补。 2 4 测试系统的介绍 本系统是在“平面解析几何计算器( t h ec a l c u l a t o ro fp l a n ea n a l y t i cg e o m e t r y ) ” 基础上进行开发和测试，该平台具有界面直观、操作简便等特点。图2 2 为该系统的主 界面图。条件的输入是在系统的主界面中通过作图而产生的。作图系统有作图工具栏和 作图菜单两项互为补充，如图2 3 和图2 4 。 图2 - 2 计算器的主界面 图2 - 3 作图工具栏 f i g u r e2 - 3t o o l b a ro fc o n s t r u c t i o n 2 0 第二章系统实现的基础 图2 4 作图菜单 f i g u r e2 - 4m e n uo fc o n s t r u c t i o n 用户通过一个交互的对话框来进行计算，即可以单击菜单中的“解题”下的“解析 几何计算器”来打开计算对话框，如图2 5 。 2 5 本章小结 图2 - 5 计算器对话框 f i g u r e2 - 5d i a l o gb o xo fc a l c u l a t o r 平面解析几何计算器是基于m i c r o s o f tv i s u a lc + + 6 0 环境开发完成的，其中包含 三个系统模块：代数式系统模块、计算信息库系统模块和用于外部信息输入及测试系统 模块。本文首先具体分析了系统实现的基础部分代数式系统，代数式系统共分了四个类 2 l 基于前向推理的平面解析几何计算器 来完成各部分功能。然后介绍了实现计算信息库系统的基础的三个基本概念：谓词、操 作符和条件组对，并列出了本系统中全部的谓词及部分的操作符。最后介绍了外部信息 输入及测试系统。计算器提供了作图工具栏和作图菜单两种作图方式，完成用户信息的 输入。信息输入完成后打开“解析几何计算器”，从条件出发，选用操作符来进行计算。 3 1 系统实现策略 第三章系统的实现 本款计算器采用了计算机自动推理的前向推理技术。将前向推理技术应用于平面解 析几何计算器的思想源自于普通计算器。普通计算器主要对数值进行计算，其计算的方 法是选定两个数，然后选择对这两个数进行操作的运算符，最后计算出结果。下表比较 了平面解析几何计算器与普通计算器。 表3 - 1 两种计算器的比较 t a b l e3 - 1c o m p a r i n go ft w oc a l c u l a t o r s 两种计算器的比较平面解析几何计算器普通计算器 运算对象解析几何对象的属性、对象之间的关系、方程等数值 运算符操作符( 定理、定义、公式)四则运算符与三 角函数运算符 运算结果数值、解析几何对象的属性、对象之间的关系等数值 从两个计算器的比较可以看出，平面解析几何计算器是对解析几何对象的属性、对 象之间的关系、方程等进行计算的。于是要选择计算的对象也就是条件，然后选择操作 符进行计算。但需要说明的是，在选定了条件后并不是所有的操作符都有用，而是根据 条件在系统内部已给出判断哪些操作符有效，要选有效的操作符才能够进行正确的计算。 本系统的系统策略如图3 - 1 。 团、 粤 + 困昌困