Конкурс CADE ATP System - CADE ATP System Competition

В Конкурс CADE ATP System (CASC) - ежегодное соревнование полностью автоматические средства доказательства теорем за классическая логика[1][2][3][4] CASC связан с Конференция по автоматическому вычету и Международная совместная конференция по автоматизированному мышлению организованный Ассоциация автоматизированного мышления. Это послужило стимулом для аналогичных соревнований в смежных областях, в частности, успешное соревнование SMT-COMP.[5] за Теории выполнимости по модулю, конкурс SAT[6] для пропозициональных рассуждающих и модальной логической конкуренции рассуждений.[7]

Первый CASC, CASC-13, был проведен в рамках 13-й конференции по автоматизированному вычету в г. Университет Рутгерса, Нью-Брансуик, штат Нью-Джерси, в 1996 году.[3] Среди конкурирующих систем были Выдра[8] и СЕТЕО.[9]

Смотрите также

Рекомендации

  1. ^ Сатклифф, Джефф (2011). "Пятый конкурс автоматизированных систем доказательства теорем IJCAR - CASC-J5". AI-коммуникации. 24 (1): 75–89. Дои:10.3233 / AIC-2010-0483.
  2. ^ Джефф Сатклифф. «Конкурс CADE ATP System». Архивировано из оригинал на 2009-03-02. Получено 2008-10-23.
  3. ^ а б Джефф Сатклифф и Кристиан Саттнер (2006). «Состояние CASC». AI-коммуникации. 19 (1): 35–48.
  4. ^ Джефф Пеллетье, Джефф Сатклифф и Кристиан Саттнер (2002). «Развитие CASC» (PDF). AI-коммуникации. 15 (2–3): 79–90.
  5. ^ Барретт, Кларк; де Моура, Леонардо; Пень, Аарон (2005). "SMT-COMP: Конкурс теорий удовлетворенности по модулю" (PDF). Компьютерная проверка. CAV 2005. Конспект лекций по информатике. Springer. 3576: 20–23. Дои:10.1007/11513988_4. ISBN  978-3-540-27231-1.
  6. ^ Матти, Ярвисало; Ле Бер, Даниэль; Руссель, Оливье; Саймон, Лоран (2012). «Международные соревнования SAT Solver». Журнал AI. 33 (1): 89–92. Дои:10.1609 / aimag.v33i1.2395.
  7. ^ Массаччи, Фабио; Донини, Франческо М. (2000). «Дизайн и результаты сравнения неклассических (модальных) систем TANCS-2000». Международная конференция по автоматическому мышлению с аналитическими таблицами и родственными методами. Конспект лекций по информатике. Springer. 1847: 52–56. CiteSeerX  10.1.1.385.6267. Дои:10.1007/10722086_4. ISBN  978-3-540-67697-3.
  8. ^ МакКьюн, Уильям; Вос, Ларри (1997). «Выдра-соревновательные воплощения САДЕ-13». Журнал автоматизированных рассуждений. 18 (2): 211–220. Дои:10.1023 / А: 1005843632307.
  9. ^ Мозер, Макс; Ибенс, Ортрун; Letz, Reinhold; Штейнбах, Иоахим; Голлер, Кристоф; Шуман, Иоганн; Майр, Клаус (1997). «Выдра-соревновательные воплощения САДЕ-13». Журнал автоматизированных рассуждений. 18 (2): 237–246. Дои:10.1023 / А: 1005808119103.

внешняя ссылка