论文部分内容阅读
在逻辑系统中证明定理是学习数理逻辑的重要内容之一,命题逻辑公理系统的定理证明则是其中最基础的部分。但是,只能以公理模式和推理规则为工具的定理证明,对于初学者来说并非易事,其主要表现在不能有效地找到证明的起点。本文的目标并不是建立面向计算机的严格的机械化方法,而是探索面向初学者的实用性技巧和方法:一方面既能使证明的某些中间环节实现部分的机械化,以便于寻找证明的思路;另一方面又能使证明不失直观和简洁的特征,从而增强初学者的可读性,提高初学者的学习效率,优化数理逻辑的教学。研究命题逻辑公理系统定理证明的技巧和方法,还可以为定理机械化证明的理论和方法的创新提供必要的实践准备,从而促进定理机器证明的发展,因此具有重要的理论和现实意义。本文在深入研习前人成果和相关理论的基础上,首先,根据定理证明总是相对于某个具体的公理系统这一事实,从考察共性的角度出发,探索公理模式在定理证明中的特征,尤其着重探索公理模式在定理证明中所起的作用,并由此形成消件法和换位法两个实用的证明技巧。其次,利用消件法和换位法,结合采用几何定理证明中常用的综合法和分析法,研究简单定理的证明技巧和方法,以及证明中应当遵循的原则,并由此形成了要对具体定理作具体分析的思想。最后,以证明简单定理的技巧和方法为基础,运用传统逻辑关于复合命题推理的相关规则和方法,研究复杂定理的证明方法,并由此形成了从传统逻辑的推理构造复杂定理证明的定理分解法。