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

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 唐金文;解析命題符號化[J];曲靖師范學(xué)院學(xué)報(bào);2002年06期

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

3 李立峰;張東曉;;概念格在二值命題邏輯命題集約簡中的應(yīng)用[J];電子學(xué)報(bào);2007年08期

4 張勝禮;;中介命題邏輯一種改進(jìn)的無窮值語義模型[J];興義民族師范學(xué)院學(xué)報(bào);2011年01期

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

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

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

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

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

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

相關(guān)博士學(xué)位論文 前1條

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

本文編號：2882955