An Empirical Assessment of Progress in Automated Theorem Proving

被引：2
作者：
Sutcliffe, Geoff [1 ]
Suttner, Christian
Kotthoff, Lars [2 ]
Perrault, C. Raymond [3 ]
Khalid, Zain [1 ]
机构：
[1] Univ Miami, Miami, FL 33124 USA
[2] Univ Wyoming, Laramie, WY USA
[3] SRI Int, Menlo Pk, CA USA
来源：
AUTOMATED REASONING, IJCAR 2024, PT I | 2024年 / 14739卷
关键词：
Automated Theorem Proving; Empirical Evaluation; Progress; SYSTEM COMPETITION; SMT-COMP; TPTP; IMPLEMENTATION; LOGIC;
D O I：
10.1007/978-3-031-63498-7_4
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. This work uses data in the TPTP World to assess progress in ATP from 2015 to 2023.
引用
收藏
页码：53 / 74
页数：22
相关论文
共 90 条
[1]  
[Anonymous], 2008, LNCS (LNAI), V5195, P292, DOI [10.1007/978-3-540-71070-724, DOI 10.1007/978-3-540-71070-724]
[2]  
Aygün E, 2022, PR MACH LEARN RES
[3]  
Azerbayev Z, 2024, Arxiv, DOI [arXiv:2310.10631, 10.48550/ARXIV.2310.10631]
[4]  
Bansal K., 2019, PR MACH LEARN RES, P454
[5]  
Barrett C, 2005, LECT NOTES COMPUT SC, V3576, P20
[6]  
Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
[7]   TOOLympics 2019: An Overview of Competitions in Formal Methods [J].
Bartocci, Ezio ;
Beyer, Dirk ;
Black, Paul E. ;
Fedyukovich, Grigory ;
Garavel, Hubert ;
Hartmanns, Arnd ;
Huisman, Marieke ;
Kordon, Fabrice ;
Nagele, Julian ;
Sighireanu, Mihaela ;
Steffen, Bernhard ;
Suda, Martin ;
Sutcliffe, Geoff ;
Weber, Tjark ;
Yamada, Akihisa .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 :3-24
[8]   Superposition for Full Higher-order Logic [J].
Bentkamp, Alexander ;
Blanchette, Jasmin ;
Tourret, Sophie ;
Vukmirovic, Petar .
AUTOMATED DEDUCTION, CADE 28, 2021, 12699 :396-412
[9]   Superposition with Lambdas [J].
Bentkamp, Alexander ;
Blanchette, Jasmin ;
Tourret, Sophie ;
Vukmirovic, Petar ;
Waldmann, Uwe .
AUTOMATED DEDUCTION, CADE 27, 2019, 11716 :55-73
[10]   Reliable benchmarking: requirements and solutions [J].
Beyer, Dirk ;
Loewe, Stefan ;
Wendler, Philipp .
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (01) :1-29
123456789