CADE ATP System Competition: Difference between revisions

Revision as of 17:12, 14 July 2018

Latest revision as of 03:26, 15 August 2025

(21 intermediate revisions by 18 users not shown)

Line 1:

{{Short description|Annual automated theorem proving competition}}

<!-- Please do not remove or change this AfD message until the discussion has been closed. -->

The '''CADE ATP System Competition''' ('''CASC''') is an annual competition of fully [[automated theorem proving|automated theorem provers]] for [[classical logic]].<ref>{{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|url-access=subscription}}</ref><ref>{{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}}</ref><ref name=stateofcasc>{{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}}</ref><ref>{{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}}</ref>

{{Article for deletion/dated|page=CADE ATP System Competition|timestamp=20180713135737|year=2018|month=July|day=13|substed=yes|help=off}}

<!-- Once discussion is closed, please place on talk page: {{Old AfD multi|page=CADE ATP System Competition|date=13 July 2018|result='''keep'''}} -->

<!-- End of AfD message, feel free to edit beyond this point -->

The '''CADE ATP System Competition''' (CASC) is a yearly competition of fully [[Automated theorem proving|automated theorem provers]] for [[classical logic]]<ref>{{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}}</ref><ref>{{cite web|url=http://www.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition|author=[[Geoff Sutcliffe]]|accessdate=2008-10-23}}</ref><ref name=stateofcasc>{{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}}</ref><ref>{{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}}</ref> 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<ref>{{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. CAV 2005 |date=2005 |volume=3576 |publisher=Springer}}</ref> for [[Satisfiability Modulo Theories]], the SAT Competition<ref>{{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}}</ref> for propositional reasoners, and the modal logic reasoning competition.<ref>{{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}}</ref>

==Competition==

The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at [[Rutgers University]], New Brunswick, NJ, in 1996.<ref name=stateofcasc /> Among the systems competing were [[Otter (theorem prover)|Otter]]<ref>{{cite journal |last1=McCune |first1=William |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}}</ref> and [[SETHEO]].<ref>{{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}}</ref>

The '''CADE ATP System Competition''' (CASC) is a yearly competition of fully [[Automated theorem proving|automated theorem provers]] for [[classical logic]]<ref>{{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}}</ref><ref>{{cite web|url=http://www.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition|author=[[Geoff Sutcliffe]]|accessdate=2008-10-23}}</ref><ref name=stateofcasc>{{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}}</ref><ref>{{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}}</ref> 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<ref>{{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. CAV 2005]] |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 }}</ref> for [[Satisfiabilitysatisfiability Modulomodulo Theoriestheories]], the SAT Competition<ref>{{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-9289–92 |url=http://www.aaai.org/ojs/index.php/aimagazine/article/download/2395/2278|doi=10.1609/aimag.v33i1.2395 |doi-access=free }}</ref> for [[propositional logic|propositional]] reasoners, and the [[modal logic]] reasoning competition.<ref>{{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-5652–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 }}</ref>

The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at [[Rutgers University]], New Brunswick, NJ, in 1996.<ref name=stateofcasc /> Among the systems competing were [[Otter (theorem prover)|Otter]]<ref>{{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-220211–220|doi=10.1023/A:1005843632307 |s2cid=2481653 }}</ref> and [[SETHEO]].<ref>{{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-246237–246|doi=10.1023/A:1005808119103 |s2cid=821198 }}</ref>

== See also ==

* [[List of computer science awards]]

== References ==

{{Reflist}}

==External links==

* [https://web.archive.org/web/20090302112038/http://www.cs.miami.edu/~tptp/CASC/ Archive of original CASC Websitewebsite]

* [http://tptp.org/CASC/ CASC Website]

[[Category:Artificial intelligence competitions]]

[[Category:Computer science competitions]]

{{compsci-stub}}