Computer Science

Computer Science ›› 2026, Vol. 53 ›› Issue (7): 186-194.doi: 10.11896/jsjkx.250400099

• Artificial Intelligence • Previous Articles     Next Articles

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 Online:2026-07-15 Published: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)

8

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

CLC Number: 

  • 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.
[1] HU Junjie, CHEN Yujie, HU Yikun, WEN Cheng, CAO Jialun, MA Zhi, SU Jie, SUN Weidi, TIAN Cong, QIN Shengchao. Formal Theorem Proving Empowered by Large Language Model:Survey and Perspectives [J]. Computer Science, 2026, 53(4): 1-23.
[2] CHEN Hongxiu, ZENG Xia, LIU Zhiming, ZHAO Hengjun. Automatic Theorem Proving Based on Pre-trained Language Models and Unification [J]. Computer Science, 2026, 53(4): 40-47.
[3] ZHU Jian, HU Kai, WANG Jun, LI Jie, YE Yafei, SHI Xiyan. Reliable Smart Contract Automatic Generation Based on Event-B [J]. Computer Science, 2023, 50(10): 343-349.
[4] ZHENG Wen-ping, WANG Ning, YANG Gui. Overlapping Community Detection Algorithm Based on Local Path Information [J]. Computer Science, 2022, 49(12): 155-162.
[5] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[6] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[7] ZHU Xian-wei, ZHU Zhi-qiang and SUN Lei. Design and Formal Verification of Xen Hybrid Multi-police Model [J]. Computer Science, 2017, 44(10): 134-141.
[8] LI Shan-shan, ZHAO Chun-na, GUAN Yong, SHI Zhi-ping, WANG Rui, LI Xiao-juan and YE Shi-wei. Formalization of Consistency of Fractional Calculus in HOL4 [J]. Computer Science, 2016, 43(3): 23-26.
[9] YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29.
[10] LV Xing-li, SHI Zhi-ping, LI Xiao-juan, GUAN Yong, YE Shi-wei and ZHANG Jie. Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform [J]. Computer Science, 2015, 42(4): 31-36.
[11] . Formal Model of Web Component Based on Object-Z Specification [J]. Computer Science, 2012, 39(Z6): 383-388.
[12] REN Hong-Bo （Computer Science Institute, Zhejiang University, Hangzhou310027）. [J]. Computer Science, 2007, 34(4): 49-51.
[13] WU Guang-Wei, DONG Rong-Sheng （Department of Computer, Guilin University of Electronic Technology, Guilin 541004）. [J]. Computer Science, 2006, 33(8): 9-13.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.