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