关于PI证明的若干注记以及逻辑公式的真度理论

论文摘要

归结原理是定理自动证明的重要工具。归结的目的在于用归结原理证明子句集S不可满足。PI证明是谓词逻辑归结证明的一种重要类型,其中P指关于谓词符号（predicate symbol）的一种顺序,I是指某一个特定的解释。但是在目前所见的许多文献中对PI推理的定义还有一些不妥之处,没有确保其中的每一步归结都是PI归结。本文给出了一种新的PI推理的定义,弥补了这一缺陷,并且对PI归结的完备性定理证明所需要的引理给出了两种简化证明。 关于区分命题逻辑中公式可靠程度的思想早在1952年就由Rosser与Turequtte提出,多年来许多学者从不同的角度提出了确定这类公式真确程度的方法。建立了积分语义学之后,王国俊教授在经典的二值命题逻辑中建立了命题的真度理论。随后李骏基于相同思想给出了Lukasiewicz多值命题逻辑与标准序列逻辑系统中公式的真度理论。本文也提出了Godel和Kleene三值命题逻辑系统中命题的一种真度理论。以上各种真度理论都是在命题逻辑中给出的,对于谓词逻辑而言,建立公式的真度理论要复杂得多。本文首次在这方面作了讨论,在二值谓词逻辑中,定义了公式的一种相对真度。然后提出了公式的准真度理论,为二值谓词逻辑中的近似推理理论提供了一种可能的逻辑框架。 文章的主要内容如下: 第一部分:作为预备知识,给出了PI冲撞的定义,Davis与Putnam规则,以及一些相关概念。然后指出了原有PI推理定义的不妥之处,给出了修正后的定义。最后对PI归结的完备性定理证明所需要的引理给出了两种简化证明。 第二部分:基于均匀概率的思想,给出了Godel和Kleene三值命题逻辑系统中公式的真度理论。在G3系统中得出:真度为1等价于公式为重言式,但是真度为0并不等价于公式为矛盾式;在K3系统中虽然没有重言式和矛盾式,但是真度值可以取到0,并且0和1都不是孤立点。最后分别在两个系统中证明了真度的广义MP规则与广义HS规则是成立的。 第三部分:研究二值谓词逻辑中公式的真度。首先提出了一阶语言的一类特殊解释（这类解释的论域都是非空有限的）,然后在每个特殊解释中基于均匀概率的思想定义了二值谓词逻辑中公式的相对真度。紧接着,在相对真度的基础上提出了公式的准真度定义,讨论了逻辑有效公式与真度为1的公式,矛盾式与真度为0的公式之间的关系,按照公式的准真度对全体谓词公式进行了分类。最后给

论文目录

• 前言
• 第一章 关于PI证明的若干注记
• §1.1 预备知识
• §1.2 关于PI证明的若干注记
• 第二章 两个三值命题逻辑系统中命题的真度理论
• §2.1 G（o|¨）del三值命题逻辑中命题的真度理论
• §2.2 Kleene三值命题逻辑中命题的真度理论
• 第三章 二值谓词逻辑中公式的一类准真度理论
• §3.1 预备知识
• §3.2 谓词公式的相对真度
• §3.3 谓词公式的准真度
• 总结
• 参考文献
• 致谢
• 攻读硕士学位期间的研究成果