·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ｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ． ［Ｓ．ｌ．］， ２０００： ２７３⁃２７８． ［４］ ＦＯＵＲＤＲＩＮＯＹ Ｏ， ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ｅｔ ａｌ． Ｅ⁃ ｌｉｍｉｎａｔｉｎｇ ｒｅｄｕｎｄａｎｔ ｃｌａｕｓｅｓ ｉｎ ｓａｔ ｉｎｓｔａｎｃｅｓ［Ｍ］ ／ ／ Ｉｎｔｅｇｒａ⁃ ｔｉｏｎ ｏｆ ＡＩ ａｎｄ ＯＲ Ｔｅｃｈｎｉｑｕｅｓ ｉｎ Ｃｏｎｓｔｒａｉｎｔ Ｐｒｏｇｒａｍｍｉｎｇ ｆｏｒ Ｃｏｍｂｉｎａｔｏｒｉａｌ Ｏｐｔｉｍｉｚａｔｉｏｎ Ｐｒｏｂｌｅｍｓ． Ｂｅｒｌｉｎ ／ Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７： ７１⁃８３． ［５］ＫＵＬＬＭＡＮＮ Ｏ． Ｃｏｎｓｔｒａｉｎｔ ｓａｔｉｓｆａｃｔｉｏｎ ｐｒｏｂｌｅｍｓ ｉｎ ｃｌａｕｓａｌ ｆｏｒｍ ＩＩ： Ｍｉｎｉｍａｌ ｕｎｓａｔｉｓａｂｉｌｉｔｙ ａｎｄ ｃｏｎｉｃｔ ｓｔｒｕｃｔｕｒｅ ［ Ｊ ］． Ｆｕｎｄａｍｅｎｔａ Ｉｎｆｏｒｍａｔｉｃａｅ， ２０１１， １０９（１）： ８３⁃１１９． ［６］ ＭＡＮＴＨＥＹ Ｎ． Ｃｏｐｒｏｃｅｓｓｏｒ ２．０—Ａ ｆｌｅｘｉｂｌｅ ＣＮＦ ｓｉｍｐｌｉｆｉｅｒ ［Ｊ］． Ｔｈｅｏｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ－ＳＡＴ， ２０１２， ７３１７： ４３６⁃４４１． ［７］ ＢＥＬＯＶ Ａ， ＪＡＮＯＴＡ Ｍ， ＬＹＮＣＥ Ｉ， ｅｔ ａｌ． Ｏｎ ｃｏｍｐｕｔｉｎｇ ｍｉｎｉｍａｌ ｅｑｕｉｖａｌｅｎｔ ｓｕｂｆｏｒｍｕｌａｓ［Ｊ］． Ｐｒｉｎｃｉｐｌｅｓ ａｎｄ Ｐｒａｃｔｉｃｅ ｏｆ Ｃｏｎｓｔｒａｉｎｔ Ｐｒｏｇｒａｍｍｉｎｇ， ２０１２， ７５１４： １５８⁃１７４． ［８］张建． 逻辑公式的可满足性判定———方法、工具及应用 ［Ｍ］． 北京： 科学出版社， ２０００： ２２⁃３０． ［９］许有军． 基于扩展规则的若干 ＳＡＴ 问题研究［Ｄ］． 长春： 吉林大学， ２０１１： １５⁃２８． ＸＵ Ｙｏｕｊｕｎ． Ｒｅｓｅａｒｃｈ ｏｎ ｓｅｖｅｒａｌ ＳＡＴ ｉｓｓｕｅｓ ｂａｓｅｄ ｏｎ ｅｘｔｅｎ⁃ ｓｉｏｎ ｒｕｌｅ［Ｄ］． Ｃｈａｎｇｃｈｕｎ， Ｃｈｉｎａ： Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， ２０１１： １５⁃２８． ［１０］ＣＨＡＮＧ Ｃ Ｌ， ＬＥＥ Ｒ Ｃ Ｔ． Ｓｙｍｂｏｌｉｃ ｌｏｇｉｃ ａｎｄ ｍｅｃｈａｎｉｃａｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ［Ｍ］． Ｎｅｗ Ｙｏｒｋ： Ａｃａｄｅｍｉｃ Ｐｒｅｓｓ，１９７３： １９⁃７３， ２２⁃２５． ［１１］ＬＩＵ Ｙｉ， ＪＩＡ Ｈａｉｒｕｉ， ＸＵ Ｙａｎｇ． Ｄｅｔｅｒｍｉｎａｔｉｏｎ ｏｆ ３⁃Ａｒｙ α⁃ ｒｅｓｏｌｕｔｉｏｎ ｉｎ ｌａｔｔｉｃｅ⁃ｖａｌｕｅｄ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ ＬＰ（Ｘ） ［ Ｊ］． Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔａｔｉｏｎａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ Ｓｙｓ⁃ ｔｅｍｓ， ２０１３， ６（５）： ９４３⁃９５３． ［１２］翟翠红， 秦克云． 命题逻辑公式中的冗余子句及冗余文 字［Ｊ］． 计算机科学， ２０１３， ４０（５）： ４８⁃５０． ＺＨＡＩ Ｃｕｉｈｏｎｇ， ＱＩＮ Ｋｅｙｕｎ． Ｒｅｄｕｎｄａｎｃｙ ｃｌａｕｓｅ ａｎｄ ｒｅ⁃ ｄｕｎｄａｎｃｙ ｌｉｔｅｒａｌ ｏｆ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ［ Ｊ］． Ｃｏｍｐｕｔｅｒ Ｓｃｉ⁃ ｅｎｃｅ， ２０１３， ４０（５）： ４８⁃５０． ［１３］唐世辉． 命题逻辑中子句集的冗余性研究［Ｄ］．成都： 西南交通大学， ２０１４： ３０⁃３５． ＴＡＮＧ Ｓｈｉｈｕｉ． Ｒｅｓｅａｒｃｈ ｒｅｄｕｎｄａｎｃｙ ｏｆ ｓｅｔ ｏｆ ｃｌａｕｓｅｓ ｉｎ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ［Ｄ］． Ｃｈｅｎｇｄｕ， Ｃｈｉｎａ： Ｓｏｕｔｈｗｅｓｔ Ｊｉａｏ⁃ ｔｏｎｇ Ｕｎｉｖｅｒｓｉｔｙ， ２０１４： ３０⁃３５． ［１４］王国俊． 数理逻辑引论与归结原理［Ｍ］． 北京： 科学出 版社， ２００６： １６⁃２５． ＷＡＮＧ Ｇｕｏｊｕｎ． Ｉｎｔｒｏｄｕｃｔｉｏｎ ｔｏ ｍａｔｈｅｍａｔｉｃａｌ ｌｏｇｉｃ ａｎｄ ｒｅｓ⁃ ｏｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ ［ Ｍ ］． Ｂｅｉｊｉｎｇ： Ｓｃｉｅｎｃｅ Ｐｒｅｓｓ， ２００６： １６⁃２５． ［１５］ ＭＵＧＧＬＥＴＯＮ Ｓ． Ｉｎｄｕｃｔｉｖｅ ｌｏｇｉｃ ｐｒｏｇｒａｍｍｉｎｇ ［ Ｊ］． Ｎｅｗ Ｇｅｎｅｒａｔｉｏｎ Ｃｏｍｐｕｔｉｎｇ， １９９１， ８（４）： ２９５⁃３１８． 作者简介： 邓鹏，男，１９８９ 年生，硕士研究生， 主要研究方向为逻辑与推理。 徐扬，男，１９５６ 年生，教授，博士生 导师， 主要研究方向为逻辑代数、代数 逻辑、不确定性推理和自动推理。 ·７４０· 智 能 系 统 学 报 第 １０ 卷