:CADE ATP System Competition
{{Short description|Annual automated theorem proving competition}}
The CADE ATP System Competition (CASC) is an annual competition of fully automated theorem provers for classical logic{{cite journal|last=Sutcliffe|first=Geoff|title=The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5|journal=AI Communications|year=2011|volume=24|issue=1|pages=75–89|url=https://content.iospress.com/articles/ai-communications/aic483|doi=10.3233/AIC-2010-0483}}{{cite web|url=http://www.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition|author=Geoff Sutcliffe|accessdate=2008-10-23|archive-url=https://web.archive.org/web/20090302112038/http://www.cs.miami.edu/~tptp/CASC/|archive-date=2009-03-02|url-status=dead|author-link=Geoff Sutcliffe}}{{cite journal|journal=AI Communications|title=The State of CASC|year=2006|volume=19|issue=1|pages=35–48|author=Geoff Sutcliffe and Christian Suttner|url=https://content.iospress.com/articles/ai-communications/aic359}}{{cite journal|journal=AI Communications|title=The Development of CASC|year=2002|volume=15|issue=2–3|pages=79–90|author=Jeff Pelletier, Geoff Sutcliffe and Christian Suttner|url=http://www.cs.miami.edu/home/geoff/Papers/Journal/2002_PSS02_AIComm-15-2-79-90.pdf}}
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{{cite journal |last1=Barrett |first1=Clark |last2=de Moura |first2=Leonardo |last3=Stump |first3=Aaron |title=SMT-COMP: Satisfiability Modulo Theories Competition |journal=Computer Aided Verification |date=2005 |volume=3576 |pages=20–23 |publisher=Springer|url=https://link.springer.com/content/pdf/10.1007/11513988_4.pdf|doi=10.1007/11513988_4 |series=Lecture Notes in Computer Science |isbn=978-3-540-27231-1 }} for satisfiability modulo theories, the SAT Competition{{cite journal |last1=Matti |first1=Järvisalo |last2=Le Berre |first2=Daniel |last3=Roussel |first3=Olivier |last4=Simon |first4=Laurent |title=The international SAT solver competitions|journal=AI Magazine |date=2012 |volume=33 |issue=1 |pages=89–92 |url=http://www.aaai.org/ojs/index.php/aimagazine/article/download/2395/2278|doi=10.1609/aimag.v33i1.2395 |doi-access=free }} for propositional reasoners, and the modal logic reasoning competition.{{cite journal |last1=Massacci |first1=Fabio |last2=Donini |first2=Francesco M. |title=Design and results of TANCS-2000 non-classical (modal) systems comparison |journal=International Conference on Automated Reasoning with Analytic Tableaux and Related Methods |date=2000 |volume=1847 |pages=52–56 |publisher=Springer|url=https://www.researchgate.net/publication/221342978|doi=10.1007/10722086_4 |citeseerx=10.1.1.385.6267 |series=Lecture Notes in Computer Science |isbn=978-3-540-67697-3 }}
The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at Rutgers University, New Brunswick, NJ, in 1996. Among the systems competing were Otter{{cite journal |last1=McCune |first1=William |author1link = William McCune|last2=Wos |first2=Larry |title=Otter-the CADE-13 competition incarnations |journal=Journal of Automated Reasoning |date=1997 |volume=18 |issue=2 |pages=211–220|doi=10.1023/A:1005843632307 |s2cid=2481653 }} and SETHEO.{{cite journal |last1=Moser |first1=Max |last2=Ibens |first2=Ortrun |last3=Letz |first3=Reinhold |last4=Steinbach |first4=Joachim |last5=Goller |first5=Christoph |last6=Schumann |first6=Johann |last7=Mayr |first7=Klaus |title=Otter-the CADE-13 competition incarnations |journal=Journal of Automated Reasoning |date=1997 |volume=18 |issue=2 |pages=237–246|doi=10.1023/A:1005808119103 |s2cid=821198 }}
See also
References
{{Reflist}}
External links
- [https://web.archive.org/web/20090302112038/http://www.cs.miami.edu/~tptp/CASC/ Archive of original CASC website]
- [http://tptp.org/CASC/ CASC Website]