邏輯公式的可滿足性問題在工程技術(shù)、交通運輸、軍事及自然科學等領(lǐng)域有著廣泛的應用。隨著計算機求解問題容量的逐漸增大、求解的問題愈加復雜,命題邏輯中邏輯公式的冗余越來越多,浪費大量的儲存空間和計算時間。檢測并消除邏輯公式中的冗余可以有效的提高計算機儲存空間利用效率和削減計算時間。本文研究邏輯公式的冗余性質(zhì)及其判定,以期為冗余的消除提供一定的理論基礎。主要的研究工作如下:一、研究冗余子句的性質(zhì),提出冗余子句的判定方法。首先,引用二元子句定義的隱藏文字及其相關(guān)性質(zhì)提出邏輯公式中冗余子句的概念。然后,分別得到子句集中是否存在單元子句的判定方法;基于冗余子句的概念,討論了邏輯公式中子句冗余的問題,推導出冗余子句與其相對應的子句集的可滿足性的等價條件。最后,利用子句集間的等價性,得到了冗余子句的相應判定條件。二、研究了冗余文字的性質(zhì),提出冗余文字的判定方法。首先,根據(jù)二元子句中隱藏文字的添加規(guī)則,提出了子句集中冗余文字的概念,并得到冗余文字與其相對應的子句集的可滿足性之間的關(guān)系。然后,根據(jù)冗余子句的相關(guān)性質(zhì),推導出冗余子句與冗余文字的相互關(guān)系。最后,根據(jù)子句集間的等價性,提出了判定冗余子句和冗余文字... 

【文章來源】：西南交通大學四川省 211工程院校 教育部直屬院校

【文章頁數(shù)】：68 頁

【學位級別】：碩士

【文章目錄】：
摘要
abstract
常用子句集
第1章 緒論
    1.1 研究背景及意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 研究的內(nèi)容及方法
第2章 預備知識
    2.1 命題邏輯中邏輯公式的基本概念
    2.2 命題邏輯中邏輯公式的化簡規(guī)則
    2.3 本章小結(jié)
第3章 命題邏輯中子句集的冗余子句的判定方法
    3.1 子句集的冗余子句
    3.2 子句集中冗余子句的判定
    3.3 本章小結(jié)
第4章 命題邏輯中子句集的冗余文字的判定方法
    4.1 子句集的冗余文字
    4.2 子句集中冗余文字的判定
    4.3 本章小結(jié)
總結(jié)與展望
致謝
參考文獻
附錄 文字冗余性的判定程序
碩士學位期間發(fā)表的論文和研究工作


【參考文獻】：
期刊論文
[1]求解MinSAT問題的加強式格局檢測與子句加權(quán)算法[J]. 周俊萍,任雪亮,殷茜,李睿智,殷明浩.  計算機學報. 2018(04)
[2]移動網(wǎng)絡服務信息傳輸中冗余量消除方法研究[J]. 顧愛華.  計算機仿真. 2016(11)
[3]基于子句文字長度動態(tài)約束的變量消除算法[J]. 鄧曉瑤,馮志勇,饒國政,王鑫.  計算機科學與探索. 2014(11)
[4]命題邏輯公式中的冗余子句及冗余文字[J]. 翟翠紅,秦克云.  計算機科學. 2013(05)
[5]格值邏輯公式中短語和文字的可消性[J]. 徐揚,宋振明.  數(shù)學季刊. 1990(Z1)
[6]布爾邏輯公式中文字和小項的可消性[J]. 徐揚,鄒開其.  西南交通大學學報. 1990(01)

博士論文
[1]基于分治的布爾可滿足性判定[D]. 范全潤.西安電子科技大學 2015

碩士論文
[1]命題邏輯中子句集的分類研究[D]. 鄧鵬.西南交通大學 2015
[2]應用線性代數(shù)求解可滿足性問題的研究與實現(xiàn)[D]. 丁志宇.中山大學 2014
[3]命題邏輯中子句集的冗余性研究[D]. 唐仕輝.西南交通大學 2014



本文編號：3536999