含等词子句集上的子句冗余性原理

宁欣然; 吴贯锋; 徐扬

doi:10.3969/j.issn.0258-2724.20240586

含等词子句集上的子句冗余性原理

doi: 10.3969/j.issn.0258-2724.20240586

宁欣然^1,,
吴贯锋^2, ,,
徐扬²

1.
西南民族大学计算机与人工智能学院，四川成都 610225
2.
西南交通大学数学学院，四川成都 611752

基金项目: 国家自然科学基金项目（62106206）；中央高校基本科研业务费专项资金（ZYN2024054）

详细信息

作者简介:
宁欣然（1990—），女，讲师，博士，研究方向为自动推理，E-mail：ningxinran99@foxmail.com

通讯作者:
吴贯锋（1986—），男，工程师，博士，研究方向为自动推理、并行计算，E-mail： wgf1024@swjtu.edu.cn

中图分类号: TP391.1
计量
- 文章访问数: 36
- HTML全文浏览量: 21
- PDF下载量: 10
- 被引次数: 0
出版历程
- 收稿日期: 2024-11-12
- 修回日期: 2025-03-11
- 网络出版日期: 2025-12-19

Principle for Clause Redundancy in Clause Sets with Equality

NING Xinran^1
,,
WU Guanfeng^{2
, ,},
XU Yang²

1.
College of Computer Science and Artificial Intelligence, Southwest Minzu University, Chengdu 610225, China
2.
School of Mathematics, Southwest Jiaotong University, Chengdu 611752, China

摘要

摘要:
为探讨含等词子句集中的子句冗余性问题，提出一种新的子句冗余性判定方法——等词蕴涵模归结原理（EIMR）. 首先，分析一阶逻辑定理证明器在化简过程中对冗余子句的处理需求，指出蕴涵模归结原理无法直接应用于含等词子句集的不足；其次，通过结合平展操作与归结方法，定义适用于含等词子句集的等词蕴涵模归结原理，详细证明其理论可靠性，并阐明该原理在冗余子句判定中的具体作用；随后，以EIMR为基础，将命题逻辑和不含等词子句集上的子句消去方法扩展至含等词子句集，定义等词归结不对称恒真子句和等词归结包含子句，并证实这些扩展方法的有效性；最后，利用该原理进一步验证主流一阶逻辑定理证明器在预处理阶段中谓词消去方法的可靠性. 研究结果表明，等词蕴涵模归结原理为含等词子句集上的子句冗余性研究提供了理论依据，并扩展了现有子句消去方法的适用范围.
- 一阶逻辑定理证明 /
- 等词蕴涵模归结原理 /
- 子句冗余性 /
- 子句消去方法
Abstract:
To investigate clause redundancy in clause sets with equality, a determination method for clause redundancy, namely equality implication modulo resolution (EIMR) principle, was proposed. First, the need for handling redundant clauses during the simplification process in a first-order logic theorem prover was analyzed, and the limitations of implication modulo resolution principle in handling clause sets with equality were identified. By integrating flattening and resolution methods, the EIMR principle applicable to clause sets with equality was defined. The reliability of the principle was proven, and the specific role of the principle in the determination of redundant clauses was clarified. Subsequently, on the basis of EIMR, the clause elimination methods from propositional logic and clause sets without equality were extended to clause sets with equality. Asymmetric tautologies and subsumption clauses of equality resolution were defined, and the effectiveness of these methods was demonstrated. Finally, the reliability of predicate elimination preprocessing methods in mainstream first-order theorem provers was validated using the EIMR principle. The results indicate that EIMR provides a theoretical basis for clause redundancy studies in clause sets with equality and extends the applicable scope of existing clause elimination methods.
- first-order logic theorem proving /
- equality implication modulo resolution principle /
- clause redundancy /
- clause elimination method

HTML全文

参考文献(34)

[1]	MCCUNE W. Prover9 and Mace4[EB/OL]. http://www.cs.unm.edu/ ~ mccune/Prover9, 2005-2010.
[2]	JAKUBUV J, CHVALOVSKY K, GOERTZEL Z, et al. MizAR 60 for Mizar 50[EB/OL]. (2023-03-23). https://arxiv.org/abs/2303.06686
[3]	WEIDENBACH C, DIMOVA D, FIETZKE A, et al. SPASS version 3.5[C]//Automated Deduction–CADE-22. Berlin: Springer, 2009: 140-145.
[4]	WITHERELL P, KRISHNAMURTY S, GROSSE I R, et al. Improved knowledge management through first-order logic in engineering design ontologies[J]. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 2010, 24(2): 245-257. doi: 10.1017/S0890060409990096
[5]	LIU H M, LIU J, CUI L Y, et al. LogiQA 2.0: an improved dataset for logical reasoning in natural language understanding[J]. IEEE/ACM Transactions on Audio, Speech, and Language Processing, 2023, 31: 2947-2962. doi: 10.1109/TASLP.2023.3293046
[6]	BECKERT B, HÄHNLE R. Reasoning and verification: state of the art and current trends[J]. IEEE Intelligent Systems, 2014, 29(1): 20-29. doi: 10.1109/MIS.2014.3
[7]	FLÜGEL S, GLAUER M, NEUHAUS F, et al. When one logic is not enough: integrating first-order annotations in OWL ontologies[J/OL]. Semantic Web, 2024: 1-16. [2024-10-21]. https://ouci.dntb.gov.ua/en/works/7AKLooal/
[8]	HERRON D, JIMENEZ-RUIZ E, WEYDE T. On the benefits of OWL-based knowledge graphs for neural-symbolic systems[C]//Proceedings of the 17th International Workshop on Neural-Symbolic Learning and Reasoning, Siena: [s.n.], 2023: 327-335
[9]	WANG Z H, YAN S Q, WANG H M, et. al. An overview of Microsoft Deep QA System on Stanford WebQuestions benchmark[R]. [S.l.]: Microsoft Research Technical, 2014: 1-8.
[10]	RAMOS L. Semantic Web for manufacturing, trends and open issues Toward a state of the art[J]. Computers & Industrial Engineering, 2015, 90: 444-460.
[11]	SUDA M. Vampire with a brain is a good ITP hammer[C]//Frontiers of Combining Systems. Cham: Springer, 2021: 192-209.
[12]	SCHULZ S. E–a brainiac theorem prover[J]. Ai Communications, 2002, 15(2/3): 111-126.
[13]	SUBBARAYAN S, PRADHAN D K. NiVER: non-increasing variable elimination resolution for preprocessing SAT instances[M]//Theory and Applications of Satisfiability Testing. Berlin: Springer, 2005: 276-291.
[14]	KALISZYK C, URBAN J. MizAR 40 for Mizar 40[J]. Journal of Automated Reasoning, 2015, 55: 245-256. doi: 10.1007/s10817-015-9330-8
[15]	RIAZANOV A, VORONKOV A. The design and implementation of VAMPIRE[J]. AI Communications, 2002, 15(2/3): 91-110.
[16]	KIESL B, SUDA M. A unifying principle for clause elimination in first-order logic[C]//Automated Deduction–CADE 26. Cham: Springer, 2017: 274-290.
[17]	NING X R, XU Y, WU G F, et al. Set-blocked clause and extended set-blocked clause in first-order logic[J]. Symmetry, 2018, 10(11): 553. doi: 10.3390/sym10110553
[18]	LIU Q H, XU Y, HE X X. Attention recurrent cross-graph neural network for selecting premises[J]. International Journal of Machine Learning and Cybernetics, 2022, 13(5): 1301-1315. doi: 10.1007/s13042-021-01448-9
[19]	HOLDEN E K, KOROVIN K. Graph sequence learning for premise selection[J]. Journal of Symbolic Computation, 2025, 128: 102376. doi: 10.1016/j.jsc.2024.102376
[20]	KHASIDASHVILI Z, KOROVIN K. Predicate elimination for preprocessing in first-order theorem proving[C]//Theory and Applications of Satisfiability Testing–SAT 2016. Cham: Springer, 2016: 361-372.
[21]	MCCUNE W. Release of Prover9[R]. Colorado: Mile High Conference on Quasigroups, Loops and Nonassociative Systems, 2005.
[22]	宁欣然, 徐扬, 何星星. 一阶逻辑中的扩展子句消去原则[J]. 西南交通大学学报, 2020, 55(3): 588-595. NING Xinran, XU Yang, HE Xingxing. Extended unifying principle of clause elimination in first-order logic[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 588-595.
[23]	刘清华, 李瑞杰, 朱绪胜, 等. 基于符号权重的一阶逻辑前提选择方法[J]. 西南交通大学学报, 2023, 58(3): 704-710. LIU Qinghua, LI Ruijie, ZHU Xusheng, et al. First-order logical premise selection method based on symbol weight[J]. Journal of Southwest Jiaotong University, 2023, 58(3): 704-710.
[24]	王霞, 王恪铭, 徐扬, 等. 基于形式化方法的平交道口控制系统安全设计[J]. 西南交通大学学报, 2023, 58(1): 109-116. WANG Xia, WANG Keming, XU Yang, et al. Safety design of level crossing control system based on formal method[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 109-116.
[25]	SUTCLIFFE G. The TPTP problem library and associated infrastructure[J]. Journal of Automated Reasoning, 2017, 59(4): 483-502. doi: 10.1007/s10817-017-9407-7
[26]	FITTING M. First-order logic and automated theorem proving[M]. New York: Springer, 1996.
[27]	KIESL B, SUDA M, SEIDL M, et al. Blocked clauses in first-order logic[J]//EPiC Series in Computing, 2017, 46: 31-12.
[28]	REEVES J E, HEULE M J H, BRYANT R E. Preprocessing of propagation redundant clauses[J]. Journal of Automated Reasoning, 2023, 67(3): 31. doi: 10.1007/s10817-023-09681-3
[29]	ALTMANNINGER J, REBOLA PARDO A. Frying the egg, roasting the chicken: unit deletions in DRAT proofs[C]//Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. New Orleans: ACM, 2020: 61-70.
[30]	JÄRVISALO M, HEULE M J H, BIERE A. Inprocessing rules[M]//Automated Reasoning. Berlin: Springer, 2012: 355-370.
[31]	HEULE M, JARVISALO M, BIERE A. Covered clause elimination[EB/OL]. [2024-09-25]. https://doi.org/10.48550/arXiv.1011.5202.
[32]	刘叙华. 基于归结方法的自动推理[M]. 北京: 科学出版社, 1994.
[33]	LIEBIG T. Reasoning with OWL–system support and insights[R]. Munich: Ulm University, 2006.
[34]	HEULE M, JÄRVISALO M, BIERE A. Clause elimination procedures for CNF formulas[M]//Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer, 2010: 357-371.