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