命题逻辑中一种矛盾体生成新方法*黎兴玉1,何星星1,马雪1,李莹芳2(1.西南交通大学数学学院,四川成都610031;2.西南财经大学计算机与人工智能学院,四川成都611130)摘要:人工智能是用计算机来模拟人的某些思维过程和智能行为的学科。自动推理中的归结原理是一种简洁、可靠且完备的推理规则。矛盾体的动态多子句协同演绎理论不仅是归结原理的重要延拓,而且具有较高的推理演绎效率。由于矛盾体的结构复杂、生成策略较少,因此在矛盾体的动态演绎可靠性和完备性的基础上,提出复合2个或多个矛盾体的部分子句的不同策略,为矛盾体的构造提供了一种有效的方法。关键词:命题逻辑;矛盾体;矛盾体的复合性质;不可满足性中图分类号:TP181文献标志码:Adoi:10.3969/j.issn.1007-130X.2023.06.021AnewcontradictiongenerationmethodinpropositionallogicLIXing-yu1,HEXing-xing1,MAXue1,LIYing-fang2(1.SchoolofMathematics,SouthwestJiaotongUniversity,Chengdu610031;2.SchoolofComputingandArtificialIntelligence,SouthwesternUniversityofFinanceandEconomics,Chengdu611130,China)Abstract:ArtificialIntelligence(AI)isadisciplinethatsimulatessomethinkingprocessesandintel-ligentbehaviorsofhumanbeingswithcomputers.Theresolutionprincipleinautomaticreasoningisaconcise,reliableandcompletereasoningrule.Thecontradictionseparationbaseddynamicmulti-clausesynergizedautomateddeductionisnotonlyacrucialextensionofresolutionprinciple,butalsohashigh-erdeductiveefficiency.Duetothecomplexstructureofcontradictionsandfewergenerationstrategies,thepaperproposesdifferentstrategiesforcompoundingthepartialclausesoftwoormorecontradictionsonthebasisofthedynamicdeductionreliabilitytheoremandcompletenesstheoremofcontradictions,whichprovidesaneffectivemethodfortheconstructionofcontradictions.Keywords:propositionallogic;contradiction;compoundpropertiesofcontradictions;unsatisfiability1引言自17世纪末叶,德国数学家Leibniz创立了数理逻辑以来,广大研究人员就开启了探索用计算机模拟人类证明命题逻辑定理的推理过程,并随着《逻辑理论机》的面世,自动定理证明ATP(Auto-maticTheoremProver)[1]进入了人们的视野。自动定理证明在软硬件领域[2]、专家系统[3]、问答系统[4]、语义网、知识图谱等知识表示和知识推理领域[5],以及...
