命题逻辑中子句集的分类研究

发布时间：2020-11-14 02:27

　　定理机器证明是通过计算机实现定理自动证明。自上世纪五十年代以来定理自动证明一直是计算机科学研究的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用。其中检测和删除逻辑公式中的冗余子句是该方向广泛研究的基本问题。基于已有的研究工作,本文围绕命题逻辑中子句和文字的相关知识,取得的主要研究结果如下：1、将命题逻辑的子句集中文字划分为三类,即有用文字、必需文字和无用文字,分别给出了三种文字的定义,同时得到了相应的等价描述方法,进而得到了三种文字之间的相互关系。得到了子句集中的必需文字是非冗余文字,子句集中的无用文字是冗余文字。2、基于子句集中文字的划分,得到了有用文字、必需文字和无用文字的判别方法,借助子句集的可满足性给出了三种文字与子句集的可满足性的等价条件。给出了有用文字、必需文字和无用文字的判定定理并设计相应算法。3、研究了命题逻辑的子句集中冗余子句的性质,得到了命题逻辑的子句集中冗余子句的等价定理,给出了命题逻辑的子句集中的有用子句、必需子句和无用子句的相关性质。根据子句集的可满足性得到了一种判断有用子句、必需子句和无用子句的判别方法,通过实例说明了该方法的有效性。
【学位单位】：西南交通大学
【学位级别】：硕士
【学位年份】：2015
【中图分类】：O141.1
【文章目录】：
摘要
Abstract
第一章绪论
    1.1 研究背景和研究意义
    1.2 国内外研究现状
    1.3 本文的主要工作和章节安排
第二章基础知识
    2.1 命题逻辑中子句和文字的基本概念
    2.2 命题逻辑中子句集的简化方法
    2.3 命题逻辑中的归结方法
    2.4 冗余子句和冗余文字
    2.5 本章小结
第三章命题逻辑的子句集中文字的冗余性研究
    3.1 子句集中文字的分类
    3.2 子句集中文字的冗余性判定
    3.3 文字的冗余性判定算法及程序实现
    3.4 本章小结
第四章命题逻辑的子句集中子句的冗余性研究
    4.1 基本理论
    4.2 子句集中子句的冗余性判定
    4.3 子句的冗余性判定算法
    4.4 本章小结
第五章总结与展望
    5.1 论文总结
    5.2 展望
致谢
参考文献
附录文字冗余性和子句冗余性判定程序
攻读硕士学位期间发表的论文

【相似文献】

相关期刊论文前10条

1 唐金文;解析命题符号化[J];曲靖师范学院学报;2002年06期

2 徐凤生;命题逻辑中的集合表示[J];计算机与现代化;2005年05期

3 李立峰;张东晓;;概念格在二值命题逻辑命题集约简中的应用[J];电子学报;2007年08期

4 张胜礼;;中介命题逻辑一种改进的无穷值语义模型[J];兴义民族师范学院学报;2011年01期

5 陈敬华;胡松林;;关于命题逻辑中两个问题的思考[J];湖北师范学院学报(自然科学版);2011年04期

6 张建成;苏连塔;;命题逻辑系统理论(广义)根性质及应用[J];山东大学学报(工学版);2013年04期

7 张永清;;模糊问句与超命题逻辑[J];辽宁师范大学学报(自然科学版);1992年04期

8 苏岐芳,杨捷飞;0—1多项式与命题逻辑[J];齐齐哈尔师范学院学报(自然科学版);1995年03期

9 王郁昕;;互逆主义逻辑中的逻辑命题[J];北京联合大学学报(自然科学版);2005年04期

10 王敏;;命题逻辑中几种常见的推理证明方法[J];吉林师范大学学报(自然科学版);2007年04期

相关博士学位论文前1条

1 王伟;格值命题逻辑系统LP（X）中基于α-归结原理的自动推理方法的研究[D];西南交通大学;2002年