摘要：离散数学是现代科学的一个重要分支，是计算机科学中基础理论的核心课程，而谓词逻辑是其中一个十分重要的内容之一。如何将计算机自动推理的另一个经典方法——吴方法引入到离散数学的教学中是本文着重探讨的问题。
关键词：离散数学；自动推理；吴方法
中图分类号：O158文献标识码：A文章编号：1007-9599 (2010) 06-0000-00
Application of Wu"s Method in Predicate Calculus Discrete Mathematics Teaching
Li Yi
(University of Electronic Science and Technology,National Computer Experiment Teaching Center,Chengdu610054,China)
Abstract:Discrete Mathematics is an important branch of modern science,is the basic theory of computer science core curriculum,and predicate logic is one of the important contents.How to Computer Automated Reasoning another classic method - Wu introduced into the teaching of discrete mathematics is the focus of this issue.
Keywords:Discrete mathematics;Automated reasoning;Wu"s method
一、引言离散数学是计算机科学与技术专业的一门核心课程
作为数学的一个分支，其研究的对象是各种各样的离散量的结构及其离散量之间的关系。通过这门课程的学习，可以培养学生们严密的数学思维能力。同时，离散数学与计算机科学中的数据结构、操作系统、编译理论、数字逻辑理论、算法分析、逻辑程序设计、系统结构、容错诊断、机器定理证明、计算机网络、人工智能等课程有着紧密的联系。
离散数学的基础知识主要包括数理逻辑、集合论、抽象代数、格、布尔代数以及图论。对于工科学生，教学中，不仅要从数学的逻辑性和严密性上去论述所涉及的数学理论知识，更要注重培养学生了解这些数学知识在计算机科学诸领域中所起的应用作用。数理逻辑往往是工科学生在学习离散课程中最早接触的内容，且与人工智能和定理机器证明有着极大的联系。因此，如何让学生学好数理逻辑将直接关系到学生逻辑推理能力提高。谓词演算的演绎推理是数理逻辑部分的重点和难点内容，里面涉及到大量的知识点。教学实践表明，工科学生对这部分的内容往往难以掌握。而大部分院校在讲授谓词演算推理时，往往采用“纸和笔”的形式向学生演示整个推理的过程，甚少采用人机交互的方式。
本文中，针对谓词演算的演绎和推理，我们探讨了如何将吴方法引入到该教学内容中，以此从侧面来帮助学生了解数学推理的本质，加深他们对计算机自动推理的认识，提高学习数理逻辑的热情。
二、谓词演算的演绎和推理
在谓词逻辑中，为了研究命题内的内在联系就必须对命题做进一步的分解。
例1：小王是老师
对上述命题进行分解得到：首先，这里的“小王”被称为个体；“是老师”被称为谓词。如果用字每s来表示小王，用字母Q来表示谓词“是学生”。那么，上述命题可表为Q(s)。当需要描述个体间的关系时，就要引入二元谓词。
例2：10小于3
引进谓词Q，则上述命题可表位Q(10,3)。
此外，为了更好地刻画命题函数所表达的意思，往往还需要引进量词： 。在引入了个体、谓词和量词之后，谓词逻辑的表达就更加广泛了。如：
例3：并非所有的实数都是有理数
引进谓词R和Q，有 。
命题演算系统是被包含在谓词演算系统之中。因此，在谓词演算系统内，除了要使用命题演算系统所使用的RP，RT和CP规则外，还要引入关于量词的4条重要性质的推理规则：
US（全称特指规则）：
ES（存在特指规则）：
UG（全称推广规则）：
EG（存在推广规则）：
应用上述4条规则以及命题演算的推理规则，使得谓词演算公式的推理过程可类似于命题演算中推理理论那样进行。这样的推理方法常常需要一些技巧，在教学过程也很少通过计算机向学生演算整个推理过程。为了加深学生对计算机自动推理的理解，并便于人机交互的形式去演示推理过程，我们将计算机代数中的经典推理方法——吴方法引入到谓词演算推理的教学中。不同于前面介绍的经典逻辑推理，吴方法的引入实现了几何、代数命题推理的机械化。
三、几何定理机器证明
定理的机器证明是自动推理和符号计算领域最为活跃的分支之一。我国数学家吴文俊在70年代末提出的吴方法是在计算机上证明和发现几何定理，解决各种几何问题的有效工具。定理机器证明的思想可追溯到17世纪的G.W.Leibniz和R.Descartes。它的目标是要把一类数学问题当作一个整体，建立一种统一的，确定的证明过程，使得该类的定理只要按程序步骤机械地进行下去，在有限步后，就一定能判断出定理的真伪。这方面的工作可分为：以Hebrand理论及归结原理为代表的逻辑方法；以A.Newll及H.A.Simon等人的工作为代表的人工智能方法；以Tarski理论和吴方法为代表的代数方法。吴方法从提出至今，已在世界各国广泛传播，并出现了大量的学术论著。吴方法的发现使初等几何真正跨入了机械化阶段。当人们在初等几何范围内提出新命题而不知真假时，只要上机一试，便知分晓。而人的工作则主要是猜测、发现，并从机器证明的定理中挑选最漂亮的加以分析。吴方法的基本思想非常朴素：把几何命题化为代数形式加以处理。
例4：设梯形ABCD的两条对角线之中点的连线EF与梯形的一边AB相交，那么直线EF将线段AB平分（如图）。
当然，对此例，可以使用谓词逻辑的推理方法进行推断定理的真伪。这种推理方法需要一些技巧才能完成，且推理过程在教学中不便于通过计算机采用人机交互方式进行演示。因此，我们采用吴方法来进行自动推理，使得整个推理过程可通过计算机实时演示，从而使教学过程可视化。根据吴方法，
第一步，选取Descartes坐标系，不失一般性，将各点坐标依次选为：
于是，定理的假设由下列关系构成：
E是AC中点
F是BD中点
M是AB和EF交点
要证明的结论是：
M是AB中点
至此，我们已经完成了吴方法证明定理的第一步：用解析几何方法将问题代数化。剩下的问题就是，在假设一组多项式为0的条件下，求证另一组多项式为0。对本例，这就是：
设 求证
第二步，吴-ritt整序原理。将 或 中的变元 消去，得到一个导元为 的多项式，再用 将该多项式中的 消去，继而将 或 中的 消去。最后得到 的特征列为
其中， 。
第三步，伪除。即对 ，都有 。这说明，在非退化条件 下，定理是成立的。事实上，这些非退化条件是有几何意义的：
AD不与BC重合；
AB不与AD垂直；
ABCD不是平行四边形。
从上述过程易见，吴方法将推理的过程转变为代数方程组整相关的问题。
四、推理平台Maple
上述的三个步骤完全可以在计算机上通过人机交互的方式进行计算推理。这里，我们主要采用计算机代数系统Maple进行上述推理计算。
Maple是1980年由加拿大waterloo大学开发出来的。
当初开发Maple的目的是为了解决繁杂的代数运算问题。如今其版本已提升到Maple13，并已发展成一个相当完备的软件。它提供的数学元算工具相当完备，气符号运算能力使我们能一步一步地进行复杂的公式推导。对例4中的推理，我们仅需要将 对应的表达式键入到Maple工作区中；然后，调用Maple函数 计算 的值是否均为0。若是，则定理为真；否则，定理为假。此方法虽然是代数的，但它提供了一个可视化的方式去引导学生对计算机推理的认识。同时，通过在课堂上比较逻辑推理和吴法代数推理之间的差异和各自的特点，加深学生对谓词演算推理方式的理解。
五、结束语
由于谓词演算的推理涉及到大量规则的使用，因此在利用相关规则推理时，需要一定的技巧性。在教学方法上，针对工科学生的特点，我们不仅要注重启发创新，引入新方法，使教学内容丰富多彩，而且还要培养学生们的严密的逻辑思维能力。具体体现在，教学中，多采用可视化强，可人机交互的方式进行授课，从而便于学生容易理解和接受。对大部分概念都用实例加以说明；强化基本概念的描述，注重基本理论的证明方法。此外，对同一个问题，引导学生采用多种方法进行求解，充分发挥学生的主观能动性。通过开设实验课，使学生们不仅要掌握书上的理论知识，还要让他们了解这些知识的应用背景，真正做到学以致用。
参考文献：
[1]傅彦.离散数学基础及应用[M].电子科技大学出版社,2000.8
[2]左孝凌,李为鑑,刘永才.离散数学[M].上海科学技术文献出版社,1982,9
[3]魏长华,王光明,魏媛媛. 离散数学及其应用[M].武汉大学出版社,2006.6
[4]杨路,张景中,侯晓荣. 非线性代数方程组与定理机器证明[M].上海科技教育出版社,1995,12
[5]吴文俊.几何定理机器证明的基本原理[M].科学出版社,1984、
[6]何锋.离散数学教学中的命题符号化难点讨论[J].计算机教育,2007,(9):38-40
[7]师雪霖,尤枫,颜可庆.离散数学教学联系计算机实践的探索[J].计算机教育.2008,(20):113-115
[8]刘光洁.谈谈离散数学的教学[J].计算机教育,2007,(12):62-64
[9]蔺永政,王新红,李金屏.“离散数学”中实践教学的探讨[J].计算机教育,2006,(10):103-104
作者简介：李轶，男，博士，主要研究方向为：符号计算、程序验证。