计算机科学 ›› 2025, Vol. 52 ›› Issue (5): 235-240.doi: 10.11896/jsjkx.241000175
吴鑫, 陈树伟, 姜世攀
WU Xin, CHEN Shuwei, JIANG Shipan
摘要： 一阶逻辑自动定理证明器能够解决大量形式化后的实际问题,具有重要的应用价值。矛盾体分离演绎发展了自动定理证明领域经典的归结原理,具有更强的证明能力。在基于矛盾体分离规则的自动定理证明器CSE(Contradiction Separation Extension)的基础上,提出一种矛盾体分离式的简化算法,通过优化数据结构,使用指针保存子句间的互补信息,并在此基础上选择实际参与演绎的子句,从而得到最简矛盾体分离式。这种新的简化算法可生成更简短的分离式,进一步利用子句的合一互补性,增强空子句演绎路径的检测能力,提高证明器的效率。实验结果显示,相比CSE,使用此简化算法后的证明器CSE_ BSCS能多证明39个测试例,平均证明时间减少了18.64%,在证明能力和效率上均更优。
中图分类号:
| [1]NDUNGI R,UYUN S.A review of automated reasoning and its applications in the 21st century[J].The Indonesian Journal of Computer Science,2023,12(2):483-491. [2]CHEN G.Formal mathematics and proof engineering [J].Newsletter of the Chinese Computer Society,2016,12(9):40-44. [3]ROBINSON J A.A machine-oriented logic based on the resolution principle[J].Journal of the ACM,1965,12(1):23-41. [4]SLAGLE J R.Automatic theorem proving with renamable andsemantic resolution[J].Journal of the ACM,1967,14(4):687-697. [5]LOVELAND D W.A linear format for resolution[C]//Symposium on Automatic Demonstration.Berlin:Springer,2006:147-162. [6]LIU X H.Automatic reasoning based on resolution method[M]//Beijing:Science Press,1994:15-107. [7]KOVÁCS L,VORONKOV A.First-order theorem proving andVampire[C]//International Conference on Computer Aided Verification.Berlin:Springer,2013:1-35. [8]SCHULZ S,CRUANES S,VUKMIROVIĆ P.Faster,higher,stronger:E 2.3[C]//Automated Deduction-CADE 27:27th International Conference on Automated Deduction.Natal,Brazil:Springer International Publishing,2019:495-507. [9]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. [10]CAO F.Research on an automated theorem prover for first-order logic based on contradiction separation [D].Chengdu:Southwest Jiaotong University,2020:58-93. [11]CHEN S W,XU Y,JIANG Y,et al.Some synergized clause selection strategies for contradiction separation based automated deduction[C]//2017 12th International Conference on Intelligent Systems Knowledge Engineering(ISKE).IEEE,2017:1-6. [12]CAO F,XU Y,CHEN S W,et al.A contradiction separation dynamic deduction algorithm based on optimized proof search[J].International Journal of Computational Intelligence Systems,2019,12(2):1245-1254. [13]CAO F,XU Y,LIU J,et al.A multi-clause dynamic deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2021,566:281-299. [14]LIU P Y,WU G F,XU Y,et al.Extending e prover with fully use binary clauses algorithm based on standard contradiction separation rule[C]//2021 16th International Conference on Intelligent Systems and Knowledge Engineering(ISKE).IEEE,2021:11-14. [15]LIU P Y,XU Y,LIU J,et al.Fully reusing clause deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2023,622:337-356. [16]LIU P Y,CHEN S W,LIU J,et al.An efficient contradictionseparation based automated deduction algorithm for enhancing reasoning capability[J].Knowledge-Based Systems,2023,261:110217. [17]ZENG G Y,CHEN S W,LIU J,et al.A complementary ratiobased clause selection method for contradiction separation dynamic deduction[J].Knowledge-Based Systems,2024,284:111238. [18]JIANG S P,CHEN S W.Clause and Literal Selection Strategies Based on Complementary Pair Distribution for Contradiction Separation Deduction[C]//International Conference on AI Logic and Applications.Singapore:Springer Nature Singapore,2023:214-226. [19]ROBINSON A J,VORONKOV A.Handbook ofautomated reasoning[M]//Elsevier,2001:19-99. [20]CAO F,WANG J,XU Y,et al.CSE-A Automated TheoremProver Based on Standard Contradiction Separation Dynamic Deduction[J/OL].https://www.researchsquare.com/article/rs-3955960/v1. [21]SUTCLIFFE G,DESHARNAIS M.The 11th IJCAR automated theorem proving system competition-CASC-J11[J].AI Communications,2023,36(2):73-91. |
|
||
首页