Journal of Computer Applications ›› 2024, Vol. 44 ›› Issue (10): 3074-3080.DOI: 10.11772/j.issn.1001-9081.2023101404

• Artificial intelligence • Previous Articles     Next Articles

Contradiction separation super-deduction method and application

Feng CAO(), Xiaoling YANG, Jianbing YI, Jun LI   

  1. School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou Jiangxi 341000,China
  • Received:2023-10-19 Revised:2024-02-08 Accepted:2024-02-21 Online:2024-10-15 Published:2024-10-10
  • Contact: Feng CAO
  • About author:YANG Xiaoling, born in 2000, M. S. candidate. Her research interests include intelligent information processing, automated reasoning, first-order logic automated theorem prover.
    YI Jianbing, born in 1980, Ph. D., associate professor. His research interests include artificial intelligence.
    LI Jun, born in 1984, Ph. D., lecturer. His research interests include artificial intelligence.
  • Supported by:
    National Natural Science Foundation of China(62366017);General Research Project of Jiangxi Education Department(GJJ200818);Ganzhou Science and Technology Plan Project(GZKJ20206030);Doctorial Initiation Fund of Jiangxi University of Science and Technology(205200100060)

矛盾体分离超演绎方法及应用

曹锋(), 杨小玲, 易见兵, 李俊   

  1. 江西理工大学 信息工程学院,江西 赣州 341000
  • 通讯作者: 曹锋
  • 作者简介:曹锋(1984—),男,江西上饶人,讲师,博士,主要研究方向:智能信息处理、自动推理、一阶逻辑自动定理证明器 caofeng19840301@163.com
    杨小玲(2000—),女,江西抚州人,硕士研究生,主要研究方向:智能信息处理、自动推理、一阶逻辑自动定理证明器
    易见兵(1980—),男,江西宜春人,副教授,博士,主要研究方向:人工智能
    李俊(1984—),男,湖南益阳人,讲师,博士,主要研究方向:人工智能。
  • 基金资助:
    国家自然科学基金资助项目(62366017);江西省教育厅科研项目(GJJ200818);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金资助项目(205200100060)

Abstract:

As a common inference mechanism in the current automated theorem prover, the traditional hyper-resolution method based on binary deduction is limited to only two clauses involved in each deduction step. The separated deduction steps lead to the lack of guidance and prediction of the binary chain deduction, and its deduction efficiency needs to be improved. To improve the efficiency of deduction, in theory, the idea of multi-clause deduction was introduced into the traditional method of super-resolution, the definition and method of the contradiction separation super-deduction were proposed,which had the deduction characteristics of multi-clause, dynamics and guidance. In the implementation of the algorithm, considering that the clause participation in deduction had multi-clause and synergized characteristics, and flexibly setting the deduction conditions, a contradiction separation super-deduction algorithm with backtracking mechanism was proposed. The proposed algorithm was applied to Eprover3.1 prover, taking the International Automated Theorem Prover Competition 2023 and the most difficult problems with a difficulty rating of 1 in the TPTP (Thousands of Problems for Theorem Provers) benchmark database as the test objects. Within 300 s, the Eprover3.1 prover with the proposed algorithm solved 15 theorems more than the original Eprover3.1 prover, and the average proof time was reduced by 1.326 s with the same total number of solved theorems, and 7 theorems with the rating of 1 could be solved. The test results show that the proposed algorithm can be effectively applied to automated theorem proving in first-order logic, improving the proof capability and efficiency of automated theorem prover.

Key words: theorem prover, binary deduction, super-resolution, multi-clause deduction, contradiction separation

摘要:

作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法引入多元演绎思想,提出矛盾体分离超演绎定义和方法,它具有多元性、动态性和导向性的演绎特性;在算法实现中,考虑子句参与演绎具有多元和协同特性,并灵活设定演绎的条件,提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器,以国际自动定理证明器2023年竞赛例和TPTP(Thousands of Problems for Theorem Provers)问题库中难度系数为1的问题作为测试对象,在300 s内,应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理;当测试相同数量的定理时,所提算法的平均证明时间缩减了1.326 s,能够证明7个难度系数为1的定理。测试结果表明,所提算法能有效地应用于一阶逻辑自动定理证明,提升自动定理证明器的证明能力和效率。

关键词: 定理证明器, 二元演绎, 超归结, 多元演绎, 矛盾体分离

CLC Number: