一种基于子句稳定度的多元动态演绎算法及应用

摘要/Abstract

参考文献

Metrics

doi:10.16088/j.issn.1001-6600.2024020302

摘要： 一阶逻辑自动定理证明是人工智能领域的核心基础。启发式策略在提升一阶逻辑自动定理证明器方面备受关注,其中根据子句属性选择较优子句参与演绎为重要的研究内容。基于矛盾体分离规则,将子句中的文字分为构建标准矛盾体的文字和构建矛盾体分离式的文字,通过分析变元项、函数项、基项之间的联系与差异,本文提出一种基于稳定度的子句评估方法,其核心思想是通过所含项的组成部分度量子句参与演绎的稳定程度;同时提出一种基于子句稳定度的多元动态演绎算法(clause stability algorithm,CFA),旨在搜索当前演绎过程中的较优路径;将提出的CFA算法应用于国际著名证明器Prover9(CFA_P证明器)和国际顶尖证明器Eprover2.6(CFA_E证明器),使用CFA_P和CFA_E对国际CASC-26 FOF组竞赛例进行测试,相比原始Prover9和原始Eprover2.6,CFA_P多证明119个定理、CFA_E多证明11个定理;在证明相同定理总数的情况下,CFA_P缩短了证明时间14.76 s、CFA_E则缩短了2.54 s;针对Eprover2.6未证明的94个定理进行单独测试,CFA_E能证明27个定理,占定理总数的28.7%。实验表明,CFA算法是有效的,其在优化演绎路径方面具有良好作用,能提高一阶逻辑自动定理证明器的性能。

关键词: 一阶逻辑, 定理证明, 人工智能, 启发式策略, 多元动态演绎

Abstract: The first-order logic automated theorem proving is the core foundation of artificial intelligence. Heuristic strategies have attracted much attention in improving first-order logic automated theorem provers, and selecting effective clauses based on clause properties to participate in deduction is an important research topic. Based on the standard contradiction separation rule, the literals in clauses are divided into two parts, which are constructing standard contradictory text and constructing contradictory separation text. By analyzing the relationship and differences between variables, functions, and constants, a stability based on clause measurement method is proposed, and its core idea is to evaluate the stability of clause participating in deduction through the components of contained term. A multi-clause dynamic deduction algorithm (CFA, clause stability algorithm) is proposed based on clause stability, aiming to search for optimal paths during the current deduction process. This newly-built CFA algorithm is applied to the internationally well-known prover Prover9 and top prover Eprover2.6, and two new provers CFA_P and CFA_E are formed, respectively. The international competition problems of CASC-26 (FOF division) is tested on CFA_P and CFA_E. CFA_P can solve 119 theorems more than the original Prover9, and CFA_E outperforms Eprover2.6, solving 11 theorems more than the original Eprover2.6, and the average proof time of theorems of CFA_P and CFA_E is reduced by 14.76 s and 2.54 s, respectively with the same total number of solved theorems. Focusing on the 94 theorems unsolved by Eprover2.6, CFA_E solves 27 theorems which accounts for 28.7% in the total. The experimental results demonstrate the effectiveness of the CFA algorithm, which has good performance in optimizing deduction paths and can enhance the performance of first-order logic automated theorem prover.

Key words: first-order logic, theorem proving, artificial intelligence, heuristic strategy, multi-clause dynamic deduction

中图分类号: TP18

曹锋, 王家帆, 易见兵, 李俊. 一种基于子句稳定度的多元动态演绎算法及应用[J]. 广西师范大学学报（自然科学版）, 2024, 42(6): 164-176.

CAO Feng, WANG Jiafan, YI Jianbing, LI Jun. A Multi-clause Dynamic Deduction Algorithm Based on Clause Stability and Its Application[J]. Journal of Guangxi Normal University(Natural Science Edition), 2024, 42(6): 164-176.

[1] ROBINSON J A. A machine-oriented logic based on the resolution principle[J]. Journal of the ACM, 1965, 12(1): 23-41. DOI: 10.1145/321250.321253.
[2] SUTCLIFFE G. The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v6.4.0[J]. Journal of Automated Reasoning, 2017, 59(4): 483-502. DOI: 10.1007/s10817-017-9407-7.
[3] KOVÁCS L. Symbolic computation and automated reasoning for program analysis[C] // Integrated Formal Methods: LNCS Volume 9681. Cham: Springer, 2016: 20-27. DOI: 10.1007/978-3-319-33693-0_2.
[4] XU Y, LIU J, CHEN S W, et al. Contradiction separation based dynamic multi-clause synergized automated deduction[J]. Information Sciences, 2018, 462: 93-113. DOI: 10.1016/j.ins.2018.04.086.
[5] XU Y,LIU J, CHEN S W, et al. A novel generalization of resolution principle for automated deduction[C] // Uncertainty Modelling in Knowledge Engineering and Decision Making: Proceedings of the 12th International FLINS Conference. Singapore: World Scientific Publishing Co. Pte. Ltd., 2016: 483-488. DOI: 10.1142/9789813146976_0078.
[6] 曾国艳, 徐扬, 陈树伟, 等. 基于多属性决策的一阶逻辑子句选择方法[J/OL]. 西南交通大学学报[2024-02-03]. https://link.cnki.net/urlid/51.1277.U.20230901.1529.011.
[7] CAO F, XU Y, ZHONG J, et al. Holistic deductive framework theorem proving based on standard contradiction separation for first-order logic[C] // 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). Piscataway, NJ: IEEE, 2017: 1-5. DOI: 10.1109/ISKE.2017.8258782.
[8] 钟建, 徐扬, 陈树伟, 等. 一阶逻辑中基于稳定度的项评估方法[J]. 计算机工程, 2019, 45(11): 183-190, 197. DOI: 10.19678/j.issn.1000-3428.0054368.
[9] 林玲瑜, 曹锋, 易见兵, 等. 基于子句活跃度和复杂度的多元动态演绎算法及应用[J]. 计算机工程与科学, 2023, 45(12): 2256-2264. DOI: 10.3969/j.issn.1007-130X.2023.12.017.
[10] 曹锋, 郭海林, 易见兵, 等. 基于矛盾体分离的多元冲突演绎方法及应用[J/OL]. 武汉大学学报(理学版)[2024-02-03]. https://doi.org/10.14188/j.1671-8836.2023.0181.
[11] 曹锋, 潘世成, 易见兵, 等. 子句充分性评估的多元动态演绎算法及应用[J]. 华中科技大学学报(自然科学版),2024,52(11):153-160. DOI: 10.13245/j.hust.240468.
[12] GROZA A. Getting Started with Prover9 and Mace4[M] // GROZA A。 Modelling Puzzles in First Order Logic. Cham: Springer, 2021: 1-9. DOI: 10.1007/978-3-030-62547-4_1.
[13] SCHULZ S. System description: E 1.8[C] // Logic for Programming Artificial Intelligence and Reasoning. Berlin: Springer-Verlag, 2013: 735-743. DOI: 10.1007/978-3-642-45221-5_49.
[14] SCHULZ S,CRUANES S,VUKMIROVIĆ P. Faster,higher,stronger:E 2.3[C] // Automated Deduction-CADE 27: LNCS Volume 11716. Cham: Springer, 2019: 495-507. DOI: 10.1007/978-3-030-29436-6_29.
[15] 郝娇, 惠小静, 马硕, 等. 一阶逻辑中公理化真度研究[J]. 计算机科学, 2021, 48(11A): 669-671, 712. DOI: 10.11896/jsjkx.210200012.
[16] 曹锋, 徐扬, 吴贯锋, 等. 多元动态演绎在Prover9证明器中的应用[J]. 计算机工程与科学, 2019, 41(9): 1686-1692. DOI: 10.3969/j.issn.1007-130X.2019.09.022.
[17] 曹锋. 一种基于矛盾体分离演绎的一阶逻辑自动定理证明器研究[D]. 成都: 西南交通大学, 2020.
[18] SUTCLIFFE G. The CADE-26 automated theorem proving system competition: CASC-26[J]. AI Communications, 2017, 30(6): 419-432. DOI: 10.3233/AIC-170744.
[19] 曹钦翔, 詹博华, 赵永望. 定理证明理论与应用专题前言[J]. 软件学报, 2022, 33(6): 2113-2114. DOI: 10.13328/j.cnki.jos.006582.
[20] 孙毅, 陈哲, 冉丹, 等. 一种SCADE同步语言程序安全属性自动验证工具[J]. 小型微型计算机系统, 2022, 43(4): 858-864. DOI: 10.20009/j.cnki.21-1106/TP.2020-0941.
[21] XU R Q, LI L M, ZHAN B H. Verified interactive computation of definite integrals[C] // Automated Deduction-CADE 28: LNCS Volume 12699. Cham: Springer, 2021: 485-503. DOI: 10.1007/978-3-030-79876-5_28.

Just accepted

Online first

Just accepted

Online first

Viewed

Full text

From	Others	local

Times	22	11
Rate	67%	33%

Abstract

Just accepted	Online first	Issue

0	0	54

From	Others	local

Times	48	6
Rate	89%	11%

Cited

Web of Science	Crossref	ScienceDirect	Search for Citations in Google Scholar >>


This page requires you have already subscribed to WoS.

Shared

Discussed