From Wikipedia, the free encyclopedia
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