命题逻辑中一类正则标准矛盾体的构造与复合
Construction and Compounding of a Class of Regular Standard Contradictions in Propositional Logic
臧珲 1何星星 1王成龙 1李莹芳 2李天瑞3
作者信息
- 1. 西南交通大学数学学院 成都 611756
- 2. 西南财经大学计算机与人工智能学院 成都 611130
- 3. 西南交通大学计算机与人工智能学院 成都 611756
- 折叠
摘要
归结原理是自动推理中一种简洁、可靠且完备的推理规则,标准矛盾体分离演绎理论是二元归结的一个延拓.矛盾体的结构非常复杂,现有的矛盾体种类和生成策略较少.针对该问题,文中基于命题逻辑的标准矛盾体分离演绎理论,首先通过复合两个或多个正则标准矛盾体,得到了生成新矛盾体的多个复合策略;其次,提出了一类特殊标准矛盾体结构——复合正则标准矛盾体,丰富了矛盾体的结构特征;然后讨论了复合得到的新矛盾体不同子句的可扩充性,进而得到相应的文字添加策略;最后,提出了矛盾体的生成算法,为进一步在计算机上实现新矛盾体的生成提供了参考.
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 separa-tion 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 strate-gies.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引用本文复制引用
基金项目
中央高校基本科研业务费专项资金(2682020ZT107)
国家自然科学基金(62106206)
教育部人文社科项目(19YJCZH048)
教育部人文社科项目(20XJCZH016)
四川省科技计划(2023YFH0066)
出版年
2024