命题逻辑中一类正则标准矛盾体的构造与复合  

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

作　　者：臧珲 何星星[1] 王成龙 李莹芳 李天瑞[3] ZANG Hui;HE Xingxing;WANG Chenglong;LI Yingfang;LI Tianrui(School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China;School of Computer and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China;School of Computer and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China)

机构地区：[1]西南交通大学数学学院,成都611756 [2]西南财经大学计算机与人工智能学院,成都611130 [3]西南交通大学计算机与人工智能学院,成都611756

出　　处：《计算机科学》2024年第1期295-300,共6页Computer Science

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

摘　　要：归结原理是自动推理中一种简洁、可靠且完备的推理规则,标准矛盾体分离演绎理论是二元归结的一个延拓。矛盾体的结构非常复杂,现有的矛盾体种类和生成策略较少。针对该问题,文中基于命题逻辑的标准矛盾体分离演绎理论,首先通过复合两个或多个正则标准矛盾体,得到了生成新矛盾体的多个复合策略;其次,提出了一类特殊标准矛盾体结构——复合正则标准矛盾体,丰富了矛盾体的结构特征;然后讨论了复合得到的新矛盾体不同子句的可扩充性,进而得到相应的文字添加策略;最后,提出了矛盾体的生成算法,为进一步在计算机上实现新矛盾体的生成提供了参考。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.

关 键 词：命题逻辑 标准矛盾体 复合正则标准矛盾体 复合策略 文字添加策略 

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