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 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: Propositional logic, Satisfiability, Redundant literals, Complementary literals, Redundant clauses

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] LIU Jing-lei, LIAO Shi-zhong. Complexity of CP-nets Learning [J]. Computer Science, 2018, 45(6): 211-215.
[2] 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.
[3] 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.
[4] 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.
[5] 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.
[6] GUO Ying, ZHANG Chang-sheng and ZHANG Bin. Research Advance of SAT Solving Algorithm [J]. Computer Science, 2016, 43(3): 8-17.
[7] 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, 122.
[8] 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, 285.
[9] 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, 280.
[10] WANG Xiao-feng, LI Qiang and DING Hong-sheng. Convergence of Warning Propagation Algorithm for Regular Structure Instances [J]. Computer Science, 2015, 42(1): 279-284.
[11] ZHOU Kuan-jiu,CHANG Jun-wang,HOU Gang,REN Long-tao and WANG Xiao-long. Interrupt Modeling and Verification for Embedded Systems Based on Time Petri Nets [J]. Computer Science, 2014, 41(9): 205-209,219.
[12] LI Shen,CHANG Liang,MENG Yu and LI Feng-ying. Branching Temporal Description Logic ALC-CTL and its Satisfiability Decision [J]. Computer Science, 2014, 41(3): 205-211.
[13] ZHAI Cui-hong and QIN Ke-yun. Redundancy Clause and Redundancy Literal of Propositional Logic [J]. Computer Science, 2013, 40(5): 48-50.
[14] . Detecting Behavioral Mismatch of Web Services Based on Bounded Model Checking [J]. Computer Science, 2012, 39(6): 129-132.
[15] GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203.
Full text



[1] ZHAI Peng-jun, FANG Xian-wen and LIU Xiang-wei. Interaction Process Model Mining Method Based on Interface Transitions[J]. Computer Science, 2018, 45(3): 317 -321 .
[2] ZHAN Yun-jiao, WEI Ou and HU Jun. Formal Description of Requirement of Slats and Flaps Control System for DO-178C Case[J]. Computer Science, 2018, 45(4): 196 -202 .
[3] GUO Jun-xia, GUO Ren-fei, XU Nan-shan and ZHAO Rui-lian. Study on Construction of EFSM Model for Web Application Based on Session[J]. Computer Science, 2018, 45(4): 203 -207, 214 .
[4] JIA Wei, HUA Qing-yi, ZHANG Min-jun, CHEN Rui, JI Xiang and WANG Bo. Mobile Interface Pattern Clustering Algorithm Based on Improved Particle Swarm Optimization[J]. Computer Science, 2018, 45(4): 220 -226 .
[5] JIN Rui, LIU Zuo-xue. Synchronization Protocol of TDMA Ad hoc Network Based on Time Slot Alignment[J]. Computer Science, 2018, 45(6): 84 -88,110 .
[6] SUO Yan-feng, WANG Shao-jie, QIN Yu, LI Qiu-xiang, FENG Da-jun and LI Jing-chun. Summary of Security Technology and Application in Industrial Control System[J]. Computer Science, 2018, 45(4): 25 -33 .
[7] SI Nian-wen, WANG Heng-jun, LI Wei, SHAN Yi-dong and XIE Peng-cheng. Chinese Part-of-speech Tagging Model Using Attention-based LSTM[J]. Computer Science, 2018, 45(4): 66 -70, 82 .
[8] LUO Shu-yan, ZHU Yi-an, ZENG Cheng. Performance Evaluation and Optimization of Inter-cores Communication for Heterogeneous
Multi-core Processor Unit
[J]. Computer Science, 2018, 45(6A): 262 -265, 274 .
[9] ZHANG Wen-bo and HOU Xiao-rong. Estimation Algorithm of Atmospheric Light Based on Gaussian Distribution[J]. Computer Science, 2018, 45(4): 301 -305 .
[10] DU Xiu-li, GU Bin-bin, HU Xing, QIU Shao-ming and CHEN Bo. Support Similarity between Lines Based CoSaMP Algorithm for Image Reconstruction[J]. Computer Science, 2018, 45(4): 306 -311 .