Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (11A): 83-85.doi: 10.11896/jsjkx.200400072

• Artificial Intelligence • Previous Articles     Next Articles

Complete Contradiction and Smallest Contradiction Based on Propositional Logic

TANG Lei-ming1, BAI Mu-chen2, HE Xing-xing1, LI Xing-yu1   

  1. 1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
    2 Shanghai Naisheng Automation Co.,LTD,Shanghai 200949,China
  • Online:2020-11-15 Published:2020-11-17
  • About author:TANG Lei-ming,born in 1996,master.His main research interests include propositional logic and SAT problem.
    HE Xing-xing,born in 1982,Ph.D,associate professor,is a member of China Computer Federation.His main research interests include automated reasoning based on logic and so on.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China (61603307,61673320,61473239),Ministry of Education,Humanities and Social Science Projects(19YJCZH048,20XJCZH016),Fundamental Research Funds for the Central Universities of Ministry of Education of China (JBK2003006) and Science and Technology Project of Sichuan Province,China (2020YFG0045,2020YFG0238).

PDF (PC)

740

Abstract: Resolution is a simple,reliable and complete reasoning rule in automatic reasoning.Contradiction is an important extension of the principle of resolution.Based on the deductive reasoning of the contradiction of the propositional logic,this paperstu-dies the nature of the contradiction,puts forward the concept of the complete contradiction and the smallest contradiction and gains related properties and theorems.The main contents of these properties and theorems are as follows:1)Characteristics of each special contradiction;2)Strategies for adding literals and non-extended changes of clauses when adding a clause to the complete contradiction;3)The law of the smallest contradiction in the complete contradiction when adding clause and related literals;4)Smallest contradiction can be extended to complete contradiction.These conclusions enable complete contradiction and Smallest contradiction to be converted to each other by adding new clauses or related literals.This property provides a certain theoretical support for the further application of deductive reasoning of contradiction to computer solving.

Key words: Complete contradiction, Contradiction, Propositional logic, Smallest contradiction

CLC Number: 

  • TP181
[1] ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of theAcm,1965,12(1):23-41.
[2] HARRISON J.Handbook of practical logic and automated reasoning[M].New York:Cambridge University Press,2009:631-667.
[3] PLAISTED D A.History and Prospects for First-Order Automated Deduction[C]//International Conference on Automated Deduction.Springer Verlag,2015,9195:3-28.
[4] ROBINSON J A.Handbook of Automated Reasoning[M].New York:MIT Press,2001.
[5] BURESH-OPPENHEIM J,PITASSI T.The Complexity ofResolution Refinements[J].Journal of Symbolic Logic,2007,72(4):1336-1352.
[6] CHANG C L,RICHARD C T.Symbolic Logic and MechanicalTheorem Proving[M].New York:Academic Press,1973.
[7] RUBIN N,HARRISON M C.Another Generalization of Resolution[J].Journal of the ACM(JACM),1978,25(3):341-351.
[8] REGER G,SUDA M,VORONKOV A,et al.Selecting the selection[C]//The 8th International Joint Conference on Automated Reasoning(IJCAR2016).Coimbra,Portugal,2016:313-329.
[9] SCHULZ S,MOHRMANN M.Performance of clause selection heuristics for saturation-based theorem proving[C]//The 8th International Joint Conference on Automated Reasoning(IJCAR2016).2016:330-345.
[10] SUTCLIFFE G.The TPTP problem library and associated infrastructure:the FOF and CNF parts,v2.10.0[J].Journal of Automated Reasoning,2009,43(4):337-362.
[11] KALISZYK C,SCHULZ S,URBAN J,et al.System Descrip-tion:E.T.0.1[C]//Proceedings of the 25th International Conference on AutomatedDeduction(CADE-25).Berlin:Springer International Publishing,2015:389-398.
[12] GOZNY J,PALEO B W.Towards the compression of first-order resolution proofs by lowering unit clauses[C]//Automated Deduction(CADE-25).Berlin:Springer International Publishing,2015:356-366.
[13] 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.
[14] CAO F,XU Y,CHEN S W,et al.Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J].Chinese Journal of Southwest Jiaotong University,2020,55(2):401-408.
[15] CAO F,XU Y,WU G F,et al.Application of multi-clause dynamic deduction in Prover9[J].Chinese Computer Engineering &Science,2019,41(9):1686-1692.
[1] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[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] HE Yun, WANG Wei and LI Tong. Formal Method for Describing Software Evolution Ability Feature [J]. Computer Science, 2017, 44(7): 128-136.
[5] 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.
[6] 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.
[7] 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.
[8] 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.
[9] CHEN Yun-hua and CHEN Ping-hua. Extension Model and Strategies Generating Mechanism for Mental Fatigue Recognition [J]. Computer Science, 2015, 42(5): 300-304.
[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.
[15] YANG Bing-Ru, ZHANG Fan, HAN Yan-Ling （School of Information Engineering, Bijing University of Science and Technology, Beijing 100083）. [J]. Computer Science, 2007, 34(4): 192-195.
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.