计算机科学

计算机科学 ›› 2026, Vol. 53 ›› Issue (7): 186-194.doi: 10.11896/jsjkx.250400099

• 人工智能 • 上一篇    下一篇

基于演绎体的多元动态演绎算法

周杰1,3, 邹玮刚2,3, 曹锋1,3, 易见兵1,3   

  1. 1 江西理工大学信息工程学院 江西 赣州 341000
    2 江西理工大学理学院 江西 赣州 341000
    3 多维智能感知与控制江西省重点实验室 江西 赣州 341000
  • 收稿日期:2025-04-21 修回日期:2025-08-17 出版日期:2026-07-15 发布日期:2026-07-10
  • 通讯作者: 邹玮刚(42587617@qq.com)
  • 作者简介:(jxustzj@163.com)
  • 基金资助:
    国家自然科学基金(62366017,62366016);江西省教育厅项目(GJJ200818,GJJ190462);赣州市科技计划(GZKJ20206030);江西理工大学博士启动基金(205200100060)

Multi-clause Dynamic Deduction Algorithm Based on Deduction Body

ZHOU Jie1,3, ZOU Weigang2,3, CAO Feng1,3, YI Jianbing1,3   

  1. 1 School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou,Jiangxi 341000,China
    2 School of Science,Jiangxi University of Science and Technology,Ganzhou,Jiangxi 341000,China
    3 Jiangxi Province Key Laboratory of Multidimensional Intelligent Perception and Control,Ganzhou,Jiangxi 341000,China
  • Received:2025-04-21 Revised:2025-08-17 Published:2026-07-15 Online:2026-07-10
  • About author:ZHOU Jie,born in 2001,postgraduate.His main research interest is automated reasoning.
    ZOU Weigang,born in 1976,master,associate professor.His main research interests include intelligent information processing and digital image proces-sing.
  • Supported by:
    National Natural Science Foundation of China(62366017,62366016),Projects of Jiangxi Provincial Department of Education(GJJ200818,GJJ190462),Ganzhou Science and Technology Plan(GZKJ20206030) and Doctoral Initiation Fund of Jiangxi University of Science and Technology(205200100060).

PDF (PC)

20

摘要： 路径信息对后续演绎具有协同推理作用,探讨演绎路径有效的表示及应用方法具有重要的学术意义。针对多元演绎过程,提出了演绎体的定义,用于系统性地描述每个多元演绎步骤的演绎路径信息;根据演绎过程中剩余文字的不同,提出了演绎体的分类方法、表示方法及其演绎方法,该方法能根据多元演绎过程生成不同类型的演绎体并进行有效存储,在后续的多元演绎中能利用演绎体对剩余文字进行进一步消元;基于该方法提出了基于演绎体的多元动态演绎算法,通过权重排序选择单元子句及候选子句参与演绎,将参与演绎的子句构建标准矛盾体并评估其有效性,若为有效演绎,则构建演绎体,若为无效演绎,则通过回溯机制重新调整参与演绎的子句,生成矛盾体分离式后,使用演绎体进一步约简或丰富演绎搜索路径。将该算法应用于国际顶尖的Eprover3.2证明器中,以2023年和2024年国际自动定理证明器FOF组竞赛例为测试对象,在测试时间300 s内,加入该算法的Eprover3.2比原始Eprover3.2多证明了14个问题;以TPTP问题库中rating为1的问题为测试对象,加入了该算法的Eprover3.2能证明出7个其他所有证明器都无法证明的问题。实验结果表明,基于演绎体的多元动态演绎算法能有效应用于一阶逻辑自动定理证明。

关键词: 路径信息, 协同推理, 演绎路径, 多元演绎, 定理证明

Abstract: Given the synergized reasoning effect of path information on subsequent deduction,exploring effective representation and application methods of deduction paths holds significant academic value.In response to the multi-clause deduction process,this paper proposes the definition of deduction body,which systematically describes the deduction path information at each step of multi-clause deduction.According to the variation of remaining literals during deduction,a classification method,a representation method and a deduction method for deduction body are introduced.This method can generate and store different types of deduction bodies according to the deduction process,and utilize them to further eliminate the remaining literals in subsequent deduction steps.Based on this method,a multi-clause dynamic deduction algorithm grounded in deduction body is presented,in which unit clauses and candidate clauses are selected for deduction through weight-based ranking.The participating clauses are used to construct standard contradiction,whose effectiveness is then evaluated.If the deduction is valid,a deduction body is constructed;if the deduction is invalid,the clauses involved in the deduction are readjusted through a backtracking mechanism.After generating a standard contradiction separation clause,the deduction body is used to further reduce or enrich the deductive search path.This algorithm is applied in the internationally leading theorem prover Eprover3.2 and tested on benchmark FOF division problems from the 2023 and 2024 international automated theorem provers competitions.Within the testing time of 300 seconds,Eprover3.2with the proposed algorithm both solves 14 more problems than the original Eprover3.2 respectively.Furthermore,the problems from TPTP(Thousands of Problems for Theorem Provers) problem library with a rating of 1 are also used as a test object,Eprover3.2 with proposed algorithm solves 7 problems that can not be solved by all other provers.Experimental results demonstrate that the multi-clause dynamic deduction algorithm based on deduction body can be effectively applied to first-order logic automated theorem proving.

Key words: Path information, Synergized reasoning, Deduction path, Multi-clause deduction, Theorem proving

中图分类号: 

  • TP181
[1]MOGHADDAM G I,PADMANABHAN R,ZHANG Y.Automated reasoning with power maps[J].Journal of Automated Reasoning,2020,64(4):689-697.
[2]FROM A H,SCHLICHTKRULL A,VILLADSEN J.A sequent calculus for first-order logic formalized in Isabelle/HOL[J].Journal of Logic and Computation,2023,33(4):818-836.
[3]COHEN E.First-order verification of cryptographic protocols[J].Journal of Computer Security,2003,11(2):189-216.
[4]KOVÁCS L.Symbolic computation and automated reasoning for program analysis[C]//International Conference on Integrated Formal Methods.Cham:Springer,2016:20-27.
[5]GULLER D.Technical foundations of a DPLL-based SAT sol-ver for propositional gödel logic[J].IEEE Transactions on Fuzzy Systems,2016,26(1):84-100.
[6]ROBINSON J A.Automatic deduction with hyper-resolution[J].International Journal of Computing and Mathematics,1965,1:227-234.
[7]KOVÁCS L,VORONKOV A.First-order theorem proving and Vampire[C]//Proceedings of the Computer Aided Verification:25th International Conference.Cham:Springer,2013:1-35.
[8]BIERE A,DRAGAN I,KOVÁCS L,et al.Experimenting with SAT solvers in vampire[C]//Mexican International Conference on Artificial Intelligence.Switzerland:Springer-Verlag,2014:431-442.
[9]SCHULZ S,CRUANES S,VUKMIROVIĆ P.Faster,higher,stronger:E 2.3[C]//Proceedings of the 2019 Automated Deduction-CADE 27:27th International Conference on Automated Deduction.Cham:Springer,2019:495-507.
[10]SCHULZ S.System description:E 1.8[C]//International Conference on Logic for Programming Artificial Intelligence and Reasoning.Berlin:Springer-Verlag,2013:735-743.
[11]MCCUNE W.Release of prover9[C]//Mile High Conference on Quasigroups,Loops and Nonassociative Systems,Denver,Colorado.2005.
[12]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.
[13]ZENG G Y,CHEN S W,LIU J,et al.A complementary ratio based clause selection method for contradiction separation dynamic deduction[J].Knowledge-Based Systems,2024,284:111238.
[14]CAO F,PAN S C,YI J B,et al.Multi-clause dynamic deduction algorithm based on clause adequacy evaluation and its application[J].Journal of Huazhong University of Science and Technology(Natural Science Edition),2024,52(11):153-160.
[15]JIANG S P,CHEN S W,ZENG G Y.Strategy of invalid clause elimination in first-order logic theorem prover[J].Journal of Computer Applications,2024,44(3):677-682.
[16]CAO F,GUO H L,YI J B,et al.A multi-clause conflict deduction method based on contradiction separation and its application[J].Journal of Wuhan University(Natural Science Edition),2024,70(6):671-679.
[17]CAO F,XU Z W,YI J B,et al.Multi-clause dynamic deduction algorithm and application based on clause comprehensive weight[J].Journal of Wuhan University(Natural Science Edition),2025, 71(2):301-312.
[18]CAOF,YANG X L,YI J B,et al. Contradiction separation super-deduction method and application[J].Journal of Computer Applications,2024,44(10):3074-3080.
[19]TANG X.A Comprehensive Survey of the Lean 4 Theorem Prover:Architecture,Applications,and Advances[J].arXiv:2501.18639,2025.
[20]WANG Q,LIU J,GUO D,et al.Formal Proof of Meta-Theorem in First-Order Logic in Coq[C]//China Intelligent Networked Things Conference.Singapore:Springer,2024:45-52.
[21]OTTEN J.20 Years of leanCoP-An Overview of the Provers[EB/OL].https://ceur-ws.org/Vol-3613/AReCCa2023_paper1.pdf.
[22]TUO H,MENG Z,SHI Z,et al.Interpretable neural networkclassification model using first-order logic rules[J].Neurocomputing,2025,614:128840.
[23]MENDELSON E.Introduction to mathematical logic[M].Chapman and Hall/CRC,2009.
[24]CAO F.Study on a first-order logic automated theorem prover based on contradiction separation deduction[D].Chengdu:Southwest Jiaotong University,2020:58-93.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市两江新区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发