第10卷第5期 智能系统学报 Vol.10 No.5 2015年10月 CAAI Transactions on Intelligent Systems 0ct.2015 D0I:10.11992/is.201410005 网s络出版t地址：htp:/ww.cmki.net/kcms/detail/23.1538.tp.20151008.1000.006.html 命题逻辑的子句集中文字的分类 邓鹏12，徐扬2 (1.西南交通大学数学学院，四川成都611756：2.西南交通大学智能控制开发中心，四川成都610031) 摘要：检测和消除命题逻辑公式中的冗余文字，是人工智能领域广泛研究的基本问题。针对命题逻辑的子句集中 子句的划分，结合冗余子句和冗余文字的概念，将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字3 类，并分别给出其定义。讨论3种文字与无冗余等价子集的性质，给出其等价子集的等价描述方法。得到题逻辑的 子句集中必需文字，有用文字和无用文字的判定方法，借助子句集的可满足性得到3种文字与子句集的可满足性的 等价条件。上述结果对命题逻辑中文字属性的判断提供了多种可选择方法，同时为命题逻辑公式的化简奠定了理 论基础。 关键词：命题逻辑：子句集：冗余子句：冗余文字；可满足性 中图分类号：TH186文献标志码：A文章编号：1673-4785(2015)05-0736-05 中文引用格式：邓鹏，徐扬.命题逻辑的子句集中文字的分类[J].智能系统学报，2015,10(5)：736-740. 英文引用格式：DENG Peng,XU Yang.Classification of the characters in the set of clauses of propositional logic[J].CAAI Transac- tions on Intelligent Systems,2015,10(5):736-740. Classification of the characters in the set of clauses of propositional logic DENG Peng'2,XU Yang'.2 (1.School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China;2.Intelligent Control Development Center,South- west Jiaotong University,Chengdu 610031,China) Abstract:The detection and elimination of redundant clauses from prepositional logic formulas is a fundamental is- sue that has been widely researched in artificial intelligence(AI).The concept for division in the set of clauses of propositional logic is combined with the concepts of redundant clause and redundant character so as to research the classification of the characters in the set of clauses of propositional logic.The characters are classified into three cat- egories:necessary characters,useful characters,and useless characters,and thereby definitions of them are given, respectively.The property of three kinds of characters and irredundant equivalent subsets is discussed,some equiv- alent descriptions of these three kinds of characters and non-redundant equivalent subsets are given respectively. The judging method for these three kinds of characters in the set of clauses of propositional logic is obtained,and by virtue of the satisfiability of the set of clauses,the equivalent conditions of satisfiability for these three kinds of characters and the set of clauses are derived.These results provide a variety of alternative methods for judging the attributes of the characters of the set of clauses in propositional logic,laying a theoretical foundation for simplifying propositional logic formulas. Keywords:propositional logic;set of clauses;redundant clause;redundant character;satisfiability 在人工智能领域，知识表示的方式多种多样，子示广泛应用于机器定理证明、专家系统和知识库等 句形式仍不失为一种重要的知识表达方式。子句表 领域。在一个知识库中，如果有部分知识可以删除 并且不减少整个知识库携带的信息，那么称这个知 收稿日期：2014-10-08.网络出版日期：2015-10-08 识库是冗余的。冗余以及与其密切相关的化简已经 基金项目：国家自然科学基金资助项目(61175055,61305074)：四川 省科技支撑计划资助项目(2011FZ0051). 成为具有重要现实意义的问题。命题逻辑中子句由 通信作者：邓鹏.E-mail:dengpengswjtu@163.com
第 １０ 卷第 ５ 期 智 能 系 统 学 报 Ｖｏｌ．１０ №．５ ２０１５ 年 １０ 月 ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ Ｏｃｔ． ２０１５ ＤＯＩ：１０．１１９９２ ／ ｔｉｓ．２０１４１０００５ 网络出版地址：ｈｔｔｐ： ／ ／ ｗｗｗ．ｃｎｋｉ．ｎｅｔ ／ ｋｃｍｓ／ ｄｅｔａｉｌ ／ ２３．１５３８．ｔｐ．２０１５１００８．１０００．００６．ｈｔｍｌ 命题逻辑的子句集中文字的分类 邓鹏１，２ ，徐扬１，２ （１． 西南交通大学 数学学院，四川 成都 ６１１７５６； ２． 西南交通大学 智能控制开发中心，四川 成都 ６１００３１） 摘 要：检测和消除命题逻辑公式中的冗余文字，是人工智能领域广泛研究的基本问题。 针对命题逻辑的子句集中 子句的划分，结合冗余子句和冗余文字的概念，将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字 ３ 类，并分别给出其定义。 讨论 ３ 种文字与无冗余等价子集的性质，给出其等价子集的等价描述方法。 得到题逻辑的 子句集中必需文字、有用文字和无用文字的判定方法，借助子句集的可满足性得到 ３ 种文字与子句集的可满足性的 等价条件。 上述结果对命题逻辑中文字属性的判断提供了多种可选择方法，同时为命题逻辑公式的化简奠定了理 论基础。 关键词：命题逻辑；子句集；冗余子句；冗余文字；可满足性 中图分类号：ＴＨ１８６ 文献标志码：Ａ 文章编号：１６７３⁃４７８５（２０１５）０５⁃０７３６⁃０５ 中文引用格式：邓鹏，徐扬． 命题逻辑的子句集中文字的分类［Ｊ］． 智能系统学报， ２０１５，１０（５）： ７３６⁃７４０． 英文引用格式：ＤＥＮＧ Ｐｅｎｇ， ＸＵ Ｙａｎｇ． Ｃｌａｓｓｉｆｉｃａｔｉｏｎ ｏｆ ｔｈｅ ｃｈａｒａｃｔｅｒｓ ｉｎ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ［Ｊ］． ＣＡＡＩ Ｔｒａｎｓａｃ⁃ ｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ， ２０１５， １０（５）： ７３６⁃７４０． Ｃｌａｓｓｉｆｉｃａｔｉｏｎ ｏｆ ｔｈｅ ｃｈａｒａｃｔｅｒｓ ｉｎ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ＤＥＮＧ Ｐｅｎｇ １，２ ， ＸＵ Ｙａｎｇ １，２ （１． Ｓｃｈｏｏｌ ｏｆ Ｍａｔｈｅｍａｔｉｃｓ， Ｓｏｕｔｈｗｅｓｔ Ｊｉａｏｔｏｎｇ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈｅｎｇｄｕ ６１１７５６， Ｃｈｉｎａ； ２． Ｉｎｔｅｌｌｉｇｅｎｔ Ｃｏｎｔｒｏｌ Ｄｅｖｅｌｏｐｍｅｎｔ Ｃｅｎｔｅｒ， Ｓｏｕｔｈ⁃ ｗｅｓｔ Ｊｉａｏｔｏｎｇ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈｅｎｇｄｕ ６１００３１， Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ：Ｔｈｅ ｄｅｔｅｃｔｉｏｎ ａｎｄ ｅｌｉｍｉｎａｔｉｏｎ ｏｆ ｒｅｄｕｎｄａｎｔ ｃｌａｕｓｅｓ ｆｒｏｍ ｐｒｅｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ｆｏｒｍｕｌａｓ ｉｓ ａ ｆｕｎｄａｍｅｎｔａｌ ｉｓ⁃ ｓｕｅ ｔｈａｔ ｈａｓ ｂｅｅｎ ｗｉｄｅｌｙ ｒｅｓｅａｒｃｈｅｄ ｉｎ ａｒｔｉｆｉｃｉａｌ ｉｎｔｅｌｌｉｇｅｎｃｅ （ＡＩ）． Ｔｈｅ ｃｏｎｃｅｐｔ ｆｏｒ ｄｉｖｉｓｉｏｎ ｉｎ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ｉｓ ｃｏｍｂｉｎｅｄ ｗｉｔｈ ｔｈｅ ｃｏｎｃｅｐｔｓ ｏｆ ｒｅｄｕｎｄａｎｔ ｃｌａｕｓｅ ａｎｄ ｒｅｄｕｎｄａｎｔ ｃｈａｒａｃｔｅｒ ｓｏ ａｓ ｔｏ ｒｅｓｅａｒｃｈ ｔｈｅ ｃｌａｓｓｉｆｉｃａｔｉｏｎ ｏｆ ｔｈｅ ｃｈａｒａｃｔｅｒｓ ｉｎ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ． Ｔｈｅ ｃｈａｒａｃｔｅｒｓ ａｒｅ ｃｌａｓｓｉｆｉｅｄ ｉｎｔｏ ｔｈｒｅｅ ｃａｔ⁃ ｅｇｏｒｉｅｓ： ｎｅｃｅｓｓａｒｙ ｃｈａｒａｃｔｅｒｓ， ｕｓｅｆｕｌ ｃｈａｒａｃｔｅｒｓ， ａｎｄ ｕｓｅｌｅｓｓ ｃｈａｒａｃｔｅｒｓ， ａｎｄ ｔｈｅｒｅｂｙ ｄｅｆｉｎｉｔｉｏｎｓ ｏｆ ｔｈｅｍ ａｒｅ ｇｉｖｅｎ， ｒｅｓｐｅｃｔｉｖｅｌｙ． Ｔｈｅ ｐｒｏｐｅｒｔｙ ｏｆ ｔｈｒｅｅ ｋｉｎｄｓ ｏｆ ｃｈａｒａｃｔｅｒｓ ａｎｄ ｉｒｒｅｄｕｎｄａｎｔ ｅｑｕｉｖａｌｅｎｔ ｓｕｂｓｅｔｓ ｉｓ ｄｉｓｃｕｓｓｅｄ， ｓｏｍｅ ｅｑｕｉｖ⁃ ａｌｅｎｔ ｄｅｓｃｒｉｐｔｉｏｎｓ ｏｆ ｔｈｅｓｅ ｔｈｒｅｅ ｋｉｎｄｓ ｏｆ ｃｈａｒａｃｔｅｒｓ ａｎｄ ｎｏｎ⁃ｒｅｄｕｎｄａｎｔ ｅｑｕｉｖａｌｅｎｔ ｓｕｂｓｅｔｓ ａｒｅ ｇｉｖｅｎ ｒｅｓｐｅｃｔｉｖｅｌｙ． Ｔｈｅ ｊｕｄｇｉｎｇ ｍｅｔｈｏｄ ｆｏｒ ｔｈｅｓｅ ｔｈｒｅｅ ｋｉｎｄｓ ｏｆ ｃｈａｒａｃｔｅｒｓ ｉｎ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ｉｓ ｏｂｔａｉｎｅｄ， ａｎｄ ｂｙ ｖｉｒｔｕｅ ｏｆ ｔｈｅ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｏｆ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ， ｔｈｅ ｅｑｕｉｖａｌｅｎｔ ｃｏｎｄｉｔｉｏｎｓ ｏｆ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｆｏｒ ｔｈｅｓｅ ｔｈｒｅｅ ｋｉｎｄｓ ｏｆ ｃｈａｒａｃｔｅｒｓ ａｎｄ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ａｒｅ ｄｅｒｉｖｅｄ． Ｔｈｅｓｅ ｒｅｓｕｌｔｓ ｐｒｏｖｉｄｅ ａ ｖａｒｉｅｔｙ ｏｆ ａｌｔｅｒｎａｔｉｖｅ ｍｅｔｈｏｄｓ ｆｏｒ ｊｕｄｇｉｎｇ ｔｈｅ ａｔｔｒｉｂｕｔｅｓ ｏｆ ｔｈｅ ｃｈａｒａｃｔｅｒｓ ｏｆ ｔｈｅ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｉｎ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ， ｌａｙｉｎｇ ａ ｔｈｅｏｒｅｔｉｃａｌ ｆｏｕｎｄａｔｉｏｎ ｆｏｒ ｓｉｍｐｌｉｆｙｉｎｇ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ｆｏｒｍｕｌａｓ． Ｋｅｙｗｏｒｄｓ：ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ； ｓｅｔ ｏｆ ｃｌａｕｓｅｓ； ｒｅｄｕｎｄａｎｔ ｃｌａｕｓｅ； ｒｅｄｕｎｄａｎｔ ｃｈａｒａｃｔｅｒ； ｓａｔｉｓｆｉａｂｉｌｉｔｙ 收稿日期：２０１４⁃１０⁃０８． 网络出版日期：２０１５⁃１０⁃０８． 基金项目：国家自然科学基金资助项目（６１１７５０５５， ６１３０５０７４）； 四川 省科技支撑计划资助项目（２０１１ＦＺ００５１）． 通信作者：邓鹏． Ｅ⁃ｍａｉｌ：ｄｅｎｇｐｅｎｇｓｗｊｔｕ＠ １６３．ｃｏｍ． 在人工智能领域，知识表示的方式多种多样，子 句形式仍不失为一种重要的知识表达方式。 子句表 示广泛应用于机器定理证明、专家系统和知识库等 领域。 在一个知识库中，如果有部分知识可以删除 并且不减少整个知识库携带的信息，那么称这个知 识库是冗余的。 冗余以及与其密切相关的化简已经 成为具有重要现实意义的问题。 命题逻辑中子句由
第5期 邓鹏，等：命题逻辑的子句集中文字的分类 ·737. 文字的析取组成，因此能够对其中的文字进行科学 3)称C在S中是无用的(useless),如果对于S 合理的分类对研究冗余文字和冗余子句很有必要， 的任一无冗余等价子集S',有C主S'。 这些理论为归结自动推理奠定了基础。 定理1)设S是子句集，C∈S,C在S中是必 逻辑公式的化简是计算机科学和人工智能领域 需的当且仅当S-{C≠C。 重要的研究方向。逻辑上的冗余问题已被许多学者 定理2】设S是子句集，C∈S。C在S中是 广泛研究4)，包括不同计算问题的复杂性的刻画。 有用的当且仅当存在S的一个无冗余等价子集$”， 其中，主要包括冗余性在实际可满足性求解中的重 使S-{C}≠C。 要作用的研究[s)。P.Liberatore!)对命题逻辑中的 定理3)设S是子句集，C∈S。C在S中是 子句集进行了分类，给出了冗余子句的一些等价条 无用的当且仅当S的无冗余等价子集恰为S-{C} 件和性质。翟翠红等]研究了命题逻辑中的冗余 的无冗余等价子集。 子句和冗余文字，讨论了子句集的无冗余等价子集。 定理4)设S={C1,C2,…,Cn,D}是命题逻 唐世辉]研究了命题逻辑中子句集的冗余性，将命 辑中子句集，且D中不含互补文字。D是S中冗余 题逻辑中子句分为绝对冗余、相对冗余和无冗余3 子句当且仅当子句集S={C,C2,…,Cm}U{D}不 类。因此，本文主要深入研究命题逻辑的子句集中 可满足。 文字的特征，将命题逻辑的子句集中的文字划分为 定义5]设S={C1,C2,…,Cm,D}是命题逻 有用文字、必需文字和无用文字，讨论3种文字的关 辑中子句集，D=xVD,其中x是一文字，D1是一子 系。最后得到有用文字、必需文字和无用文字的判 句，如果DAC,AC2∧…ACm=D1AC1 定方法，为命题逻辑公式的化简提供理论支撑。 C2∧…八Cm,则称x是D中关于S的冗余文字。 1预备知识 定理5I12)设S={C1,C2,…,Cm,D}是命题逻 辑中的子句集，D=xVD,如果D1是S={C1,C2, 在命题逻辑公式中，称原子公式及其否定叫做 …,Cm,D}中的冗余子句，则x是D中关于S的冗 文字，有限多个文字的析取叫子句，只含有一个文字 余文字 的子句称为单子句。 定义1设A(P1,P2,…P)eF(S),则当A 定理6设S={C1,C2,…,C.,D}是命题逻 辑中子句集，D=xVD,x是D中关于S的冗余文字 具有形式(Q,VQ2V…VQ)A…∧(QVoV 当且仅当D1是子句集S={D1,x,C,C2,…,Cm}中 …VQn)时，称A为合取范式(conjunction normal 的冗余子句。 form,CNF),这里Q,=p或Q,=P(ji=1,2,…,n; 定理7]设S={C,C2,…,Cn,D}是命题逻 i=1,2,…,m)。 辑中子句集，且D中不含互补文字。D是S中冗余 定义21s1设S={C1,C2,…,C.,D}是命题逻 子句当且仅当子句集S={C,-D,C2-D,…,CmD} 辑中的子句集。显然，D是S中的冗余子句，当且仅 不可满足。 当C,AC2A…∧CmAD=C,AC2A…ACm。 对于子句集S,令Sl,={C1C∈S且{x,x}∩ 一个子句是冗余的，暗示此子句可以从子句集 C=☑}U{C\{x}IC∈S且x∈C},SIx= 中删除，不会影响子句集所要表示的信息。同理，一 （((S1x）13)…1x,),其中4={x1,x2,…,x}。 个子句集是冗余的，可以定义为它和它的一个真子 定理81)设S={C1,C2,…,Cm,D}是命题逻 集等价。 定义3川子句集S是冗余的，当且仅当存在 辑中子句集，子句集S={C1,C2,…,Cm}U{D}不 S'CS,使S'=S。 可满足当且仅当子句集(S1{D})方不可满足。 在命题逻辑中，此定义和如下说法是等价的： 2子句集中文字的分类 1)存在SCS,使S=S: 2)S中含有冗余子句。 定义6设S={C1,C2,…,Cm}是命题逻辑中 定义4)设S是子句集，C∈S 的子句集，如果对于S中的任一子句C:,若有C:= 1)称C在S中是必需的(necessary),如果对于 xVD(ie{1,2,…,m}),其中x是一文字，D是一 S的任一无冗余等价子集S',有C∈S'; 子句，且x不是C:中关于S的冗余文字，则称x是S 2)称C在S中是有用的(useful),如果存在S 中的必需文字。 的一个无冗余等价子集S',使C∈S': 定义7设S={C1,C2,…,C}是命题逻辑中
文字的析取组成，因此能够对其中的文字进行科学 合理的分类对研究冗余文字和冗余子句很有必要， 这些理论为归结自动推理奠定了基础。 逻辑公式的化简是计算机科学和人工智能领域 重要的研究方向。 逻辑上的冗余问题已被许多学者 广泛研究［１⁃４］ ，包括不同计算问题的复杂性的刻画。 其中，主要包括冗余性在实际可满足性求解中的重 要作用的研究［５⁃１１］ 。 Ｐ．Ｌｉｂｅｒａｔｏｒｅ ［１］ 对命题逻辑中的 子句集进行了分类，给出了冗余子句的一些等价条 件和性质。 翟翠红等［１２］ 研究了命题逻辑中的冗余 子句和冗余文字，讨论了子句集的无冗余等价子集。 唐世辉［１３］研究了命题逻辑中子句集的冗余性，将命 题逻辑中子句分为绝对冗余、相对冗余和无冗余 ３ 类。 因此，本文主要深入研究命题逻辑的子句集中 文字的特征，将命题逻辑的子句集中的文字划分为 有用文字、必需文字和无用文字，讨论 ３ 种文字的关 系。 最后得到有用文字、必需文字和无用文字的判 定方法，为命题逻辑公式的化简提供理论支撑。 １ 预备知识 在命题逻辑公式中，称原子公式及其否定叫做 文字，有限多个文字的析取叫子句，只含有一个文字 的子句称为单子句。 定义 １ ［１４］ 设 Ａ（ｐ１ ，ｐ２ ，…，ｐｍ ）∈Ｆ（Ｓ），则当 Ａ 具有形式（Ｑ１１∨Ｑ１２∨…∨Ｑ１ｎ ）∧…∧（Ｑｍ１∨Ｑｍ２∨ …∨Ｑｍｎ ） 时，称 Ａ 为合取范式（ ｃｏｎｊｕｎｃｔｉｏｎ ｎｏｒｍａｌ ｆｏｒｍ， ＣＮＦ），这里Ｑｉｊ ＝ ｐｊ 或Ｑｉｊ ＝ ¬ ｐｊ（ ｊ ＝ １，２，…，ｎ； ｉ ＝ １，２，…，ｍ）。 定义 ２ ［１５］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中的子句集。 显然，Ｄ 是 Ｓ 中的冗余子句，当且仅 当Ｃ１∧Ｃ２∧…∧Ｃｍ∧Ｄ≡Ｃ１∧Ｃ２∧…∧Ｃｍ 。 一个子句是冗余的，暗示此子句可以从子句集 中删除，不会影响子句集所要表示的信息。 同理，一 个子句集是冗余的，可以定义为它和它的一个真子 集等价。 定义 ３ ［１］ 子句集 Ｓ 是冗余的，当且仅当存在 Ｓ′⊂Ｓ，使 Ｓ′＝ Ｓ。 在命题逻辑中，此定义和如下说法是等价的： １）存在 Ｓ′⊂Ｓ，使 Ｓ′⊨Ｓ； ２）Ｓ 中含有冗余子句。 定义 ４ ［１］ 设 Ｓ 是子句集，Ｃ∈Ｓ， １） 称 Ｃ 在 Ｓ 中是必需的（ｎｅｃｅｓｓａｒｙ），如果对于 Ｓ 的任一无冗余等价子集 Ｓ′，有 Ｃ∈Ｓ′； ２）称 Ｃ 在 Ｓ 中是有用的（ ｕｓｅｆｕｌ），如果存在 Ｓ 的一个无冗余等价子集 Ｓ′，使 Ｃ∈Ｓ′； ３）称 Ｃ 在 Ｓ 中是无用的（ｕｓｅｌｅｓｓ），如果对于 Ｓ 的任一无冗余等价子集 Ｓ′，有 Ｃ∉Ｓ′。 定理 １ ［１］ 设 Ｓ 是子句集，Ｃ∈Ｓ，Ｃ 在 Ｓ 中是必 需的当且仅当 Ｓ－｛Ｃ｝⊨／ Ｃ。 定理 ２ ［１２］ 设 Ｓ 是子句集，Ｃ∈Ｓ。 Ｃ 在 Ｓ 中是 有用的当且仅当存在 Ｓ 的一个无冗余等价子集 Ｓ′， 使 Ｓ′－｛Ｃ｝⊨／ Ｃ。 定理 ３ ［１２］ 设 Ｓ 是子句集，Ｃ∈Ｓ。 Ｃ 在 Ｓ 中是 无用的当且仅当 Ｓ 的无冗余等价子集恰为 Ｓ－｛Ｃ｝ 的无冗余等价子集。 定理 ４ ［１３］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，且 Ｄ 中不含互补文字。 Ｄ 是 Ｓ 中冗余 子句当且仅当子句集 Ｓ′ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝∪｛Ｄ｝不 可满足。 定义 ５ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，Ｄ＝ ｘ∨Ｄ１ ，其中 ｘ 是一文字，Ｄ１ 是一子 句，如果 Ｄ ∧ Ｃ１ ∧ Ｃ２ ∧ … ∧ Ｃｍ ＝ Ｄ１ ∧ Ｃ１ ∧ Ｃ２ ∧… ∧ Ｃｍ ， 则称 ｘ 是 Ｄ 中关于 Ｓ 的冗余文字。 定理 ５ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中的子句集，Ｄ ＝ ｘ∨Ｄ１ ，如果 Ｄ１ 是 Ｓ′ ＝ ｛Ｃ１ ，Ｃ２ ， …，Ｃｍ ，Ｄ１ ｝中的冗余子句，则 ｘ 是 Ｄ 中关于 Ｓ 的冗 余文字。 定理 ６ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，Ｄ＝ ｘ∨Ｄ１ ，ｘ 是 Ｄ 中关于 Ｓ 的冗余文字 当且仅当 Ｄ１ 是子句集 Ｓ′ ＝ ｛Ｄ１ ，ｘ，Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝中 的冗余子句。 定理 ７ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，且 Ｄ 中不含互补文字。 Ｄ 是 Ｓ 中冗余 子句当且仅当子句集 Ｓ′ ＝ ｛Ｃ１ －Ｄ，Ｃ２ －Ｄ，…，Ｃｍ －Ｄ｝ 不可满足。 对于子句集 Ｓ，令 Ｓ ｜ ｘ ＝ ｛Ｃ ｜ Ｃ∈Ｓ 且｛ ｘ，¬ ｘ｝∩ Ｃ ＝∅｝ ∪ ｛ Ｃ ＼ ｛ ¬ ｘ｝ ｜ Ｃ ∈ Ｓ 且 ¬ ｘ ∈ Ｃ｝， Ｓ ｜ Ａ ＝ （…（（Ｓ ｜ ｘ１ ） ｜ ｘ２ ）… ｜ ｘｎ ），其中Ａ ＝ ｛ｘ１ ，ｘ２ ，…，ｘｎ ｝。 定理 ８ ［１３］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，子句集 Ｓ ′ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝ ∪｛Ｄ｝ 不 可满足当且仅当子句集（Ｓ ＼｛Ｄ｝） ｜ Ｄ不可满足。 ２ 子句集中文字的分类 定义 ６ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，且 ｘ 不是 Ｃｉ 中关于 Ｓ 的冗余文字，则称 ｘ 是 Ｓ 中的必需文字。 定义 ７ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 第 ５ 期 邓鹏，等：命题逻辑的子句集中文字的分类 ·７３７·
·738 智能系统学报 第10卷 的子句集，如果存在S中的一个子句C:,若有C= 的子句集，如果对于S中的任一子句C:,若有C= xVD(i∈{1,2，…，m}),其中x是一文字，D是一子 xVD(i∈{1,2，…，m}),其中x是一文字，D是一 句，且x不是C:中关于S的冗余文字，则称x是S 子句，则称x是S中的无用文字当且仅当S:'的无冗 中的有用文字。 余等价子集恰为S:'-{D,}的无冗余等价子集，其中 定义8设S={C,C2,…,Cm}是命题逻辑中 S={Dx,C,…,C-,C1,…,Cnm}(ie{1,2,…,m})。 的子句集，如果对于S中的任一子句C,若有C:= 证明因为x是$中的无用文字，所以x一定 xVD(i∈{1,2，…，m}),其中x是一文字，D是一 是C:关于S的冗余文字，由定理6知x是C:中关于 子句，且x是C中关于S的冗余文字，则称x是S S的冗余文字当且仅当D:是子句集S'={D:,x,C, 中的无用文字。 …,C-1,C1,…,Cm}(i∈{1，…，m})中的冗余子 从定义6~8可以看出，子句集中的必需文字一 句，因此D在S'中是无用的，由定理3知D在S 定是有用文字，有用文字不一定是必需文字，同时有 中是无用的当且仅当S:'的无冗余等价子集恰为 用和无用是2个相对的概念，子句集中的必需文字 S:'-{D}的无冗余等价子集。 一定是非冗余文字，子句集中的无用文字一定是冗 3子句集中文字的判定 余文字。 定理9设S={C,C2,…,Cm}是命题逻辑中 根据子句集中文字的分类和冗余子句与子句集 的子句集，如果对于S中的任一子句C,若有C:= 的可满足性判定的关系可以得到如下定理。 xVD,(i∈{1,2，…，m}),其中x是一文字，D是一 定理12设S={C1,C2,…,Cm}是命题逻辑中 子句，x是S中的必需文字当且仅当S”:-{D}≠ 的子句集，如果对于S中的任一子句C:,有C:= D,S={D,x,C1,…,C-1,C1,…,Cm}(ie{1,2, xVD(ie{1,2,…,m}),其中x是一文字，D是一 …,m})。 子句，且D:中不含互补文字，则x是S中的无用文 证明因为x是S中的必需文字，所以x一定 字当且仅当子句集{x,C-D,…,C-1-D,C*1-D, 不是C:关于S的冗余文字，由定理6知x不是C:中 …,Cm-D}(i∈{1,2，…，m})不可满足。 关于S的冗余文字当且仅当D:不是子句集S,'= 证明若x是S中的无用文字，则一定存在 {D,x,C1,…,C-1,C41,…,Cm}(ie{1,2,…,m}) C:eS且C:=xVD,使x是C:中关于S的冗余文字， 中的冗余子句，因此D,在S,'中是必需的，由定理1则D:是子句集S,'={D,x,C1,…,C-1,C1,…,C} 知D,在S'中是必需的当且仅当S,'-{D,}≠D。 中的冗余子句，于是由定理7知D是子句集S:'= 推论1设S={C,C2,…,Cm}是命题逻辑中 {D,x,C…,C-1,C1,…,Cm}中的冗余子句当且仅 的子句集，如果存在S中的一个子句C,若有C,= 当子句集{x,C1-D,…,C-1-D,C1-D,…,Cm xVD(i∈{1，…，m}),其中x是一文字，D是一子 D}不可满足。 句，则x是S中的有用文字当且仅当S-{D≠D, 定理13设S={C1,C2,…,Cm}是命题逻辑中 其中S={D,x,C1,…,C-1,C+1,Cm}。 的子句集，如果对于S中的任一子句C,有C:=xV 定理10设S={C1,C2,…,Cm}是命题逻辑中 D.(i∈{1,2，…，m}),其中x是一文字，D,是一子 的子句集，如果存在S中的一个子句C,若有C= 句，且D:中不含互补文字，则x是S中的必需文字 xVD(i∈{1,2，…，m),其中x是一文字，D是一子 当且仅当子句集{x,C-D,…,C-1-D,C41-D,…, 句，则x是S中的有用文字当且仅当存在S'的一个 Cm-D}(i∈{1,2，…，m})可满足。 无冗余等价子集S"使S”-{D≠D,其中S={D,x, 证明7（充分性）若x不是S中的必需文字， C1,…,C-1,C41,…,Cm}。 则存在C∈S且C:=xVD,使x是C中关于S的冗 证明因为x是S中的有用文字，所以x一定 余文字，则D:是子句集S'={D,x,C,…,C-1, 不是C:关于S的冗余文字，由定理6知x不是C:中 C,…,C}中的冗余子句，即DAxΛCA…AC1A 关于S的冗余文字当且仅当D不是子句集S={D, C+1∧…ACm=xAC1Λ…ΛC-1ΛC1∧…ΛCmo x,C1,…,C-1,C+1,…,Cm}中的冗余子句，因此D在 又因为C:=xVD,所以xD,即x-D:=x。于是由 S'中是有用的，由定理2知D在S中是有用的当且 定理7知子句集{x,C,-D,…,C-1-D,C+1-D,…, 仅当存在S的一个无冗余等价子集S"使S"-{D≠ Cm-D}(i∈{1,2，…，m})不可满足，矛盾。 D,S'={D,x,C1,…,C-1,C+1,…,Cm}。 (必要性)假设子句集{x,C1-D,…,C-1-D, 定理11设S={C1,C2,…,Cm}是命题逻辑中 Ct1-D,…,Cm-D}不可满足，由定理7知D:是子
的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，且 ｘ 不是 Ｃｉ 中关于 Ｓ 的冗余文字，则称 ｘ 是 Ｓ 中的有用文字。 定义 ８ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，且 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字，则称 ｘ 是 Ｓ 中的无用文字。 从定义 ６～８ 可以看出，子句集中的必需文字一 定是有用文字，有用文字不一定是必需文字，同时有 用和无用是 ２ 个相对的概念，子句集中的必需文字 一定是非冗余文字，子句集中的无用文字一定是冗 余文字。 定理 ９ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，ｘ 是 Ｓ 中的必需文字当且仅当 Ｓ′ｉ －｛Ｄｉ ｝ ⊨／ Ｄｉ，Ｓ′ｉ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ （ ｉ∈｛１，２， …，ｍ｝）。 证明 因为 ｘ 是 Ｓ 中的必需文字，所以 ｘ 一定 不是 Ｃｉ 关于 Ｓ 的冗余文字，由定理 ６ 知 ｘ 不是 Ｃｉ 中 关于 Ｓ 的冗余文字当且仅当 Ｄｉ 不是子句集 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ （ ｉ∈｛１，２，…，ｍ｝） 中的冗余子句，因此 Ｄｉ 在 Ｓｉ ′中是必需的，由定理 １ 知 Ｄｉ 在 Ｓｉ ′中是必需的当且仅当 Ｓｉ ′－｛Ｄｉ｝⊨／ Ｄｉ。 推论 １ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，则 ｘ 是 Ｓ 中的有用文字当且仅当 Ｓ′－｛Ｄ｝⊨／ Ｄ， 其中 Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，Ｃｍ ｝。 定理 １０ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，则 ｘ 是 Ｓ 中的有用文字当且仅当存在 Ｓ′的一个 无冗余等价子集 Ｓ″使 Ｓ″－｛Ｄ｝⊨／ Ｄ，其中 Ｓ′ ＝ ｛Ｄ，ｘ， Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝。 证明 因为 ｘ 是 Ｓ 中的有用文字，所以 ｘ 一定 不是 Ｃｉ 关于 Ｓ 的冗余文字，由定理 ６ 知 ｘ 不是 Ｃｉ 中 关于 Ｓ 的冗余文字当且仅当 Ｄ 不是子句集 Ｓ′ ＝ ｛Ｄ， ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句，因此 Ｄ 在 Ｓ′中是有用的，由定理 ２ 知 Ｄ 在 Ｓ′中是有用的当且 仅当存在 Ｓ′的一个无冗余等价子集 Ｓ″使 Ｓ″－｛Ｄ｝⊨／ Ｄ，Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝。 定理 １１ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，则称 ｘ 是 Ｓ 中的无用文字当且仅当 Ｓｉ ′的无冗 余等价子集恰为 Ｓｉ ′－｛Ｄｉ ｝的无冗余等价子集，其中 Ｓ′ｉ ＝｛Ｄｉ，ｘ，Ｃ１，…，Ｃｉ－１，Ｃｉ＋１，…，Ｃｍ｝（ｉ∈｛１，２，…，ｍ｝）。 证明 因为 ｘ 是 Ｓ 中的无用文字，所以 ｘ 一定 是 Ｃｉ 关于 Ｓ 的冗余文字，由定理 ６ 知 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字当且仅当 Ｄｉ 是子句集 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１ ， …，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ （ ｉ∈｛ １，…，ｍ｝） 中的冗余子 句，因此 Ｄｉ 在 Ｓｉ ′中是无用的，由定理 ３ 知 Ｄｉ 在 Ｓｉ 中是无用的当且仅当 Ｓｉ ′的无冗余等价子集恰为 Ｓｉ ′－｛Ｄｉ｝的无冗余等价子集。 ３ 子句集中文字的判定 根据子句集中文字的分类和冗余子句与子句集 的可满足性判定的关系可以得到如下定理。 定理 １２ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的无用文 字当且仅当子句集｛ ｘ，Ｃ１ －Ｄｉ，…，Ｃｉ－１ －Ｄｉ，Ｃｉ＋１ －Ｄｉ， …，Ｃｍ －Ｄｉ｝（ｉ∈｛１，２，…，ｍ｝）不可满足。 证明 若 ｘ 是 Ｓ 中的无用文字，则一定存在 Ｃｉ∈Ｓ且 Ｃｉ ＝ ｘ∨Ｄｉ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字， 则 Ｄｉ 是子句集 Ｓｉ ′＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ 中的冗余子句，于是由定理 ７ 知 Ｄｉ 是子句集 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句当且仅 当子句集｛ ｘ，Ｃ１ －Ｄｉ，…，Ｃｉ－１ －Ｄｉ，Ｃｉ＋１ －Ｄｉ，…，Ｃｍ － Ｄｉ｝不可满足。 定理 １３ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨ Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一子 句，且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的必需文字 当且仅当子句集｛ｘ，Ｃ１ －Ｄｉ，…，Ｃｉ－１ －Ｄｉ，Ｃｉ＋１ －Ｄｉ，…， Ｃｍ －Ｄｉ｝（ｉ∈｛１，２，…，ｍ｝）可满足。 证明 ７ （充分性）若 ｘ 不是 Ｓ 中的必需文字， 则存在 Ｃｉ∈Ｓ 且 Ｃｉ ＝ ｘ∨Ｄｉ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗 余文字，则 Ｄｉ 是子句集 Ｓｉ ′ ＝ ｛ Ｄｉ， ｘ，Ｃ１ ，…，Ｃｉ－１ ， Ｃｉ＋１，…，Ｃｍ｝中的冗余子句，即 Ｄｉ∧ｘ∧Ｃ１∧…∧Ｃｉ－１∧ Ｃｉ＋１∧…∧Ｃｍ ＝ ｘ∧Ｃ１ ∧…∧Ｃｉ－１ ∧Ｃｉ＋１ ∧…∧Ｃｍ 。 又因为 Ｃｉ ＝ ｘ∨Ｄｉ，所以 ｘ∉Ｄｉ，即 ｘ－Ｄｉ ＝ ｘ。 于是由 定理 ７ 知子句集｛ｘ，Ｃ１ －Ｄｉ，…，Ｃｉ－１ －Ｄｉ，Ｃｉ＋１ －Ｄｉ，…， Ｃｍ －Ｄｉ｝（ｉ∈｛１，２，…，ｍ｝）不可满足，矛盾。 （必要性）假设子句集｛ ｘ，Ｃ１ －Ｄｉ，…，Ｃｉ－１ －Ｄｉ， Ｃｉ＋１ －Ｄｉ，…，Ｃｍ －Ｄｉ｝不可满足，由定理 ７ 知 Ｄｉ 是子 ·７３８· 智 能 系 统 学 报 第 １０ 卷
第5期 邓鹏，等：命题逻辑的子句集中文字的分类 ·739. 句集S:'={D,x,C,…,C-1,C1,…,Cm}中的冗余 已知矛盾。 子句，则x不是S中的必需文字，矛盾。 (必要性)假设子句集{x,C1,…,C-1,C*1,…, 定理14设S={C1,C2,…,Cm}是命题逻辑中 Cm}UHD:}不可满足，那么由定理4知D:是子句集 的子句集，如果存在S中的一个子句C,若有C:= S'={D,x,C,…,C-1,C#1,…,Cn}中的冗余子句， xVD(ie{1,2,…,m}),其中x是一文字，D是一子 则x不是S中的必需文字，矛盾。 句，则x是S中的有用文字当且仅当子句集{x,C,- D,…,C-1-D,C41-D,…,Cm-D可满足。 定理17设S={C1,C2,…,Cm}是命题逻辑中 的子句集，如果存在S中的一个子句C:,若有C:= 证明（充分性）若x不是S中的有用文字，则 xVD(ie{1,2,…,m}),其中x是一文字，D是一子 存在C:∈S且C,=xVD,使x是C:中关于S的冗余 句，则x是S中的有用文字当且仅当子句集{x,C, 文字，则D是子句集S={D,x,C1,…,C1,C+1,…, Cm}中的冗余子句，即DAxAC1A…AC-1AC1A …,C-1,C1,…,Cm}U{D}可满足。 …ACm=xAC1∧…AC-1AC41A…ACm。又因为 证明（充分性）若x不是S中的有用文字，则 C:=xVD,所以xD,于是由定理7知子句集 存在C:∈S且C,=xVD,使x是C:中关于S的冗余 {x,C-D,…,C-1-D,C1-D,…,Cm-D}不可满足， 文字，则D是子句集S'={D,x,C,…,C-1,C+1,…, 矛盾。 Cm}中的冗余子句，于是由定理4知子句集{x,C, (必要性)假设子句集{x,C1-D,…,C-1-D,C1 …,C-1,C41,…,Cm}U{D}不可满足，这显然与已 D,…,Cm-D}不可满足，由定理7知D是子句集S= 知矛盾。 {D,x,C,…,C-1,C1,…,Cm}中的冗余子句，则 (必要性)假设子句集{x,C1,…,C-,C1,…, x不是S中的有用文字，矛盾。 Cm}U{D}不可满足，那么由定理4知D是子句集 定理15设S={C1,C2,…,Cm}是命题逻辑中 的子句集，如果对于S中的任一子句C,有C:= S'={D,x,C,…,C-,C41,…,Cn}中的余子句， xVD(i∈{1,2，…，m}),其中x是一文字，D是一 则x不是S中的有用文字，矛盾。 子句，且D中不含互补文字，则x是S中的无用文 定理18设S={C1,C2,…,Cm}是命题逻辑中 字当且仅当子句集{x,C,…,C-1,C#1,…,Cm}U 的子句集，如果对于S中的任一子句C:,有C:=xV D(i∈{1,2，…，m}),其中x是一文字，D是一子 D}不可满足。 句，且D,中不含互补文字，则x是S中的无用文字 证明若x是S中的无用文字，则一定存在 当且仅当子句集(S:1{D})D不可满足，其中S:'= C:∈S且C=xVD:,使x是C:中关于S的冗余文字， {D,x,C1,…,C-1,C41,…,Cn}o 由定理1.6知x是C,中关于S的冗余文字当且仅当 证明由于C:∈S且C,=xVD,x是S中的无 D是子句集S'={D,x,C1,…,C-1,C+1,…,Cm}中 用文字，由定义知x是C:中关于S的冗余文字，所 的冗余子句，于是再由定理4知D是子句集S'= 以D:是子句集S'={D,x,C,…,C-1,C1,…,Cm} {D,x,C1,…,C-1,C1,…,Cm}中的冗余子句当且 中的冗余子句，再由定理4和定理8可以得出充要 仅当子句集{x,C,…,C-1,C41,…,Cm}U{D}不可 条件。 满足。 定理19设S={C1,C2,…,Cm}是命题逻辑中 定理16设S={C1,C2,…,Cm}是命题逻辑中 的子句集，如果对于S中的任一子句C,有C,=xV 的子句集，如果对于S中的任一子句C:,有C:=xV D.(i∈{1，…，m}),其中x是一文字，D是一子句， D.(ie{1,…,m}),其中x是一文字，D是一子句， 且D:中不含互补文字，则x是S中的必需文字当且 且D:中不含互补文字，则x是S中的必需文字当且 仅当子句集(S:1{D)可满足，其中S,'={D,x, 仅当子句集{x,C1,…,C-1,C1,…,Cm}U{D}可 C1,…,C-1,C41,…,Cm}。 满足。 证明（充分性）由于C:∈S,C:=xVD:,假设x 证明（充分性）若x不是S中的必需文字，则 不是S中的必需文字，由定义可以知x是C,中关于 存在C:∈S且C:=xVD,使x是C:中关于S的冗余 S的冗余文字，所以D:是子句集S:={D,x,C1,…, 文字，则D是子句集S'={D,x,C,…,C-1,C1, C-1,C1,…,Cm}中的冗余子句，再由定理4和定理 …,Cm}中的冗余子句，于是由定理4知子句集{x, 8可以得出子句集(S,\{D:})1。不可满足，矛盾。 C,…,C1,C1,…,Cm}U{D}不可满足，这显然与 (必要性)假设(S':1{D:})I。不可满足由定理
句集 Ｓｉ ′＝ ｛Ｄｉ，ｘ，Ｃｉ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余 子句，则 ｘ 不是 Ｓ 中的必需文字，矛盾。 定理 １４ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，则 ｘ 是 Ｓ 中的有用文字当且仅当子句集｛ｘ，Ｃ１ － Ｄ，…，Ｃｉ－１ －Ｄ，Ｃｉ＋１ －Ｄ，…，Ｃｍ －Ｄ｝可满足。 证明 （充分性）若 ｘ 不是 Ｓ 中的有用文字，则 存在 Ｃｉ∈Ｓ 且 Ｃｉ ＝ ｘ∨Ｄ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余 文字，则 Ｄ 是子句集 Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…， Ｃｍ ｝中的冗余子句，即 Ｄ∧ｘ∧Ｃ１∧…∧Ｃｉ－１∧Ｃｉ＋１∧ …∧Ｃｍ ＝ ｘ∧Ｃ１∧…∧Ｃｉ－１∧Ｃｉ＋１∧…∧Ｃｍ 。 又因为 Ｃｉ ＝ ｘ ∨ Ｄ， 所以 ｘ ∉ Ｄ， 于是由定理 ７ 知子句集 ｛ｘ，Ｃ１ －Ｄ，…，Ｃｉ－１ －Ｄ，Ｃｉ＋１ －Ｄ，…，Ｃｍ －Ｄ｝不可满足， 矛盾。 （必要性）假设子句集｛ｘ，Ｃ１ －Ｄ，…，Ｃｉ－１ －Ｄ，Ｃｉ＋１ － Ｄ，…，Ｃｍ －Ｄ｝不可满足，由定理 ７ 知 Ｄ 是子句集Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ 中的冗余子句，则 ｘ 不是 Ｓ 中的有用文字，矛盾。 定理 １５ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的无用文 字当且仅当子句集｛ ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ ∪ ｛Ｄｉ｝不可满足。 证明 若 ｘ 是 Ｓ 中的无用文字，则一定存在 Ｃｉ∈Ｓ且 Ｃｉ ＝ ｘ∨Ｄｉ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字， 由定理 １．６ 知 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字当且仅当 Ｄｉ 是子句集 Ｓｉ ′＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中 的冗余子句，于是再由定理 ４ 知 Ｄｉ 是子句集 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句当且 仅当子句集｛ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝∪｛Ｄｉ｝不可 满足。 定理 １６ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨ Ｄｉ（ｉ∈｛１，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一子句， 且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的必需文字当且 仅当子句集｛ ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ ∪｛Ｄｉ ｝ 可 满足。 证明 （充分性）若 ｘ 不是 Ｓ 中的必需文字，则 存在 Ｃｉ∈Ｓ 且 Ｃｉ ＝ ｘ∨Ｄｉ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余 文字，则 Ｄｉ 是子句集 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ， …，Ｃｍ ｝中的冗余子句，于是由定理 ４ 知子句集｛ ｘ， Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝∪｛Ｄｉ｝不可满足，这显然与 已知矛盾。 （必要性）假设子句集｛ ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…， Ｃｍ ｝∪｛Ｄｉ｝不可满足，那么由定理 ４ 知 Ｄｉ 是子句集 Ｓｉ ′＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句， 则 ｘ 不是 Ｓ 中的必需文字，矛盾。 定理 １７ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，则 ｘ 是 Ｓ 中的有用文字当且仅当子句集｛ ｘ，Ｃ１ ， …，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝∪｛Ｄ｝可满足。 证明 （充分性）若 ｘ 不是 Ｓ 中的有用文字，则 存在 Ｃｉ∈Ｓ 且 Ｃｉ ＝ ｘ∨Ｄ，使 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余 文字，则 Ｄ 是子句集 Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…， Ｃｍ ｝中的冗余子句，于是由定理 ４ 知子句集｛ ｘ，Ｃ１ ， …，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ ∪｛Ｄ｝ 不可满足，这显然与已 知矛盾。 （必要性）假设子句集｛ ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…， Ｃｍ｝∪｛Ｄ｝不可满足，那么由定理 ４ 知 Ｄ 是子句集 Ｓ′＝ ｛Ｄ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ 中的冗余子句， 则 ｘ 不是 Ｓ 中的有用文字，矛盾。 定理 １８ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨ Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一子 句，且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的无用文字 当且仅当子句集（Ｓ′ｉ ＼｛Ｄｉ｝） ｜ Ｄｉ不可满足，其中 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝。 证明 由于 Ｃｉ∈Ｓ 且 Ｃｉ ＝ ｘ∨Ｄｉ，ｘ 是 Ｓ 中的无 用文字，由定义知 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字，所 以 Ｄｉ 是子句集 Ｓｉ ′＝ ｛Ｄｉ，ｘ，Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝ 中的冗余子句，再由定理 ４ 和定理 ８ 可以得出充要 条件。 定理 １９ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，有 Ｃｉ ＝ ｘ∨ Ｄｉ（ｉ∈｛１，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一子句， 且 Ｄｉ 中不含互补文字，则 ｘ 是 Ｓ 中的必需文字当且 仅当子句集（Ｓｉ ′＼｛Ｄｉ｝） ｜ Ｄｉ可满足，其中 Ｓｉ ′ ＝ ｛Ｄｉ，ｘ， Ｃ１ ，…，Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝。 证明 （充分性）由于 Ｃｉ∈Ｓ，Ｃｉ ＝ ｘ∨Ｄｉ，假设 ｘ 不是 Ｓ 中的必需文字，由定义可以知 ｘ 是 Ｃｉ 中关于 Ｓ 的冗余文字，所以 Ｄｉ 是子句集 Ｓ ′ ｉ ＝ ｛Ｄｉ，ｘ，Ｃ１ ，…， Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句，再由定理 ４ 和定理 ８ 可以得出子句集（Ｓｉ ′＼｛Ｄｉ｝） ｜ Ｄｉ不可满足，矛盾。 （必要性）假设（Ｓ′ｉ ＼ ｛Ｄｉ ｝） ｜ Ｄｉ不可满足由定理 第 ５ 期 邓鹏，等：命题逻辑的子句集中文字的分类 ·７３９·
·740 智能系统学报 第10卷 4和定理8可知x一定是C:关于S的冗余文字，这 [6]MANTHEY N.Coprocessor 2.0-A flexible CNF simplifier 与x是S中的必需文字矛盾。 [J].Theory and Applications of Satisfiability Testing-SAT, 定理20设S={C1,C2,…,Cm}是命题逻辑中 2012,7317:436-441. [7]BELOV A,JANOTA M,LYNCE 1,et al.On computing 的子句集，如果存在S中的一个子句C,若有C:= minimal equivalent subformulas[].Principles and Practice xVD(i∈{1,2，…，m),其中x是一文字，D是一子 of Constraint Programming,2012,7514:158-174. 句，则x是S中的有用文字当且仅当子句集 [8]张建.逻辑公式的可满足性判定一方法、工具及应用 (S1{D})b可满足，其中S={D,x,C,…,C-1, [M].北京：科学出版社，2000：22-30. [9]许有军.基于扩展规则的若干SAT问题研究[D].长春： Ct1,…,Cm}。 吉林大学，2011：15-28. 证明（充分性）由于C:∈S,C:=xVD,假设x XU Youjun.Research on several SAT issues based on exten- 不是S中的有用文字，由定义知x一定是C:中关于 sion rule[D].Changchun,China:Jilin University,2011: S的冗余文字，所以D是子句集S={D,x,C1,…, 15-28. [10]CHANG C L,LEE R C T.Symbolic logic and mechanical C-,C+1,…,Cm}中的冗余子句，再由定理4和定理 theorem proving[M].New York:Academic Press,1973: 8可以得出子句集(S八{D)|云不可满足，矛盾。 19-73,22-25. (必要性)假设(S\D)|不可满足由定理4和 [11]LIU Yi,JIA Hairui,XU Yang.Determination of 3-Ary o- 定理8可知x一定是C中关于S的冗余文字，这与 resolution in lattice-valued propositional logic IP(X)[J]. International Journal of Computational Intelligence Sys- x是S中的有用文字矛盾。 tems,2013,6(5):943-953. 4结束语 [12]翟翠红，秦克云.命题逻辑公式中的冗余子句及冗余文 字[J].计算机科学，2013,40(5)：48-50. 本文主要研究命题逻辑的子句集中必需文字、 ZHAI Cuihong,QIN Keyun.Redundancy clause and re- 有用文字和无用文字的特征，讨论它们相应的等价 dundancy literal of propositional logic[J].Computer Sci- ence,2013,40(5):48-50. 条件。然后运用冗余文字和冗余子句的知识，得到 [13]唐世辉.命题逻辑中子句集的冗余性研究[D].成都： 必需文字、有用文字和无用文字与子句集可满足性 西南交通大学，2014：30-35. 的判定方法。该方法丰富了命题逻辑的子句集中文 TANG Shihui.Research redundancy of set of clauses in 字的分类方法，得到子句集中文字特征的判定方法， propositional logic[D].Chengdu,China:Southwest Jiao- tong University,2014:30-35. 为命题逻辑公式的化简奠定了理论基础。但是目前 [14]王国俊.数理逻辑引论与归结原理[M].北京：科学出 的冗余文字判定方法对子句集中文字属性的判断处 版社，2006：16-25. 理过程比较复杂，下一步将继续深入研究子句集的 WANG Guojun.Introduction to mathematical logie and res- 分类，为命题逻辑中子句集的化简和高效的归结自 olution principle M].Beijing:Science Press,2006: 动推理提供理论支撑。 16-25. [15]MUGGLETON S.Inductive logic programming J].New 参考文献： Generation Computing,1991,8(4):295-318. 作者简介： [1]LIBERATORE P.Redundancy in logic I:CNF propositional 邓鹏，男，1989年生，硕士研究生， formulae[J].Artificial Intelligence,2005,163(2):203- 主要研究方向为逻辑与推理。 232. [2]LIBERATORE P.Redundancy in logic II:2CNF and Horn propositional formulae J].Artificial Intelligence,2008, 172(2/3):265-299. [3]BOUFKHAD Y,ROUSSEL O.Redundancy in random SAT formulas[Cl//Proceedings of the 7th National Conference on Artificial Intelligence.[S.I.]2000:273-278. 徐扬，男，1956年生.教授.博士生 [4]FOURDRINOY O,GREGOIRE E.MAZURE B.et al.E- 导师，主要研究方向为逻辑代数、代数 liminating redundant clauses in sat instances[M]//Integra- 逻辑、不确定性推理和自动推理。 tion of Al and OR Techniques in Constraint Programming for Combinatorial Optimization Problems.Berlin/Heidelberg: Springer,2007:71-83. [5]KULLMANN O.Constraint satisfaction problems in clausal form II:Minimal unsatisability and conict structure [J]. Fundamenta Informaticae,2011,109(1):83-119
４ 和定理 ８ 可知 ｘ 一定是 Ｃｉ 关于 Ｓ 的冗余文字，这 与 ｘ 是 Ｓ 中的必需文字矛盾。 定理 ２０ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果存在 Ｓ 中的一个子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄ 是一子 句，则 ｘ 是 Ｓ 中 的 有 用 文 字 当 且 仅 当 子 句 集 （Ｓ′＼｛Ｄ｝） Ｄ 可满足，其中 Ｓ′ ＝ ｛Ｄ， ｘ，Ｃ１ ，…，Ｃｉ－１ ， Ｃｉ＋１ ，…，Ｃｍ ｝。 证明 （充分性）由于 Ｃｉ∈Ｓ，Ｃｉ ＝ ｘ∨Ｄ，假设 ｘ 不是 Ｓ 中的有用文字，由定义知 ｘ 一定是 Ｃｉ 中关于 Ｓ 的冗余文字，所以 Ｄ 是子句集 Ｓ′ ＝ ｛Ｄ，ｘ，Ｃ１ ，…， Ｃｉ－１ ，Ｃｉ＋１ ，…，Ｃｍ ｝中的冗余子句，再由定理 ４ 和定理 ８ 可以得出子句集（Ｓ′＼｛Ｄ｝） ｜ Ｄ不可满足，矛盾。 （必要性）假设（Ｓ′＼Ｄ｝） ｜ Ｄ不可满足由定理 ４ 和 定理 ８ 可知 ｘ 一定是 Ｃｉ 中关于 Ｓ 的冗余文字，这与 ｘ 是 Ｓ 中的有用文字矛盾。 ４ 结束语 本文主要研究命题逻辑的子句集中必需文字、 有用文字和无用文字的特征，讨论它们相应的等价 条件。 然后运用冗余文字和冗余子句的知识，得到 必需文字、有用文字和无用文字与子句集可满足性 的判定方法。 该方法丰富了命题逻辑的子句集中文 字的分类方法，得到子句集中文字特征的判定方法， 为命题逻辑公式的化简奠定了理论基础。 但是目前 的冗余文字判定方法对子句集中文字属性的判断处 理过程比较复杂，下一步将继续深入研究子句集的 分类，为命题逻辑中子句集的化简和高效的归结自 动推理提供理论支撑。 参考文献： ［１］ＬＩＢＥＲＡＴＯＲＥ Ｐ． Ｒｅｄｕｎｄａｎｃｙ ｉｎ ｌｏｇｉｃ Ｉ： ＣＮＦ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｆｏｒｍｕｌａｅ［ Ｊ］． Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ， ２００５， １６３（ ２）： ２０３⁃ ２３２． ［２］ＬＩＢＥＲＡＴＯＲＥ Ｐ． Ｒｅｄｕｎｄａｎｃｙ ｉｎ ｌｏｇｉｃ ＩＩ： ２ＣＮＦ ａｎｄ Ｈｏｒｎ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｆｏｒｍｕｌａｅ ［ Ｊ ］． Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ， ２００８， １７２（２ ／ ３）： ２６５⁃２９９． ［３］ＢＯＵＦＫＨＡＤ Ｙ， ＲＯＵＳＳＥＬ Ｏ． Ｒｅｄｕｎｄａｎｃｙ ｉｎ ｒａｎｄｏｍ ＳＡＴ ｆｏｒｍｕｌａｓ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ７ｔｈ Ｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒｔｉfiｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ． ［Ｓ．ｌ．］， ２０００： ２７３⁃２７８． ［４］ ＦＯＵＲＤＲＩＮＯＹ Ｏ， ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ｅｔ ａｌ． Ｅ⁃ ｌｉｍｉｎａｔｉｎｇ ｒｅｄｕｎｄａｎｔ ｃｌａｕｓｅｓ ｉｎ ｓａｔ ｉｎｓｔａｎｃｅｓ［Ｍ］ ／ ／ Ｉｎｔｅｇｒａ⁃ ｔｉｏｎ ｏｆ ＡＩ ａｎｄ ＯＲ Ｔｅｃｈｎｉｑｕｅｓ ｉｎ Ｃｏｎｓｔｒａｉｎｔ Ｐｒｏｇｒａｍｍｉｎｇ ｆｏｒ Ｃｏｍｂｉｎａｔｏｒｉａｌ Ｏｐｔｉｍｉｚａｔｉｏｎ Ｐｒｏｂｌｅｍｓ． Ｂｅｒｌｉｎ ／ Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７： ７１⁃８３． ［５］ＫＵＬＬＭＡＮＮ Ｏ． Ｃｏｎｓｔｒａｉｎｔ ｓａｔｉｓｆａｃｔｉｏｎ ｐｒｏｂｌｅｍｓ ｉｎ ｃｌａｕｓａｌ ｆｏｒｍ ＩＩ： Ｍｉｎｉｍａｌ ｕｎｓａｔｉｓａｂｉｌｉｔｙ ａｎｄ ｃｏｎｉｃｔ ｓｔｒｕｃｔｕｒｅ ［ Ｊ ］． Ｆｕｎｄａｍｅｎｔａ Ｉｎｆｏｒｍａｔｉｃａｅ， ２０１１， １０９（１）： ８３⁃１１９． ［６］ ＭＡＮＴＨＥＹ Ｎ． Ｃｏｐｒｏｃｅｓｓｏｒ ２．０—Ａ ｆｌｅｘｉｂｌｅ ＣＮＦ ｓｉｍｐｌｉｆｉｅｒ ［Ｊ］． Ｔｈｅｏｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ－ＳＡＴ， ２０１２， ７３１７： ４３６⁃４４１． ［７］ ＢＥＬＯＶ Ａ， ＪＡＮＯＴＡ Ｍ， ＬＹＮＣＥ Ｉ， ｅｔ ａｌ． Ｏｎ ｃｏｍｐｕｔｉｎｇ ｍｉｎｉｍａｌ ｅｑｕｉｖａｌｅｎｔ ｓｕｂｆｏｒｍｕｌａｓ［Ｊ］． Ｐｒｉｎｃｉｐｌｅｓ ａｎｄ Ｐｒａｃｔｉｃｅ ｏｆ Ｃｏｎｓｔｒａｉｎｔ Ｐｒｏｇｒａｍｍｉｎｇ， ２０１２， ７５１４： １５８⁃１７４． ［８］张建． 逻辑公式的可满足性判定———方法、工具及应用 ［Ｍ］． 北京： 科学出版社， ２０００： ２２⁃３０． ［９］许有军． 基于扩展规则的若干 ＳＡＴ 问题研究［Ｄ］． 长春： 吉林大学， ２０１１： １５⁃２８． ＸＵ Ｙｏｕｊｕｎ． Ｒｅｓｅａｒｃｈ ｏｎ ｓｅｖｅｒａｌ ＳＡＴ ｉｓｓｕｅｓ ｂａｓｅｄ ｏｎ ｅｘｔｅｎ⁃ ｓｉｏｎ ｒｕｌｅ［Ｄ］． Ｃｈａｎｇｃｈｕｎ， Ｃｈｉｎａ： Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， ２０１１： １５⁃２８． ［１０］ＣＨＡＮＧ Ｃ Ｌ， ＬＥＥ Ｒ Ｃ Ｔ． Ｓｙｍｂｏｌｉｃ ｌｏｇｉｃ ａｎｄ ｍｅｃｈａｎｉｃａｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ［Ｍ］． Ｎｅｗ Ｙｏｒｋ： Ａｃａｄｅｍｉｃ Ｐｒｅｓｓ，１９７３： １９⁃７３， ２２⁃２５． ［１１］ＬＩＵ Ｙｉ， ＪＩＡ Ｈａｉｒｕｉ， ＸＵ Ｙａｎｇ． Ｄｅｔｅｒｍｉｎａｔｉｏｎ ｏｆ ３⁃Ａｒｙ α⁃ ｒｅｓｏｌｕｔｉｏｎ ｉｎ ｌａｔｔｉｃｅ⁃ｖａｌｕｅｄ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ＬＰ（Ｘ） ［ Ｊ］． Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔａｔｉｏｎａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ Ｓｙｓ⁃ ｔｅｍｓ， ２０１３， ６（５）： ９４３⁃９５３． ［１２］翟翠红， 秦克云． 命题逻辑公式中的冗余子句及冗余文 字［Ｊ］． 计算机科学， ２０１３， ４０（５）： ４８⁃５０． ＺＨＡＩ Ｃｕｉｈｏｎｇ， ＱＩＮ Ｋｅｙｕｎ． Ｒｅｄｕｎｄａｎｃｙ ｃｌａｕｓｅ ａｎｄ ｒｅ⁃ ｄｕｎｄａｎｃｙ ｌｉｔｅｒａｌ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ［ Ｊ］． Ｃｏｍｐｕｔｅｒ Ｓｃｉ⁃ ｅｎｃｅ， ２０１３， ４０（５）： ４８⁃５０． ［１３］唐世辉． 命题逻辑中子句集的冗余性研究［Ｄ］．成都： 西南交通大学， ２０１４： ３０⁃３５． ＴＡＮＧ Ｓｈｉｈｕｉ． Ｒｅｓｅａｒｃｈ ｒｅｄｕｎｄａｎｃｙ ｏｆ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｉｎ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ［Ｄ］． Ｃｈｅｎｇｄｕ， Ｃｈｉｎａ： Ｓｏｕｔｈｗｅｓｔ Ｊｉａｏ⁃ ｔｏｎｇ Ｕｎｉｖｅｒｓｉｔｙ， ２０１４： ３０⁃３５． ［１４］王国俊． 数理逻辑引论与归结原理［Ｍ］． 北京： 科学出 版社， ２００６： １６⁃２５． ＷＡＮＧ Ｇｕｏｊｕｎ． Ｉｎｔｒｏｄｕｃｔｉｏｎ ｔｏ ｍａｔｈｅｍａｔｉｃａｌ ｌｏｇｉｃ ａｎｄ ｒｅｓ⁃ ｏｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ ［ Ｍ ］． Ｂｅｉｊｉｎｇ： Ｓｃｉｅｎｃｅ Ｐｒｅｓｓ， ２００６： １６⁃２５． ［１５］ ＭＵＧＧＬＥＴＯＮ Ｓ． Ｉｎｄｕｃｔｉｖｅ ｌｏｇｉｃ ｐｒｏｇｒａｍｍｉｎｇ ［ Ｊ］． Ｎｅｗ Ｇｅｎｅｒａｔｉｏｎ Ｃｏｍｐｕｔｉｎｇ， １９９１， ８（４）： ２９５⁃３１８． 作者简介： 邓鹏，男，１９８９ 年生，硕士研究生， 主要研究方向为逻辑与推理。 徐扬，男，１９５６ 年生，教授，博士生 导师， 主要研究方向为逻辑代数、代数 逻辑、不确定性推理和自动推理。 ·７４０· 智 能 系 统 学 报 第 １０ 卷
