命题公式范式生成算法研究与程序设计
摘   要

自动推理是人工智能领域的一个重要研究课题。从若干事实出发，经过严密的推理，得出某些结论，是人类一项重要的智能活动。不过自动推理还是个处于初级阶段，仍需不断实验的领域，但这个领域又是非常的诱人，因为在数学以及许多其他技术领域均可用一定的形式系统来表述。而一阶逻辑是一种特别简单又易于理解的语言，足以表达许多的问题。这样用今天的计算机进行快速而准确的推理已成为可能，而自动推理又可以避免令人乏味和容易出错的详细证明构造过程，所以这是一个非常值得我们去讨论的领域。计算机自动推理的研究走着两条不同的路线:研究普遍的推理规律和方法 ——逻辑推理研究，以及研究具体领域的推理规律和方法。
而本文是自动推理原理在离散数学上应用的实例，利用自动推理的思想来研究命题公式范式的生成算法等内容，通过研究本课题，可以产生一个类似命题证明器的系统。利用这个系统就可以对命题公式语法的正确性进行判定以及命题公式范式的生成。在本文中首先回顾了自动推理的历史，叙述了命题公式范式在自动推理中的重要性，以及自动推理的现状及发展趋势；然后叙述了命题逻辑的定义及原理；接着对c语言进行了简单的概述；最后讨论了命题公式范式生成算法以及实现。

关键词：自动推理  定理机器证明  命题逻辑公式  合取范式  析取范式    数理逻辑

Study the make algorithm of the formula normal form of the proposition and design the program
Abstract
  Automatic reasoning is an important subject for research of the artificial intelligence field. Proceed from several facts, through tight reasoning, draw some conclusions; it is an important intelligence activity of the mankind. But automatic reasoning piece still at primary stage, is a field that also need test constantly, but this field is very captivating, because it can state with certain form system in mathematics and a lot of other technological fields. And as a step of logic is a kind of very simple language that is very easy to understand, it is enough to express a lot of questions. So use for today’s computer that carry on fast and accurate reasoning has  already become a  possible, and construct the course in detailed identification that making people dull and apt to make mistakes in automatic reasoning can avoid, so this is a good field that we worth to go and discuss very much . There are two different routes to go in the research of the automatic reasoning of the computer: Study general law and method of reasoning——study  reasoning from logic, and study the law and method of  reasoning  in the specific field.
And this text is the instance that the automatic reasoning principle uses in dispersed mathematics, make use of thought of automatic reasoning to study such contents as the formulation algorithm of the formula normal form of the proposition, etc., through studying a subject, can produce a system which is similar to the Proving theorems by computers. Utilize this system to carry on the formulation of judging and proposition formula normal form to the exactness of the formula grammar of the proposition. Have reviewed the history of automatic reasoning, narrated the importance of the proposition formula in automatic reasoning of normal form, and introduced the current situations and development trends of automatic reasoning at first originally in this article; Then narrated the definition and principle of the logic proposition; Then has carried on the simple summary to the c programming language; Discussed finally the formula normal form of the proposition turns into the algorithm and realizes.

Keyword:  Automatic theorem proving   Proving theorems by computers   Logic formula of the proposition   Conjunction normal form   Extracted normal form   Mathematical logic    
 
 目  录

摘   要 II
Abstract III
第一章 绪 论 1
1.1数理逻辑在自动推理中的意义 1
1.1.1数理逻辑的若干新发展 1
1.1.2逻辑与人工智能 2
1.1.3命题逻辑与自动推理 2
1.2当前国内外的研究现状及发展趋势 3
1.3已有的几个流行的符号数学软件系统 4
1.4 本文的解决方案 6
第二章 命题逻辑的定义及原理 7
2.1 命题及范式定义 7
2.2求解命题公式范式的合取范式和析取范式步骤 9
第三章C语言概述及其开发过程 11
3.1 C语言的产生与发展 11
3.2 C语言的特点 11
3.3 C程序的开发过程 12
第四章 命题公式范式生成算法分析 15
4.1 广义表的定义及扩展 15
4.2扩展广义表的存储结构设计 16
4.3利用扩展广义表实现命题逻辑表达式的基本运算 17
4.4命题逻辑基本运算的算法实现举例 19
第五章 命题公式范式生成算法的实现 20
5.1 广义表存储格式的定义以及存储 20
5.2命题逻辑基本运算的函数实现…..22
5.3 范式生成的主函数实现 25
5.4 程序的调试 26
第六章 结束语 28
参考文献 29
致  谢 30

第一章  绪 论

     自动推理是人工智能研究中一个非常活跃而又极其重要的领域，它的发展对专家系统，信息智能检索、智能机器人等人工智能其它领域都有深远的影响。而数理逻辑是现代数学的重要基础，也是计算机科学的重要基础之一。作为数理逻辑的基本知识命题公式范式的生成已成为定理机器证明的重要基础理论。