命题逻辑中文字块矛盾型及子句正则矛盾体  

Literal Chunk Contradiction and Clause Regular Contradiction in Propositional Logic

作　　者：王成龙 何星星[1] 臧珲 李莹芳 王丹琛 李天瑞[4] WANG Chenglong;HE Xingxing;ZANG Hui;LI Yingfang;WANG Danchen;LI Tianrui(School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China;School of Computing and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China;Sichuan Digital Economy Research Center,Chengdu 610021,China;School of Computing and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China)

机构地区：[1]西南交通大学数学学院,成都611756 [2]西南财经大学计算机与人工智能学院,成都611130 [3]四川省数字经济研究中心,成都610021 [4]西南交通大学计算机与人工智能学院,成都611756

出　　处：《计算机科学》2024年第7期272-277,共6页Computer Science

基　　金：中央高校基本科研业务费专项资金(2682020ZT107);国家自然科学基金(62106206);教育部人文社科项目(19YJCZH048,20XJCZH016);四川省科技计划(2023YFH0066)。

摘　　要：归结原理是自动推理中一种简洁、可靠且完备的推理规则。基于矛盾体分离的自动演绎理论是归结原理的延伸,矛盾体是该理论的核心部分。由于矛盾体结构复杂且生成策略较少,因此文中提出了一种新的生成矛盾体的策略,即利用多个标准矛盾体生成文字块矛盾型,再通过添加互补矛盾集得到新的矛盾体。重点讨论了具有特殊结构的文字块矛盾型生成的矛盾体,即子句正则矛盾体的性质,这些性质说明了具有特定结构的子句正则矛盾体添加子句后仍然是矛盾体。最后,提出了矛盾体的生成算法,为在计算机上实现新的矛盾体的生成提供参考。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.

关 键 词：标准矛盾体 命题逻辑 文字块矛盾型 子句正则矛盾体 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]