АссистентНовый вопросИсторияОбласти знаний
Партнёрские проектыСпецпроектыСтать автором
Сменить язык
О РУВИКИ

Соревнование систем автоматического доказательства теорем CADE

Соревнование систем автоматического доказательства теорем CADE (англ. CADE ATP System Competition, CASC) — ежегодное соревнование полностью автоматических систем доказательства теорем для классической логики[1][2][3][4]. Соревнование имеет официальный статус чемпионата мира[5], его организатором является Джефф Сатклифф из Университета Майами.

Соревнование

CASC связан с Конференцией по автоматическому выводу и Международной объединённой конференцией по автоматическому рассуждению, организуемыми Ассоциацией по автоматическому рассуждению. Соревнование послужило вдохновением для аналогичных соревнований в смежных областях, в частности, для успешного соревнования SMT-COMP[6] по проверке удовлетворимости с учётом теорий, соревнования SAT[7] для решателей пропозициональной логики и соревнования по рассуждению в модальной логике.

Первое соревнование CASC, CASC-13, прошло в рамках 13-й Конференции по автоматическому выводу в Университете Ратгерса, Нью-Брансуик, Нью-Джерси, в 1996 году[3]. Среди участвовавших систем были Otter[8] и SETHEO[9]. Официальными победителями турнира стали система E-SETHEO в дивизионе MIX и Otter 3.0.4z в дивизионе UEQ[10]

Формат и отбор задач

Библиотека TPTP является источником задач для соревнования. К участию допускаются задачи, имеющие рейтинг сложности от 0.21 до 0.99, при этом они не должны быть пропозициональными или искусственно подогнанными (biased) под конкретные системы. Для предотвращения получения системами преимущества за счёт специфического форматирования применяется процесс обфускации задач, включающий удаление комментариев и перемешивание формул[11].

Хронология и рекорды

Последние соревнования проходили в следующих городах: CASC-29 (2023) состоялось в Риме, CASC-J12 (2024) — в Нанси, а CASC-30 (2025) — в Штутгарте[12].

Исторический рекорд турнира принадлежит системе автоматического доказательства теорем Vampire, которую разрабатывает команда Технического университета Вены под руководством Лауры Ковач[13]. В 2025 году на соревновании CASC-30 система впервые в истории CASC одержала победу во всех восьми дивизионах[13][14]. В 2026 году на турнире CASC-J13 Vampire также выиграла во всех проведённых дивизионах.

Примечания

  1. ↑ Sutcliffe, Geoff (2011). “The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5”. AI Communications [англ.]. 24 (1): 75—89. DOI:10.3233/AIC-2010-0483. Дата обращения 2026-08-26.
  2. ↑ Geoff Sutcliffe. The CADE ATP System Competition (англ.). Дата обращения: 23 октября 2008. Архивировано 2 марта 2009 года.
  3. ↑ 1 2 Geoff Sutcliffe and Christian Suttner (2006). “The State of CASC”. AI Communications [англ.]. 19 (1): 35—48. Дата обращения 2026-08-26.
  4. ↑ Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002). “The Development of CASC” (PDF). AI Communications [англ.]. 15 (2—3): 79—90. Дата обращения 2026-08-26.
  5. ↑ CASC World Championship Status. ACM Digital Library. Дата обращения: 26 августа 2026.
  6. ↑ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). “SMT-COMP: Satisfiability Modulo Theories Competition” (PDF). Computer Aided Verification. Lecture Notes in Computer Science [англ.]. Springer. 3576: 20—23. DOI:10.1007/11513988_4. ISBN 978-3-540-27231-1. Дата обращения 2026-08-26.
  7. ↑ Järvisalo, Matti; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). “The international SAT solver competitions”. AI Magazine [англ.]. 33 (1): 89—92. DOI:10.1609/aimag.v33i1.2395. Дата обращения 2026-08-26.
  8. ↑ McCune, William; Wos, Larry (1997). “Otter — инкарнации для соревнования CADE-13”. Journal of Automated Reasoning [англ.]. 18 (2): 211—220. DOI:10.1023/A:1005843632307. S2CID 2481653. Дата обращения 2024-06-23. |access-date= требует |url= (справка)
  9. ↑ Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). “Otter — инкарнации для соревнования CADE-13”. Journal of Automated Reasoning [англ.]. 18 (2): 237—246. DOI:10.1023/A:1005808119103. S2CID 821198. Дата обращения 2024-06-23. |access-date= требует |url= (справка)
  10. ↑ Официальные победители CASC-13. University of Miami. Дата обращения: 26 августа 2026.
  11. ↑ The CADE ATP System Competition (CASC). AI Magazine. Дата обращения: 26 августа 2026.
  12. ↑ CASC-30. Google Groups. Дата обращения: 26 августа 2026.
  13. ↑ 1 2 Riesenerfolg für Vampire. TU Wien Informatics. Дата обращения: 26 августа 2026.
  14. ↑ Huge success for Vampire. TU Wien. Дата обращения: 26 августа 2026.

Литература

  • Geoff Sutcliffe. The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5 // AI Communications. 2011. Т. 24, № 1. С. 75–89. doi:10.3233/AIC-2010-0483.
  • Jeff Pelletier, Geoff Sutcliffe, Christian Suttner. The Development of CASC // AI Communications. 2002. Т. 15, № 2–3. С. 79–90.
  • Geoff Sutcliffe и др. The CADE-29 Automated Theorem Proving System Competition – CASC-29 // AI Communications. 2024. doi:10.3233/aic-230325.
  • Geoff Sutcliffe. The CADE-30 Automated Theorem Proving System Competition-CASC-30 // The European journal on artificial intelligence. 2026. 20 с. doi:10.1177/30504554261463374[1].

Ссылки

  1. ↑ The CADE-30 Automated Theorem Proving System Competition-CASC-30. scholarship.miami.edu (2026). Дата обращения: 26 августа 2026.

Категории