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