Competición del sistema ATP de CADE

La competición del sistema CADE ATP ( CASC ) es una competición anual de demostradores de teoremas totalmente automatizados para lógica clásica . ^{[ 1 ]}^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}

Competencia

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 competiciones similares en campos relacionados, en particular la exitosa competición SMT-COMP ^{[ 5 ]} para la satisfacibilidad módulo teorías , la competición SAT ^{[ 6 ]} para razonadores proposicionales y la competición de razonamiento lógico modal ^[⁷^] .

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

Véase también

Lista de premios de informática

Referencias

↑ Sutcliffe, Geoff (2011). "La quinta competición de sistemas de demostración automática de teoremas de IJCAR - CASC-J5" . AI Communications . 24 (1): 75–89 . doi : 10.3233/AIC-2010-0483 .
↑ Geoff Sutcliffe . "La competición del sistema CADE ATP" . Archivado del original el 2 de marzo de 2009. Consultado el 23 de octubre de 2008 .
1 2 Geoff Sutcliffe y Christian Suttner (2006). "El estado de CASC" . AI Communications . 19 (1): 35– 48.
↑ Jeff Pelletier, Geoff Sutcliffe y Christian Suttner (2002). "El desarrollo de CASC" (PDF) . AI Communications . 15 ( 2–3 ): 79–90 .
↑ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfacibilidad Módulo Teorías Competitiva" (PDF) . Verificación Asistida por Computadora . Notas de Clase en Ciencias de la Computación. Vol. 3576. Springer. pp. 20–23 . doi : 10.1007/11513988_4 . ISBN 978-3-540-27231-1.
↑ 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 .
↑ 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 Tableaux Analíticos y Métodos Relacionados . Lecture Notes in Computer Science. Vol. 1847. Springer. pp. 52–56 . CiteSeerX 10.1.1.385.6267 . doi : 10.1007/10722086_4 . ISBN 978-3-540-67697-3.
↑ McCune, William ; Wos, Larry (1997). "Otter: las encarnaciones de la competición CADE-13". Journal of Automated Reasoning . 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). "Otter: las encarnaciones de la competición CADE-13". Journal of Automated Reasoning . 18 (2): 237– 246. doi : 10.1023/A:1005808119103 . S2CID 821198 .

Enlaces externos

Archivo del sitio web original de CASC
Sitio web de CASC

[1] Sutcliffe, Geoff (2011). "La quinta competición de sistemas de demostración automática de teoremas 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 del original el 2 de marzo de 2009. Consultado el 23 de octubre de 2008 .

[stateofcasc-3] 1 2 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: Satisfacibilidad Módulo Teorías Competitiva" (PDF) . Verificación Asistida por Computadora . Notas de Clase en Ciencias de la Computación. Vol. 3576. Springer. pp. 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 Tableaux Analíticos y Métodos Relacionados . Lecture Notes in Computer Science. Vol. 1847. Springer. pp. 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 competición CADE-13". Journal of Automated Reasoning . 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 competición CADE-13". Journal of Automated Reasoning . 18 (2): 237– 246. doi : 10.1023/A:1005808119103 . S2CID 821198 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[

[ 8 ]

[ 9 ]

Competencia

Véase también

Referencias

Enlaces externos

Articulos relacionados