El CADE ATP System Competition (CASC) es un concurso anual de probadores de teoremas totalmente automatizados para la lógica clásica [1] [2] [3] [4] CASC está asociado con la Conferencia sobre Deducción Automatizada y la Conferencia Conjunta Internacional sobre Razonamiento Automatizado organizado por la Asociación para el Razonamiento Automatizado . Ha inspirado una competencia similar en campos relacionados, en particular la exitosa competencia SMT-COMP [5] para las teorías de módulo de satisfacción , la competencia SAT [6] para razonadores proposicionales y la competencia de razonamiento lógico modal.[7]
El primer CASC, CASC-13, se llevó a cabo como parte de la 13ª Conferencia sobre Deducción Automatizada en la Universidad de Rutgers , New Brunswick, Nueva Jersey, en 1996. [3] Entre los sistemas que competían estaban Otter [8] y SETHEO . [9]
Ver también
Referencias
- ^ Sutcliffe, Geoff (2011). "El 5º Concurso de Sistema de Prueba de Teorema Automatizado IJCAR - CASC-J5" . Comunicaciones AI . 24 (1): 75–89. doi : 10.3233 / AIC-2010-0483 .
- ^ Geoff Sutcliffe . "La Competencia del Sistema CADE ATP" . Archivado desde el original el 2 de marzo de 2009 . Consultado el 23 de octubre de 2008 .
- ^ a b Geoff Sutcliffe y Christian Suttner (2006). "El Estado de CASC" . Comunicaciones AI . 19 (1): 35–48.
- ^ Jeff Pelletier, Geoff Sutcliffe y Christian Suttner (2002). "El desarrollo de CASC" (PDF) . Comunicaciones AI . 15 (2-3): 79-90.
- ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Concurso de teorías de módulo de satisfacción" (PDF) . Verificación asistida por computadora . Apuntes de conferencias en informática. Saltador. 3576 : 20-23. doi : 10.1007 / 11513988_4 . ISBN 978-3-540-27231-1.
- ^ Matti, Järvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). "Los concursos internacionales de solucionadores de SAT" . Revista AI . 33 (1): 89–92. doi : 10.1609 / aimag.v33i1.2395 .
- ^ Massacci, Fabio; Donini, Francesco M. (2000). "Diseño y resultados de la comparación de sistemas (modales) no clásicos TANCS-2000" . Conferencia internacional sobre razonamiento automatizado con cuadros analíticos y métodos relacionados . Apuntes de conferencias en informática. Saltador. 1847 : 52–56. CiteSeerX 10.1.1.385.6267 . doi : 10.1007 / 10722086_4 . ISBN 978-3-540-67697-3.
- ^ McCune, William; Wos, Larry (1997). "Encarnaciones de competencia Otter-the CADE-13". Revista de razonamiento automatizado . 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). "Encarnaciones de competencia Otter-the CADE-13". Revista de razonamiento automatizado . 18 (2): 237–246. doi : 10.1023 / A: 1005808119103 . S2CID 821198 .
enlaces externos
- Archivo del sitio web original de CASC
- Sitio web CASC