檢測(cè)和消除命題邏輯公式中的冗余子句,是許多應(yīng)用領(lǐng)域（包括人工智能）廣泛研究的基本問(wèn)題�；谝延械难芯抗ぷ�,本文主要探討命題邏輯公式中的冗余子句及冗余文字。本文的主要研究工作包括：1.將子句集中的子句劃分為三類(lèi)：無(wú)冗余子句、相對(duì)冗余子句和絕對(duì)冗余子句,并分別給出了一些等價(jià)描述方法：S是命題邏輯中子句集,C∈Sred,C在S中是相對(duì)冗余的當(dāng)且僅當(dāng)存在S的一個(gè)無(wú)冗余等價(jià)子集S’,使S’{C}|≠C；C在S中是絕對(duì)冗余的當(dāng)且僅當(dāng)S的無(wú)冗余等價(jià)子集恰為S\{C}的無(wú)冗余等價(jià)子集。2.當(dāng)命題邏輯公式蘊(yùn)涵某一文字時(shí),給出了子句集中某幾類(lèi)子句是冗余子句的一些等價(jià)結(jié)論。若S是命題邏輯中子句集,S|=l,C∈S,l∈C,則C在S中是冗余的當(dāng)且僅當(dāng)C在（S\S（l））U{1}是冗余的。此外,進(jìn)一步得到了子句集中包含冗余文字的一些等價(jià)結(jié)論,以及子句集中子句中的文字是冗余文字的等價(jià)描述,即S={C1,C2,…,Gn,D}是命題邏輯中子句集,D=x∨D1,x是D中關(guān)于S的冗余文字當(dāng)且僅當(dāng)D1S’={D1,x,C1,C2,…,Cn}中的冗余子句。3.從子句集的極小不可滿(mǎn)足子集與可滿(mǎn)足核兩個(gè)方面討論同子句集冗余性的關(guān)... 

【文章來(lái)源】：西南交通大學(xué)四川省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：72 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
Chapter 1 Preface
    1.1 Research Background
    1.2 Current Research Statuses
    1.3 Structure of This Paper
Chapter 2 Preliminaries
    2.1 Definitions
    2.2 Simplification Techniques
Chapter 3 Redundant Clauses
    3.1 Redundancy and Irredundant Equivalent Subsets
    3.2 Relatively Redundancy and Absolute Redundancy
Chapter 4 Redundant Literals
    4.1 Formulae Implying Literals
    4.2 Equivalent Description of Redundant Literals
Chapter 5 Judgment of the Redundancy of Set of Clauses
    5.1 Subformulas in Propositional Logic
        5.1.1 Satisfiable Core
        5.1.2 Minimally Unsatisfiable Subformulas
    5.2 Judgment of the Redundancy of Set of Clauses
Conclusions and Future Works
Acknowledgments
Reference
Appendix: procedures for removing redundant clauses
List of Publications and Research Projects



本文編號(hào)：3561467