命题逻辑中的冗余子句和冗余文字问题研究

发布时间：2021-12-15 19:18

　　逻辑公式的可满足性问题在工程技术、交通运输、军事及自然科学等领域有着广泛的应用。随着计算机求解问题容量的逐渐增大、求解的问题愈加复杂,命题逻辑中逻辑公式的冗余越来越多,浪费大量的储存空间和计算时间。检测并消除逻辑公式中的冗余可以有效的提高计算机储存空间利用效率和削减计算时间。本文研究逻辑公式的冗余性质及其判定,以期为冗余的消除提供一定的理论基础。主要的研究工作如下:一、研究冗余子句的性质,提出冗余子句的判定方法。首先,引用二元子句定义的隐藏文字及其相关性质提出逻辑公式中冗余子句的概念。然后,分别得到子句集中是否存在单元子句的判定方法;基于冗余子句的概念,讨论了逻辑公式中子句冗余的问题,推导出冗余子句与其相对应的子句集的可满足性的等价条件。最后,利用子句集间的等价性,得到了冗余子句的相应判定条件。二、研究了冗余文字的性质,提出冗余文字的判定方法。首先,根据二元子句中隐藏文字的添加规则,提出了子句集中冗余文字的概念,并得到冗余文字与其相对应的子句集的可满足性之间的关系。然后,根据冗余子句的相关性质,推导出冗余子句与冗余文字的相互关系。最后,根据子句集间的等价性,提出了判定冗余子句和冗余文字... 

【文章来源】：西南交通大学四川省 211工程院校 教育部直属院校

【文章页数】：68 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
常用子句集
第1章 绪论
    1.1 研究背景及意义
    1.2 国内外研究现状
    1.3 研究的内容及方法
第2章 预备知识
    2.1 命题逻辑中逻辑公式的基本概念
    2.2 命题逻辑中逻辑公式的化简规则
    2.3 本章小结
第3章 命题逻辑中子句集的冗余子句的判定方法
    3.1 子句集的冗余子句
    3.2 子句集中冗余子句的判定
    3.3 本章小结
第4章 命题逻辑中子句集的冗余文字的判定方法
    4.1 子句集的冗余文字
    4.2 子句集中冗余文字的判定
    4.3 本章小结
总结与展望
致谢
参考文献
附录 文字冗余性的判定程序
硕士学位期间发表的论文和研究工作


【参考文献】：
期刊论文
[1]求解MinSAT问题的加强式格局检测与子句加权算法[J]. 周俊萍,任雪亮,殷茜,李睿智,殷明浩.  计算机学报. 2018(04)
[2]移动网络服务信息传输中冗余量消除方法研究[J]. 顾爱华.  计算机仿真. 2016(11)
[3]基于子句文字长度动态约束的变量消除算法[J]. 邓晓瑶,冯志勇,饶国政,王鑫.  计算机科学与探索. 2014(11)
[4]命题逻辑公式中的冗余子句及冗余文字[J]. 翟翠红,秦克云.  计算机科学. 2013(05)
[5]格值逻辑公式中短语和文字的可消性[J]. 徐扬,宋振明.  数学季刊. 1990(Z1)
[6]布尔逻辑公式中文字和小项的可消性[J]. 徐扬,邹开其.  西南交通大学学报. 1990(01)

博士论文
[1]基于分治的布尔可满足性判定[D]. 范全润.西安电子科技大学 2015

硕士论文
[1]命题逻辑中子句集的分类研究[D]. 邓鹏.西南交通大学 2015
[2]应用线性代数求解可满足性问题的研究与实现[D]. 丁志宇.中山大学 2014
[3]命题逻辑中子句集的冗余性研究[D]. 唐仕辉.西南交通大学 2014



本文编号：3536999