Computer Science ›› 2025, Vol. 52 ›› Issue (5): 235-240.doi: 10.11896/jsjkx.241000175
• Artificial Intelligence • Previous Articles Next Articles
WU Xin, CHEN Shuwei, JIANG Shipan
CLC Number:
| [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. |
| [1] | REN Shuang-yan, GUO Wei, FAN Chang-qi, WANG Zhe, WU Song-yang. Multi-view Distance Metric Learning with Inter-class and Intra-class Density [J]. Computer Science, 2022, 49(11A): 211000131-6. |
| [2] | CHEN Li-ping, XU Peng, WANG Dan-chen, XU Yang. Study on Formal Verification of EAP-TLS Protocol [J]. Computer Science, 2022, 49(11A): 211100111-5. |
|
||
Home