Computer Science

Computer Science ›› 2024, Vol. 51 ›› Issue (1): 295-300.doi: 10.11896/jsjkx.230600009

• Artificial Intelligence • Previous Articles     Next Articles

Construction and Compounding of a Class of Regular Standard Contradictions in Propositional Logic

ZANG Hui1, HE Xingxing1, WANG Chenglong1, LI Yingfang2, LI Tianrui3   

  1. 1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
    2 School of Computer and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China
    3 School of Computer and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China
  • Received:2023-05-31 Revised:2023-09-25 Online:2024-01-15 Published:2024-01-12
  • About author:ZANG Hui,born in 2000,master.Her main research interests include compo-site of contradictions and graph depth learning.
    LI Yingfang,born in 1985,Ph.D,asso-ciate professor.Her main research in-terests include intelligent information processing,intelligent decision making and control,measurement and analysis of uncertain information,reasoning and problem solving and so on.
  • Supported by:
    Fundamental Research Funds for the Central Universities of Ministry of Education of China(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)

1456

Abstract: The resolution principle is a brief,reliable and complete inference rule in automated reasoning and the deductive theory of standard contradiction separation is an extension of binary resolution.Since the structure of the standard contradiction is very complex and there are few existing contradiction types and generation strategies,this paper first obtains multiple compound stra-tegies for generating new contradictions by compounding two or more contradictions based on the standard contradiction separation deduction theory in propositional logic.Then a kind of special standard contradiction structure,i.e.,composite regular stan-dard contradiction,is put forward to enrich the structural features of contradictions.Furthermore,the expandability of the diffe-rent clauses of the new contradictions obtained by compounding is discussed,which leads to corresponding literals adding strategies.Finally,algorithms for generating contradictions are proposed to provide a reference for further implementing the generation of new contradictions on computers.

Key words: Propositional logic, Standard contradiction, Composite regular standard contradiction, Composite strategy, Literals adding strategy

CLC Number: 

  • TP181
[1]NICK.A Brief History of Artificial Intelligence[J].ScienceWriting,2018,1(3):96.
[2]ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of the ACM(JACM),1965,12(1):23-41.
[3]HERBRAND J.Researches in the theory of demonstration[C]//From Frege to Goedel:a source book in Mathematical Logic,Hoard University Press.1930:525-581.
[4]BECKERT B,HAHNLE R.Reasoning and verification:State of the art and current trends[J].IEEE Intelligent System,2014,29(1):20-29.
[5]WITHERELL P,KRISHNAMURTY S,GROSSE I R,et al.Improved knowledge management through first-order logic in engineering design ontologies[J].Artificial Intelligence for Engineering Design Analysis & Manufacturing,2010,24(2):245-257.
[6]WANG Z,YAN S,WANG H,et al.An overview of microsoft deep qa system on stanford web questions benchmark[R].Microsoft Research,2014.
[7]LIEBIG T.Reasoning with OWL-system support and insights
[M].Germany:Springer Berlin Heidelberg,2013.
[8]MARIA F,LUC D R,WOLFGANG B.Artificial Intelligence in a historical perspective[J].AI Communications,2014,27(1):87-102.
[9]CEZARY K,JOSEF U.MizAR 40 for Mizar 40[J].Journal of Automated Reasoning,2015,55(3):245-256.
[10]CEZARY K,JOSEF U.Learning-Assisted Automated Reaso-ning with Flyspeck[J].Journal of Automated Reasoning,2014,53(2):173- 213.
[11]WOS L,ROBINSON G A,CARSON D F.Efficiency and Completeness of the Set of Support Strategy in Theorem Proving[J].Journal of the ACM,1965,12(4):536-541.
[12]SLAGLE J R.Automatic theorem proving with renamable and semantic resolution[J].Journal of the ACM,1983,14(4):687-697.
[13]LOVELAND D W.A linear format for resolution[C]//Procee-dings of Symposium on Automatic Demonstration.1970:163-190.
[14]BOYER R S.Locking:A Restriction of Resolution(Disserta-tion),also ATP-05[M].University of Texas at Austin,1971.
[15]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.
[16]TANG L M,BAI M C,HE X X,et al.Complete contradiction and smallest contradiction based on propositional logic[J].Computer Science,2020,47(S2):83-85,105.
[17]LI X Y,HE X X,MA X,et al.A new method of generating contradictions in propositional logic[J].Computer-Engineering & Science,2023,45(6):1134-1140.
[18]LIU X H.Automatic Reasoning Based on the Reduced Method[M].Beijing:Science Press,1994.
[19]XU Y,LIU J,CHEN S,et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462:93-113.
[20]HE X X,LI Y F,FENG Y H.On structures of regular standardcontradictions in propositional logic[J].Information Sciences,2022,586:261-278.
[1] LIU Lingrong, CHEN Shuwei, JIANG Shipan. L-type Redundancy Property in Propositional Logic [J]. Computer Science, 2023, 50(6A): 220600013-5.
[2] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[3] 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.
[4] 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.
[5] 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.
[6] 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.
[7] 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.
[8] 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.
[9] 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.
[10] 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.
[11] GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203.
[12] 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.
[13] TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT [J]. Computer Science, 2010, 37(5): 184-186.
[14] . [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.