Computer Science ›› 2019, Vol. 46 ›› Issue (8): 255-259.doi: 10.11896/j.issn.1002-137X.2019.08.042

• Artificial Intelligence • Previous Articles     Next Articles

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

CLC Number: 

  • 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] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[2] HAO Jiao, HUI Xiao-jing, MA Shuo, JIN Ming-hui. Study on Axiomatic Truth Degree in First-order Logic [J]. Computer Science, 2021, 48(11A): 669-671.
[3] WANG Yi-jie, XU Yang, WU Guan-feng. Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver [J]. Computer Science, 2021, 48(11): 294-299.
[4] SHEN Xue, CHEN Shu-wei, AI Sen-yang. Reward Mechanism Based Branching Strategy for SAT Solver [J]. Computer Science, 2020, 47(7): 42-46.
[5] LIU Jiang, ZHOU Hong-hao. New Algebraic Logic Reduction Method for Boolean Formula [J]. Computer Science, 2020, 47(5): 32-37.
[6] TANG Lei-ming, BAI Mu-chen, HE Xing-xing, LI Xing-yu. Complete Contradiction and Smallest Contradiction Based on Propositional Logic [J]. Computer Science, 2020, 47(11A): 83-85.
[7] LIU Jing-lei, LIAO Shi-zhong. Complexity of CP-nets Learning [J]. Computer Science, 2018, 45(6): 211-215.
[8] CHEN Qing-shan, XU Yang, WU Guan-feng. Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength [J]. Computer Science, 2018, 45(12): 137-141.
[9] CHEN Cheng, PAN Zheng-hua and LV Yong-xi. Fuzzy Modal Propositional Logic with Three Kinds of Negation [J]. Computer Science, 2017, 44(4): 263-268.
[10] XU Wei, LI Xiao-fen and LIU Duan-yang. Propositional Logic-based Association-rule Mining Algorithm L-Eclat [J]. Computer Science, 2017, 44(12): 211-215.
[11] CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing. Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver [J]. Computer Science, 2017, 44(11): 279-283.
[12] GUO Ying, ZHANG Chang-sheng and ZHANG Bin. Research Advance of SAT Solving Algorithm [J]. Computer Science, 2016, 43(3): 8-17.
[13] WU Xiao-gang and PAN Zheng-hua. Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic [J]. Computer Science, 2015, 42(Z11): 100-103.
[14] SUN Xue-jiao and LIU Jing-lei. Research on Algorithm of Satisfiability Ranking Generation for CP-nets [J]. Computer Science, 2015, 42(5): 270-273.
[15] LIU Yi, XU Yang and JIA Hai-rui. Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X) [J]. Computer Science, 2015, 42(4): 249-252.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!