命题逻辑推理的代数化证明-计算机工程与科学.PDF

CN43-1258／TP 计算机工程与科学 2008年第 3O卷第 1O期 ISSN 1007—130X COMPUTER ENGINEERING SCIENCE V01．30，No．10，2008 文章编号：1007—130X(2OO8)100078—04 命题逻辑推理的代数化证明 TheAlgebraicProofofPropositionDeduction 王礼萍 ，张树功 WANG Li-ping~，ZItANG Shu-gongz (1．哈尔滨学院数学与计算机学院，黑龙江 哈尔滨 150086；2．吉林大学数学学院，吉林 长春 130012) (1．SchoolofMathematicsandComputerScience，HarbinUniversity，Hrabin150086； 2．SchoolofMathematics。JilinUniversity，Changchun130012，China) 摘 要：本文尝试利用纯代数的方式，通过解多项式方程组对命题逻辑进行演算、推理。 Abstract：Inthisthesis，WOtrytOuseasimplealgebraicwaytOperform logicoperationsanddeductionsthroughsolving thepolynomia1equations． 关键词：真值函数；赋值；多项式；命题公式 Keywords：truthfunction；assignment；polynomial；proposition 中图分类号：TP301 文献标识码：A 公式 (永真式)为基础，称为公理 (Axioms)；以若干可对公 1 引言 式进行重写的规则 (确保 由永真式重写出永真式)作为系统 内公式变换的依据 ，称为推理规则 (RulesofReference)。 逻辑学 (1ogic)是研究人类推理过程的科学 ，数理逻辑 系统内推演的全部依据是符号的形式，而不是别的任何东 (MathematicalLogic)则是用数学的方法来进行这一研究 西，并且系统能导出且只能导出反映人们思维正确规律的 的一个数学学科。它的显著特征是符号化和形式化，即把 永真式，进而成为人类进行逻辑推理的一个框架 ，它保证在 逻辑学所涉及的 “概念、判断、推理”用符号来表示，用公理 前提正确的条件下总能得出正确的推理结果。这就是所谓 体系 (形式系统)来刻画，并基于符号形式的演算来描述推 数理逻辑的形式系统_1]。本文主要将逻辑证明问题转化成 理过程的一般规律[】]。早在 17世纪，莱布尼兹 (Leibniz)已 多项式方程组的求解 问题，通过对方程组的求解实现逻辑 经提出用代数的方法研究逻辑学的想法，但由于社会条件 推理。首先，利用多项式方程组表示命题推理中的前提，再 等原因，当时这一思想并未得到应有的重视。直到 l9世纪 利用代数方法解多项式方程组，最后将得到的结果转化成 的中后期，布尔(Boole)和弗雷格 (Frege)的天才工作 “布尔 前提的演绎结果，从而实现用代数方法演绎逻辑推理，进行 代数”、“概念演算”，才真正翻开逻辑代数的辉煌篇章。 逻辑证明和推理。 1930年 Godel完全性定理的证明使逻辑代数的基础得 以 完善，最终完成了数理逻辑形式系统的研究工作。数理逻 2 命题公式和真值函数 辑与随后的计算理论的出现，为现代数字计算机的诞生奠 定了重要的基础_1]。其中，命题逻辑部分的基础演算被叫 定义 1 命题公式： 做逻辑代数，