吴方法在离散数学谓词演算教学中的应用.docVIP

吴方法在离散数学谓词演算教学中的应用 　　摘要：离散数学是现代科学的一个重要分支，是计算机科学中基础理论的核心课程，而谓词逻辑是其中一个十分重要的内容之一。如何将计算机自动推理的另一个经典方法――吴方法引入到离散数学的教学中是本文着重探讨的问题。 　　关键词：离散数学；自动推理；吴方法 　　 　　中图分类号：O158文献标识码：A文章编号：1007-9599 (2010) 06-0000-00 　　Application of Wus 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;Wus 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条规则以及命题演算的推理规则，使得谓词演算公式的推理过程可类似于命题演算中推理理论那样进行。这样的推理方法常常需要一些技巧，在教学过程也很少通过计算机向学生演算整个推理过程。为了加深学生对计算机自动推理的理解，并便于人机交互的形式去演示推理过程，我们将计算机代数中的经典推理方法――吴方法引