定理機器證明是通過計算機實現(xiàn)定理自動證明。自上世紀五十年代以來定理自動證明一直是計算機科學研究的熱點之一,在數(shù)學、硬件測試與驗證、軟件生成與驗證、協(xié)議驗證、人工智能方面都得到了成功的應用。其中檢測和刪除邏輯公式中的冗余子句是該方向廣泛研究的基本問題。基于已有的研究工作,本文圍繞命題邏輯中子句和文字的相關知識,取得的主要研究結果如下：1、將命題邏輯的子句集中文字劃分為三類,即有用文字、必需文字和無用文字,分別給出了三種文字的定義,同時得到了相應的等價描述方法,進而得到了三種文字之間的相互關系。得到了子句集中的必需文字是非冗余文字,子句集中的無用文字是冗余文字。2、基于子句集中文字的劃分,得到了有用文字、必需文字和無用文字的判別方法,借助子句集的可滿足性給出了三種文字與子句集的可滿足性的等價條件。給出了有用文字、必需文字和無用文字的判定定理并設計相應算法。3、研究了命題邏輯的子句集中冗余子句的性質,得到了命題邏輯的子句集中冗余子句的等價定理,給出了命題邏輯的子句集中的有用子句、必需子句和無用子句的相關性質。根據(jù)子句集的可滿足性得到了一種判斷有用子句、必需子句和無用子句的判別方法,通過實例說明了該方法的有效性。
【學位單位】：西南交通大學
【學位級別】：碩士
【學位年份】：2015
【中圖分類】：O141.1
【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景和研究意義
    1.2 國內外研究現(xiàn)狀
    1.3 本文的主要工作和章節(jié)安排
第二章 基礎知識
    2.1 命題邏輯中子句和文字的基本概念
    2.2 命題邏輯中子句集的簡化方法
    2.3 命題邏輯中的歸結方法
    2.4 冗余子句和冗余文字
    2.5 本章小結
第三章 命題邏輯的子句集中文字的冗余性研究
    3.1 子句集中文字的分類
    3.2 子句集中文字的冗余性判定
    3.3 文字的冗余性判定算法及程序實現(xiàn)
    3.4 本章小結
第四章 命題邏輯的子句集中子句的冗余性研究
    4.1 基本理論
    4.2 子句集中子句的冗余性判定
    4.3 子句的冗余性判定算法
    4.4 本章小結
第五章 總結與展望
    5.1 論文總結
    5.2 展望
致謝
參考文獻
附錄 文字冗余性和子句冗余性判定程序
攻讀碩士學位期間發(fā)表的論文

【相似文獻】

相關期刊論文 前10條

1 唐金文;解析命題符號化[J];曲靖師范學院學報;2002年06期

2 徐鳳生;命題邏輯中的集合表示[J];計算機與現(xiàn)代化;2005年05期

3 李立峰;張東曉;;概念格在二值命題邏輯命題集約簡中的應用[J];電子學報;2007年08期

4 張勝禮;;中介命題邏輯一種改進的無窮值語義模型[J];興義民族師范學院學報;2011年01期

5 陳敬華;胡松林;;關于命題邏輯中兩個問題的思考[J];湖北師范學院學報(自然科學版);2011年04期

6 張建成;蘇連塔;;命題邏輯系統(tǒng)理論(廣義)根性質及應用[J];山東大學學報(工學版);2013年04期

7 張永清;;模糊問句與超命題邏輯[J];遼寧師范大學學報(自然科學版);1992年04期

8 蘇岐芳,楊捷飛;0—1多項式與命題邏輯[J];齊齊哈爾師范學院學報(自然科學版);1995年03期

9 王郁昕;;互逆主義邏輯中的邏輯命題[J];北京聯(lián)合大學學報(自然科學版);2005年04期

10 王敏;;命題邏輯中幾種常見的推理證明方法[J];吉林師范大學學報(自然科學版);2007年04期

相關博士學位論文 前1條

1 王偉;格值命題邏輯系統(tǒng)LP（X）中基于α-歸結原理的自動推理方法的研究[D];西南交通大學;2002年

本文編號：2882955