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

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

【文章頁數】：72 頁

【學位級別】：碩士

【文章目錄】：
摘要
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



本文編號：3561467