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 条
[51]  
McKeown J., 2023, P 36 INT FLAIRS C, DOI [10.32473/flairs.36.133334, DOI 10.32473/FLAIRS.36.133334]
[52]  
Nelson G., 1979, ACM Transactions on Programming Languages and Systems, V1, P245, DOI 10.1145/357073.357079
[53]   Mapping global dynamics of benchmark creation and saturation in artificial intelligence [J].
Ott, Simon ;
Barbosa-Silva, Adriano ;
Blagec, Kathrin ;
Brauner, Jan ;
Samwald, Matthias .
NATURE COMMUNICATIONS, 2022, 13 (01)
[54]  
Paulson L.C., 2012, EPIC SERIES COMPUTIN, V2, P1, DOI [DOI 10.29007/36DT, 10.29007/tnfd, 10, 10.29007/36dt]
[55]  
Pelletier FJ, 2002, AI COMMUN, V15, P79
[56]  
Peter L.J., 1969, THE PETER PRINCIPLE
[57]  
Quaife A., 1989, Journal of Automated Reasoning, V5, P97, DOI 10.1007/BF00245024
[58]   A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic [J].
Rummer, Philipp .
Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2008, 5330 :274-289
[59]  
Schulz Stephan, 2013, Logic for Programming, Artificial Intelligence and Reasoning. 19th International Conference, LPAR-19, Proceedings: LNCS 8312, P735, DOI 10.1007/978-3-642-45221-5_49
[60]   Faster, Higher, Stronger: E 2.3 [J].
Schulz, Stephan ;
Cruanes, Simon ;
Vukmirovic, Petar .
AUTOMATED DEDUCTION, CADE 27, 2019, 11716 :495-507
123456789