命题公式真值表生成算法研究与程序设计
摘要
推理的自动化（包括自动定理证明）特别诱人，因为所有数学以及许多技术领域均可用一定的形式系统来表述。今天用现代计算机进行快速而准确的推理已经成为可能。自动推理可以避免令人乏味和容易出错的详细证明构造过程。命题公式真值生成算法研究就是研究推理的自动化的基础。掌握好了它，就等于是在推理自动化的旅程上建立了一个好的开始。
本文以命题公式真值表生成为目标。从基本真值矩阵开始入手，研究其生成的算法和程序设计。而后，借助基本真值矩阵，得到真值表生成算法。论文中主要介绍了本课题的开发背景，程序所要完成的功能和程序设计中的主要算法。程序用C语言实现，能将用户输入的命题公式的真值表，以特定的表示形式输出。
【关键字】:自动定理证明，命题公式真值生成，基本真值矩阵
Proposition formula truth table production algorithm research and programming
ABSTRACT
The inference automation (including automatic theorem proving) is specially attractive, because all mathematics as well as many areas of technology may use the certain formal system to indicate. Today carried on fast but the accurate inference with the modern computer already to become possibly. The automatic inference may avoid the detailed proving structure process which tasteless and is easy to make a mistake. The proposition formula true value production algorithm research is studies the inference the automation foundation. Grasped it, and so on thereupon has established a good start in the inference automation journey.
This article becomes the goal by the proposition formula truth table. Starts from the basic true value matrix to obtain, studies its production the algorithm and the programming. But after, with the aid of the basic true value matrix, obtains the truth table production algorithm. In the paper mainly introduced this topic development background, the procedure must complete in function and programming main algorithm. The procedure realizes with the C language, can the user input proposition formula truth table, by the specific expression form output.
【Keywords】: Automatic theorem prooving，the proposition formula truth table，the basic true value matrix
目录
摘要 2
ABSTRACT 2
目录 3
第一章 概述 4
1.1引言 4
1.2算法设计意义 5
1.3毕业设计目的 5
1.4本次毕业设计所要完成的主要工作 5
1.5本章小结 5
第二章 数理逻辑的相关知识 6
2.1联结词种类和含义 6
2.2联结词在计算机中的表示方法 7
2.3本章小结 7
第三章 基本真值矩阵的计算机表示 8
3.1基本真值矩阵的引入 8
3.2基本真值矩阵生成算法 9
3.3本章小结 11
第四章 命题公式真值表的生成算法 12
4.1真值表的表示 12
4.2命题公式真值表的生成算法 12
4.3本章小结 15
第五章 核心算法部分原代码 16
5.1调用基本真值矩阵子函数的代码 16
5.2基本真值矩阵生成的代码 17
第六章 系统运行中不同的命题公式的即时输入 18
第七章 综合系统的构想 19
第八章 总结与展望 20
致谢 21
参考文献 21
第一章 概述
1.1引言
1956年夏天， 美国达特莫斯大学（Dartmouth）召开了一次影响深远的历史性会议。学者们在充分讨论的基础上，首次提出了“人工智能” （Artificial Intelligence）这一术语，标志着人工智能（AI）作为一门新兴学科正式诞生。1956年AI研究另外一个重大的突破，是纽厄尔、赫伯特•西蒙等人合作编制的《逻辑理论机》数学定理证明程序（简称LT），从而使机器迈出了逻辑推理的第一步。
在卡内基—梅隆大学的计算机实验室，纽厄尔和西蒙从分析人类解答数学题的技巧入手，让一些人对各种数学题作周密的思考，要求他们不仅写出求解的答案，而且说出自己推理的方法和步骤。通过大量的观察实例，纽厄尔和赫伯特•西蒙广泛收集了人类求解一般性问题的各种方案。他们发现，人们求解数学题通常是用试凑的办法进行的，试凑时不一定列出了所有的可能性，而是用逻辑推理来迅速缩小搜索范围。
