题目：012.VC命题公式范式生成算法研究与程序设计

本课题是自动推理在离散数学上应用的实例，利用自动推理的思想来研究命题公式范式的生成算法以及程序设计。定理证明是系统及其特性均以某种数学逻辑公式表示的技术。逻辑由一具有公理和推理规则的形式化系统给出。定理证明实质上是从系统公理中寻找特性证明的过程。证明采用公理或者规则,且可能推演出定义和引理。不同于模型检验，定理证明可以处理无限状态空间问题。定理证明系统可粗略地分为自动和交互的两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功；交互式定理证明系统刚更适合于系统的形式化开发和机械形式化。同样地，定理证明的实施也是需要定理证明器的支持。  现在的定理证明器包括：用户导引自动推演工具，证明检验器和复合证明器。用户导引自动推演工具有ACL2,Eves，LP，Nqthm，Reve和RRL，这些工具由引理或者定义序列导引，每一个定理采用已建立的推演，引理驱动重写和简化启发式来自动证明；证明检验器有Coq，HOL，LEGO，LCF和Nuprl；复合证明器Analytica中将定理证明和符号代数系统Mathematica复合，PVS和Step将决策过程，模型检验和交互证明复合在一体。凡能以离散数学为代表的构造性数学方法描述的问题，当该问题所涉及的论域为有穷，或虽为无穷但存在有穷表示时，这个问题也一定能用计算机来处理。反之，凡能被计算机处理的问题均可以转换为一个数学问题，换言之，所有能被计算机处理的问题均可以用数学方法解决。

本文试图以计算机为工具解决命题公式的范式自动生成问题，其初步结果是作为后面的归结系统的输入。主要论述的是在用目标语言把数理逻辑中的命题描述成符号的数学逻辑公式表示后，在c语言的环境中利用广义表的特点，把这些数学逻辑公式用广义表的结点来存储，然后分别按照求解合取范式和析取范式的步骤，遍历广义表分析命题逻辑公式，根据等价公式和推理公式分别对它们进行等值变换和推理，得到最后所要求的范式公式。