Computer Science

Computer Science ›› 2024, Vol. 51 ›› Issue (7): 272-277.doi: 10.11896/jsjkx.230500237

• Artificial Intelligence • Previous Articles     Next Articles

Literal Chunk Contradiction and Clause Regular Contradiction in Propositional Logic

WANG Chenglong1, HE Xingxing1, ZANG Hui1, LI Yingfang2, WANG Danchen3, LI Tianrui4   

  1. 1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
    2 School of Computing and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China
    3 Sichuan Digital Economy Research Center,Chengdu 610021,China
    4 School of Computing and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China
  • Received:2023-05-31 Revised:2023-10-12 Online:2024-07-15 Published:2024-07-10
  • About author:WANG Chenglong,born in 1999,master.His main research interests include propositional logic and deep learning.
    LI Yingfang,born in 1985,Ph.D,asso-ciate professor.Her main research interests include intelligent information processing,intelligent decision making and control,measurement and analysis of uncertain information,reasoning and problem solving and so on.
  • Supported by:
    Basic Research Funds for Central Universities(2682020ZT107),National Natural Science Foundation of China(62106206),Humanities and Social Sciences Project of Ministry of Education(19YJCZH048,20XJCZH016) and Science and Technology Program of Sichuan Province(2023YFH0066).

PDF (PC)

450

Abstract: The resolution principle is a concise,reliable,and complete inference rule in automatic reasoning.The contradiction sepa-ration-based dynamic multi-clause synergized automated deduction is an extension of the resolution principle,and the contradiction is the theory's core part.Due to the complex structure of the contradiction and the few generation strategies,a new strategy for generating the contradiction is proposed,i.e.,multiple standard contradictions are used to generate the literal chunk contradiction.Then,a new contradiction is obtained by adding complementary contradiction sets.The focus is on the nature of the contradiction generated by the literal chunk contradiction with a special structure,i.e.,the clause regular contradiction,which shows that the clause regular contradiction with a specific structure is still a contradiction after adding the clause.Finally,an algorithm for generating contradiction is proposed,which provides a reference for generating new contradictions on computers.

Key words: Standard contradiction, Propositional logic, Literal chunk contradiction, Clause regular contradiction

CLC Number: 

  • TP181
[1]BECKERT B,HAHNLE R.Reasoning and verification:State ofthe art and current trends[J].IEEE Intelligent Systems,2014,29(1):20-29.
[2]WITHERELL P,KRISHNAMURTY S,GROSSE I R,et al.Improved knowledge management through first-order logic in engineering design ontologies[J].AI EDAM,2010,24(2):245-257.
[3]WANG Z,YAN S,WANG H,et al.An overview of microsoft deep qa system on stanford webquestions benchmark[J/OL].[2018-09-15].https://www.microsoft.com/en-us/research/publication/an-overview-of-microsoft-deep-qa-system-on-stanford-webquestionsbenchmark,2014.
[4]BIBEL W.Artificial Intelligence in a historical perspective[J].AI Communications,2014,27(1):87-102.
[5]KALISZYK C,URBAN J.Mizar 40 for mizar 40[J].Journal of Automated Reasoning,2015,55(3):245-256.
[6]KALISZYK C,URBAN J.Learning-assisted automated reaso-ning with Flyspeck[J].Journal of Automated Reasoning,2014,53:173-213.
[7]ZOU L,LIU D,ZHENG H L.(α,β)-Generalized Lock Resolution of Intuitionistic Fuzzy Logic[J].Journal of Frontiers of Computer Science and Technology,2015,9(8):1004-1009.
[8]MENG J.Resolution-based Automated Reasoning in Linguistic2-Tuple[D].Liaoning:Liaoning Normal University,2018.
[9]LI X N.The Study of (α,β)-Linear Resolution Method for Intui-tionistic Fuzzy Logic[D].Liaoning:Liaoning normal University,2017.
[10]XU Y,LIU J,CHEN S W,et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462:93-113.
[11]CAO F,XU Y,LIU J,et al.CSE_E 1.0:Anintegrated automated theorem prover for first-order logic[J].Symmetry,2019,11(9):1142.
[12]CAO F,XU Y,CHEN S W,et al.A contradiction separation dynamic deduction algorithm based on optimized proof search[J].International Journal of Computational Intelligence Systems,2019,12(2):1245-1254.
[13]CAO F,XU Y,LIU J,et al.A multi-clause dynamic deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2021,566:281-299.
[14]ZHONG J,XU Y,CAO F.A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic[J].International Journal of Computational Intelligence Systems,2020,13(1):672-680.
[15]LIU P Y,XU Y,LIU J,et al.Fully reusing clause deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2023,622:337-356.
[16]TANG L M,BAI M C,HE X X,et al.Complete contradictionand smallest contradiction based on propositional logic[J].Computer Science,2020,47(S2):83-85,105.
[17]HE X X,LI Y F,FENG Y F.On structures of regular standard contradictions in propositional logic[J].Information Sciences,2022,586:261-278.
[18]LI X Y,HE X X,MA X,et al.A new contradiction generation method in propositional logic[J].Computer Engineering & Science,2023,45(6):1134-1140.
[19]LIU X H.Automatic Reasoning Based on the Reduced Method[M].Beijing:Science Press,1994.
[1] ZANG Hui, HE Xingxing, WANG Chenglong, LI Yingfang, LI Tianrui. Construction and Compounding of a Class of Regular Standard Contradictions in Propositional Logic [J]. Computer Science, 2024, 51(1): 295-300.
[2] LIU Lingrong, CHEN Shuwei, JIANG Shipan. L-type Redundancy Property in Propositional Logic [J]. Computer Science, 2023, 50(6A): 220600013-5.
[3] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[4] 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.
[5] 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.
[6] 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.
[7] 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.
[8] 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.
[9] 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.
[10] 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.
[11] 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.
[12] GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203.
[13] 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.
[14] TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT [J]. Computer Science, 2010, 37(5): 184-186.
[15] . [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.