Annual automated theorem proving competition
The CADE ATP System Competition (CASC ) is an annual competition of fully automated theorem provers for classical logic [ 1] [ 2] [ 3] [ 4]
Competition
CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning . It has inspired similar competition in related fields, in particular the successful SMT-COMP competition[ 5] for satisfiability modulo theories , the SAT Competition[ 6] for propositional reasoners, and the modal logic reasoning competition.[ 7]
The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at Rutgers University , New Brunswick, NJ, in 1996.[ 3] Among the systems competing were Otter [ 8] and SETHEO .[ 9]
See also
References
^ Sutcliffe, Geoff (2011). "The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5" . AI Communications . 24 (1): 75–89. doi :10.3233/AIC-2010-0483 .
^ Geoff Sutcliffe . "The CADE ATP System Competition" . Archived from the original on 2009-03-02. Retrieved 2008-10-23 .
^ a b Geoff Sutcliffe and Christian Suttner (2006). "The State of CASC" . AI Communications . 19 (1): 35–48.
^ Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002). "The Development of CASC" (PDF) . AI Communications . 15 (2–3): 79–90.
^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfiability Modulo Theories Competition" (PDF) . Computer Aided Verification . Lecture Notes in Computer Science. 3576 . Springer: 20–23. doi :10.1007/11513988_4 . ISBN 978-3-540-27231-1 .
^ Matti, Järvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). "The international SAT solver competitions" . AI Magazine . 33 (1): 89–92. doi :10.1609/aimag.v33i1.2395 .
^ Massacci, Fabio; Donini, Francesco M. (2000). "Design and results of TANCS-2000 non-classical (modal) systems comparison" . International Conference on Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Computer Science. 1847 . Springer: 52–56. CiteSeerX 10.1.1.385.6267 . doi :10.1007/10722086_4 . ISBN 978-3-540-67697-3 .
^ McCune, William ; Wos, Larry (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning . 18 (2): 211–220. doi :10.1023/A:1005843632307 . S2CID 2481653 .
^ Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning . 18 (2): 237–246. doi :10.1023/A:1005808119103 . S2CID 821198 .
External links