计算机科学 ›› 2019, Vol. 46 ›› Issue (8): 255-259.doi: 10.11896/j.issn.1002-137X.2019.08.042

• 人工智能 • 上一篇    下一篇

命题逻辑中单元子句及其负文字和冗余子句

刘婷, 徐扬, 陈秀兰   

  1. (西南交通大学系统可信性自动验证国家地方联合工程实验室 成都610031)
  • 收稿日期:2018-06-30 出版日期:2019-08-15 发布日期:2019-08-15
  • 通讯作者: 徐扬(1956-),男,教授,博士生导师,主要研究方向为逻辑代数、代数逻辑、不确定性推理和自动推理,E-mail:xuyang@swjtu.edu.cn
  • 作者简介:刘婷(1992-),女,硕士生,主要研究方向为逻辑与推理;陈秀兰(1994-),女,硕士生,主要研究方向为自动推理
  • 基金资助:
    国家自然科学基金项目(61673320),中央高校研究基础基金项目(2682017ZT12,2682016CX119)

Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic

LIU Ting, XU Yang, CHEN Xiu-lan   

  1. (National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University,Chengdu 610031,China)
  • Received:2018-06-30 Online:2019-08-15 Published:2019-08-15

摘要: 针对命题逻辑中逻辑公式的某个单元子句及其负文字和冗余子句,给出了含单元子句的子句集的等价条件,同时刻画了子句集中文字和子句的冗余性,得到了一些冗余文字和冗余子句的判定方法,还提出了与子句集可满足性的等价条件。所提方法可以使命题逻辑的逻辑公式更简单,为命题逻辑中逻辑公式的简化提供一定的理论支撑。

关键词: 负文字, 可满足性, 命题逻辑, 冗余文字, 冗余子句

Abstract: In the logical formula of propositional logic,some equivalence conditions for the set of clauses containing an unit clause was given by studying the unit clause and its complementary literal,and the redundancy of literals and clauses in the set of clauses were described.The methods of judging redundant literals and redundant clauses were obtained,and the equivalence conditions of the satisfiability of clause sets were also proposed.These methods can simplify the logic formula and provide some theoretical support for simplifying the logic formula in propositional logic.

Key words: Complementary literals, Propositional logic, Redundant clauses, Redundant literals, Satisfiability

中图分类号: 

  • O141.1
[1]LIBERATORE P.Redundancy in logic I:CNF propositional formulae [J].Artificial Intelligence,2005,163(2):203-232.
[2]FOURDRINOY O,ÉRIC G,MAZURE B,et al.Eliminating Redundant Clauses in SAT Instances [C]∥Proceedings of International Conference on Integration of Ai and Or Techniques in Constraint Programming for Combinatorial Optimization Problems.DBLP,2007:71-83.
[3]GRIMM S,WISSMANN J.Elimination of Redundancy in Onto- logies [C]∥Extended Semantic Web Conference on the Semantic Web:Research and Applications.Springer-Verlag,2011:260-274.
[4]TANG S H.Research redundancy of set of clauses in propositional logic [D].Chengdu:Southwest Jiaotong University,2014.(in Chinese) 唐仕辉.命题逻辑中子句集的冗余性研究[D].成都:西南交通大学,2014.
[5]LAVRAC N,DZEROSKI S.Inductive Logic Programming[C]∥ International Conference on Inductive Logic Programming.1994:146-160.
[6]HEULE M,RVISALO M,LONSING F,et al.Clause elimination for SAT and QSAT[J].Journal of Artificial Intelligence Research,2015,53(1):127-168.
[7]ZHAI C H,QIN K Y.Redundancy clause and redundancy literal of proposition logic [J].Computer Science,2013,40(5):48-50.(in Chinese) 翟翠红,秦克云.命题逻辑公式中的冗余子句及冗余文字[J].计算机科学,2013,40(5):48-50.
[8]BOUFKHAD Y,ROUSSEL O.Redundancy in random SAT formulas [C]∥Seventeenth National Conference on Artificial Intelligence & Twelfth Conference on Innovative Applications of Artificial Intelligence.AAAI Press,2000:273-278.
[9]XU Y,ZOU K Q.Reducibility of literals andMintermsof Boolean Logic Formulas [J].Journal of Southwest Jiaotong University.1990,25(1):108-112.(in Chinese) 徐扬,邹开其.布尔逻辑公式中文字和小项的可消性[J].西南交通大学学报,1990,25(1):108-112.
[10]XU Y,SONG Z M.Reducibility of Phrase and Literal on Lattice-Value Logic Formula[J].Chinese Quarterly Journal of Mathematics,1990,5(1):172-181.(in Chinese) 徐扬,宋振明.格值逻辑公式中短语和文字的可消性[J].数学季刊,1990,5(1):172-181.
[11]HEULE M,JÄRVISALO M,BIERE A,et al.Clause Elimination Procedures for CNF Formulas [C]∥International Confe-rence on Logic for Programming Artificial Intelligence and Reasoning.DBLP,2010:357-371.
[12]DENG P,XU Y.Classification of Concentrated Texts in Clause of Propositional Logic[J].Journal of Intelligent Systems,2015,10(5):736-740.(in Chinese) 邓鹏,徐扬.命题逻辑的子句集中文字的分类[J].智能系统学报,2015,10(5):736-740.
[13]PALEO B W.Reducing redundancy in cut-elimination by resolution[J].Journal of Logic and Computation,2014,27(2):577-606.
[14]GU A H.Research on Redundancy Elimination Method in Mobile Network Service Information Transmission[J].Computer Simulation,2016,33(11):294-297.(in Chinese) 顾爱华.移动网络服务信息传输中冗余量消除方法研究[J].计算机仿真,2016,33(11):294-297.
[15]YUE C L,BJORK E L.Using selective redundancy to eliminate the seductive details effect[J].Applied Cognitive Psychology,2017,31(5):565-571.
[1] 李洁, 钟小梅.
命题逻辑中三元子句集的冗余文字
Redundant Literals of Ternary Clause Sets in Propositional Logic
计算机科学, 2022, 49(6A): 109-112. https://doi.org/10.11896/jsjkx.210700036
[2] 郝娇, 惠小静, 马硕, 金明慧.
一阶逻辑中公理化真度研究
Study on Axiomatic Truth Degree in First-order Logic
计算机科学, 2021, 48(11A): 669-671. https://doi.org/10.11896/jsjkx.210200012
[3] 王钇杰, 徐扬, 吴贯锋.
基于学习子句删除策略的SAT求解器分支策略
Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver
计算机科学, 2021, 48(11): 294-299. https://doi.org/10.11896/jsjkx.201000142
[4] 沈雪, 陈树伟, 艾森阳.
基于奖励机制的SAT求解器分支策略
Reward Mechanism Based Branching Strategy for SAT Solver
计算机科学, 2020, 47(7): 42-46. https://doi.org/10.11896/jsjkx.190700191
[5] 刘江, 周鸿昊.
一种布尔公式的代数逻辑约化新方法
New Algebraic Logic Reduction Method for Boolean Formula
计算机科学, 2020, 47(5): 32-37. https://doi.org/10.11896/jsjkx.190400018
[6] 曹锋,徐扬,钟建,宁欣然.
基于目标演绎距离的一阶逻辑子句集预处理方法
First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance
计算机科学, 2020, 47(3): 217-221. https://doi.org/10.11896/jsjkx.190100004
[7] 唐雷明, 白沐尘, 何星星, 黎兴玉.
基于命题逻辑的完全标准矛盾体及最小标准矛盾体
Complete Contradiction and Smallest Contradiction Based on Propositional Logic
计算机科学, 2020, 47(11A): 83-85. https://doi.org/10.11896/jsjkx.200400072
[8] 刘惊雷, 廖士中.
CP-nets学习的复杂度
Complexity of CP-nets Learning
计算机科学, 2018, 45(6): 211-215. https://doi.org/10.11896/j.issn.1002-137X.2018.06.038
[9] 陈青山, 徐扬, 吴贯锋.
基于趋势强度的SAT问题学习子句评估算法
Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength
计算机科学, 2018, 45(12): 137-141. https://doi.org/10.11896/j.issn.1002-137X.2018.12.021
[10] 陈成,潘正华,吕永席.
一类具有3种否定的模糊模态命题逻辑
Fuzzy Modal Propositional Logic with Three Kinds of Negation
计算机科学, 2017, 44(4): 263-268. https://doi.org/10.11896/j.issn.1002-137X.2017.04.055
[11] 徐卫,李晓粉,刘端阳.
基于命题逻辑的关联规则挖掘算法L-Eclat
Propositional Logic-based Association-rule Mining Algorithm L-Eclat
计算机科学, 2017, 44(12): 211-215. https://doi.org/10.11896/j.issn.1002-137X.2017.12.038
[12] 陈青山,徐扬,吴贯锋,何星星.
一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法
Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver
计算机科学, 2017, 44(11): 279-283. https://doi.org/10.11896/j.issn.1002-137X.2017.11.042
[13] 吴晓刚,潘正华.
基于模糊命题逻辑形式系统FLcom的模糊推理及应用
Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic
计算机科学, 2015, 42(Z11): 100-103.
[14] 孙雪姣,刘惊雷.
CP-nets的可满足性序列求解算法研究
Research on Algorithm of Satisfiability Ranking Generation for CP-nets
计算机科学, 2015, 42(5): 270-273. https://doi.org/10.11896/j.issn.1002-137X.2015.05.054
[15] 刘 熠,徐 扬,贾海瑞.
基于格值命题逻辑系统LP(X)的多元α-归结原理的注记
Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X)
计算机科学, 2015, 42(4): 249-252. https://doi.org/10.11896/j.issn.1002-137X.2015.04.051
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!