Computer Science

Computer Science ›› 2022, Vol. 49 ›› Issue (6A): 109-112.doi: 10.11896/jsjkx.210700036

• Intelligent Computing • Previous Articles     Next Articles

Redundant Literals of Ternary Clause Sets in Propositional Logic

LI Jie, ZHONG Xiao-mei   

  1. School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China
    National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 610031,China
  • Online:2022-06-10 Published:2022-06-08
  • About author:LI Jie,born in 1996,postgraduate.Her main research interests include intelligent information processing and automatic reasoning.
    ZHONG Xiao-mei,born in 1984,Ph.D,lecturer.Her main research interests include logic-based automatic reasoning and so on.
  • Supported by:
    Humanity and Social Science Youth Foundation of Ministry of Education(20XJCZH016,19YJCZH048).

PDF (PC)

394

Abstract: Automatic reasoning is one of the core issues in the field of artificial intelligence.Since a large number of redundant li-terals and redundant clauses are generated in the process of automatic reasoning based on resolution,the resolution efficiency will be affected.It is of great significance to eliminate redundant literals and redundant clauses in the clause set.In propositional logic,according to the related concepts and properties of necessary literals,useful literals and useless literals,this paper classifies and gives the judgment methods of redundant literals in some ternary clause sets,and explains these judgment methods through specific examples.

Key words: Necessary literals, Propositional logic, Ternary clause sets, Useful literals, Useless literals

CLC Number: 

  • TP181
[1] LIBERATORE P.Redundancy in logic I:CN propositional formulae[J].Artificial Intelligence,2005,163(2):203-232.
[2] FOURDRINO Y O,ÉRIC G,MAZURE B.Eliminating Redundant Clauses in SAT Instances[C]//Proceedings of InternationalConference on Integration of Ai and Or Techniques in Constraint Programming for Combinatorial Optimization Problems.DBLP,2007:71-83.
[3] HEULE M,M JARVISALO,BIERE A.Efficient CNF simplification based on binary implication graphs[C]//Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing.Springer Berlin Heidelberg,2011.
[4] ZHAI C H,QIN K Y.Redundancy clause and redundancy literal of propositional logic[J].Computer Science,2013,40(5):48-50.
[5] TANG SH H.Research redundancy of set of clauses in propositional logic[D].Chengdu:Southwest Jiaotong University,2014.
[6] DENG P.The classification of set of clauses in propositionallogic[D].Chengdu:Southwest Jiaotong University,2015.
[7] RINALDI D,SCHUSTER P,WESSEL D.Eliminating disjunc-tions by disjunction elimination[J].Bulletin of Symbolic Logic,2017,23(2):181-200.
[8] LIU T.Research on redundant clauses and redundant literals in propositional logic[D].Chengdu:Southwest Jiaotong Univer-sity,2019.
[9] ING X R,XU Y,CHEN Z S.Novel preprocessing clause elimination methods for propositional SAT solvers[J].Computer Integrated Manufacturing Systems,2020,26(8):2133-2142.
[10] LIU X H.Automatic reasoning based on resolution method[M].Science Press,1994.
[11] SHI CH Y,WANG J X.Mathematical logic and set theory[M].Beijing:Tsinghua University Press,2000.
[12] HEULE M,RVISALO M,LONSING F.Clause elimination for SAT and QSAT[J].Journal of Artificial Intelligence Research,2015,53(1):127-168.
[13] HEULE M,JRVISALO M,BIERE A.Clause Elimination Pro-cedures for CNF Formulas[C]//Logic for Programming,Artificial Intelligence,& Reasoning-international Conference,Lpar-17.DBLP,2010:357-371.
[14] LIU J,ZHOU H H.New algebraic logic reduction method for boolean formula[J].Computer Science,2020,47(5):32-37.
[15] WANG G J.Introduction to mathematical logic and resolution principle[M].Science Press,2003:17-22.
[1] 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.
[2] LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259.
[3] 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.
[4] 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.
[5] 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.
[6] 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.
[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.
[8] 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.
[9] GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203.
[10] LIU Hong-lan,GAO Qing-sh,YANG Bing-ru. Set Algebra is Semantic Interpretation for Classical Formal System of Propositional Calculus [J]. Computer Science, 2010, 37(9): 194-197.
[11] TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT [J]. Computer Science, 2010, 37(5): 184-186.
[12] . [J]. Computer Science, 2008, 35(9): 230-232.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.