Jump to content

CADE ATP System Competition

Edit links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Jarble (talk | contribs) at 18:17, 20 August 2019 (adding links to references using Google Scholar). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic[1][2][3][4] 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]

References

  1. ^ Sutcliffe, Geoff (2011). "The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5". AI Communications. 24 (1): 75–89.
  2. ^ Geoff Sutcliffe. "The CADE ATP System Competition". Archived from the original on 2009-03-02. Retrieved 2008-10-23. {{cite web}}: Unknown parameter |dead-url= ignored (|url-status= suggested) (help)
  3. ^ a b Geoff Sutcliffe and Christian Suttner (2006). "The State of CASC". AI Communications. 19 (1): 35–48.
  4. ^ Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002). "The Development of CASC" (PDF). AI Communications. 15 (2–3): 79–90.
  5. ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfiability Modulo Theories Competition" (PDF). Computer Aided Verification. CAV 2005. 3576. Springer.
  6. ^ Matti, Järvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). "The international SAT solver competitions". AI Magazine. 33 (1): 89–92.
  7. ^ Massacci, Fabio; Donini, Francesco M. (2000). "Design and results of TANCS-2000 non-classical (modal) systems comparison" (PDF). International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. 1847. Springer: 52–56.
  8. ^ McCune, William; Wos, Larry (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning. 18 (2): 211–220.
  9. ^ 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.


Stub icon

This computer science article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=CADE_ATP_System_Competition&oldid=911721636"