stringtranslate.com

Competencia del sistema CADE ATP

La CADE ATP System Competition ( CASC ) es una competencia anual de demostradores de teoremas totalmente automatizados para lógica clásica [1] [2] [3] [4]

Competencia

La CASC está asociada con la Conferencia sobre Deducción Automatizada y la Conferencia Conjunta Internacional sobre Razonamiento Automatizado organizadas por la Asociación para el Razonamiento Automatizado . Ha inspirado competencias similares en campos relacionados, en particular la exitosa competencia SMT-COMP [5] para teorías de módulo de satisfacibilidad , la competencia SAT [6] para razonadores proposicionales y la competencia de razonamiento lógico modal . [7]

La primera CASC, CASC-13, se celebró como parte de la 13ª Conferencia sobre Deducción Automatizada en la Universidad Rutgers , New Brunswick, NJ, en 1996. [3] Entre los sistemas que competían estaban Otter [8] y SETHEO. [9]

Véase también

Referencias

  1. ^ Sutcliffe, Geoff (2011). "La quinta competencia de sistemas de demostración de teoremas automatizados de IJCAR - CASC-J5". AI Communications . 24 (1): 75–89. doi :10.3233/AIC-2010-0483.
  2. ^ Geoff Sutcliffe . "La competición del sistema CADE ATP". Archivado desde el original el 2009-03-02 . Consultado el 2008-10-23 .
  3. ^ ab Geoff Sutcliffe y Christian Suttner (2006). "El estado de CASC". AI Communications . 19 (1): 35–48.
  4. ^ Jeff Pelletier, Geoff Sutcliffe y Christian Suttner (2002). "El desarrollo de CASC" (PDF) . AI Communications . 15 (2–3): 79–90.
  5. ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Competencia de teorías de satisfacibilidad módulo" (PDF) . Verificación asistida por computadora . Apuntes de clase en informática. 3576 . Springer: 20–23. doi :10.1007/11513988_4. ISBN 978-3-540-27231-1.
  6. ^ Matti, Järvisalo; Le Berré, Daniel; Roussel, Olivier; Simón, Laurent (2012). "Los concursos internacionales de solucionadores de SAT". Revista AI . 33 (1): 89–92. doi : 10.1609/aimag.v33i1.2395 .
  7. ^ Massacci, Fabio; Donini, Francesco M. (2000). "Diseño y resultados de la comparación de sistemas no clásicos (modales) TANCS-2000". Conferencia internacional sobre razonamiento automatizado con tablas analíticas y métodos relacionados . Apuntes de clase en informática. 1847. Springer: 52–56. CiteSeerX 10.1.1.385.6267 . doi :10.1007/10722086_4. ISBN .  978-3-540-67697-3.
  8. ^ McCune, William ; Wos, Larry (1997). "Otter: las encarnaciones de la competencia CADE-13". Revista de razonamiento automatizado . 18 (2): 211–220. doi :10.1023/A:1005843632307. S2CID  2481653.
  9. ^ Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). "Otter: las encarnaciones de la competencia CADE-13". Revista de razonamiento automatizado . 18 (2): 237–246. doi :10.1023/A:1005808119103. S2CID  821198.

Enlaces externos