Парадокс (доказательство теоремы)

Парадокс
Разработчик(и)	Коэн Линдстрем Классен ; Никлас Соренссон ;
Написано в	Хаскелл
Тип	Автоматизированное доказательство теорем
Лицензия	Стандартная общественная лицензия GNU

Paradox — это средство поиска моделей в конечной области для чистой логики первого порядка (FOL) с равенством, разработанное Коэном Линдстремом Классеном и Никласом Сёренссоном из Технологического университета Чалмерса . ^[1]^[2] Он может участвовать как часть автоматизированной системы доказательства теорем . ^[2] Программное обеспечение в основном написано на языке программирования Haskell . ^[3] Он распространяется на условиях GNU General Public License и бесплатен. ^[4]

Функции

Разработчики Paradox описали это программное обеспечение как Mace метод в стиле , названный в честь одноименного инструмента МакКьюна. ^[5]^[6] В «Парадоксе» представлены новые методы, которые помогают снизить вычислительную сложность задачи поиска модели : ^[5]

определения терминов , новая техника сокращения переменных,
инкрементальная проверка выполнимости , которая сначала работает с небольшими доменами, затем постепенно увеличивает размер домена, повторно используя информацию, полученную в результате предыдущих неудачных поисков,
снижение статической симметрии , которое добавляет дополнительные ограничения,
вывод сортировки , который работает с несортированными проблемами.

Paradox был разработан до версии 4, последняя версия была эффективна при поиске моделей для языка веб-онтологии OWL2. ^[7]

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

Paradox был победителем в ежегодном конкурсе CADE ATP System Competition , ежегодном конкурсе по автоматизированному доказательству теорем, с 2003 по 2012 год. ^[8]

Ссылки

^ «Парадокс» . Технологический университет Чалмерса . Архивировано из оригинала 8 января 2007 года . Проверено 26 мая 2007 г.
↑ Перейти обратно: Перейти обратно: ^а ^б Пудлак, Петр (17 июля 2007 г.). «Семантический выбор посылок для автоматического доказательства теорем» (PDF) . В Урбане, Дж.; Сатклифф, Дж.; Шульц, С. (ред.). Материалы семинара CADE-21 по эмпирически успешным автоматизированным рассуждениям в больших теориях . 21-я Международная конференция по автоматизированному дедукции. Материалы семинара CEUR. Том. 257. Бремен. стр. 27–44. ISSN 1613-0073 . S2CID 16318678 . Архивировано из оригинала (PDF) 7 ноября 2018 года . Проверено 7 ноября 2011 г.
^ «Описание системы абитуриентов» . Университет Майами . Парадокс 3.0. Архивировано из оригинала 7 ноября 2018 года . Проверено 7 ноября 2018 г.
^ «Парадокс» . Технологический университет Чалмерса . Архивировано из оригинала 15 января 2007 года . Проверено 30 апреля 2020 г.
↑ Перейти обратно: Перейти обратно: ^а ^б Классен, Коэн; Сёренссон, Никлас. «Новые методы, улучшающие поиск конечных моделей в стиле MACE» (PDF) . S2CID 15694927 . Архивировано из оригинала (PDF) 11 ноября 2018 года . Проверено 11 ноября 2018 г.
^ «Автоматическое доказательство теорем» (PDF) . Колледж инженерии и информатики Австралийского национального университета . стр. 73–74. Архивировано (PDF) из оригинала 11 ноября 2018 г. Проверено 11 ноября 2018 г.
^ Шнайдер, Майкл; Сатклифф, Джефф (2011). «Рассуждения на языке полных онтологий OWL 2 с использованием автоматического доказательства теорем первого порядка». arXiv : 1108.0155 [ cs.AI ].
^ «Соревнования по системе CADE ATP — чемпионат мира по автоматизированному доказательству теорем» . Предыдущие победители дивизиона CASC. Архивировано из оригинала 1 сентября 2018 года . Проверено 7 ноября 2018 г.

[Equinox-Paradox-1] «Парадокс» . Технологический университет Чалмерса . Архивировано из оригинала 8 января 2007 года . Проверено 26 мая 2007 г.

[Petr-P-2] Перейти обратно: Перейти обратно: ^а ^б Пудлак, Петр (17 июля 2007 г.). «Семантический выбор посылок для автоматического доказательства теорем» (PDF) . В Урбане, Дж.; Сатклифф, Дж.; Шульц, С. (ред.). Материалы семинара CADE-21 по эмпирически успешным автоматизированным рассуждениям в больших теориях . 21-я Международная конференция по автоматизированному дедукции. Материалы семинара CEUR. Том. 257. Бремен. стр. 27–44. ISSN 1613-0073 . S2CID 16318678 . Архивировано из оригинала (PDF) 7 ноября 2018 года . Проверено 7 ноября 2011 г.

[CASC-6-Entrants-3] «Описание системы абитуриентов» . Университет Майами . Парадокс 3.0. Архивировано из оригинала 7 ноября 2018 года . Проверено 7 ноября 2018 г.

[Paradox-home-alone-4] «Парадокс» . Технологический университет Чалмерса . Архивировано из оригинала 15 января 2007 года . Проверено 30 апреля 2020 г.

[Author-paper-5] Перейти обратно: Перейти обратно: ^а ^б Классен, Коэн; Сёренссон, Никлас. «Новые методы, улучшающие поиск конечных моделей в стиле MACE» (PDF) . S2CID 15694927 . Архивировано из оригинала (PDF) 11 ноября 2018 года . Проверено 11 ноября 2018 г.

[Baumgartner-slides-6] «Автоматическое доказательство теорем» (PDF) . Колледж инженерии и информатики Австралийского национального университета . стр. 73–74. Архивировано (PDF) из оригинала 11 ноября 2018 г. Проверено 11 ноября 2018 г.

[Hoot-too-7] Шнайдер, Майкл; Сатклифф, Джефф (2011). «Рассуждения на языке полных онтологий OWL 2 с использованием автоматического доказательства теорем первого порядка». arXiv : 1108.0155 [ cs.AI ].

[CADE-comp-2018-8] «Соревнования по системе CADE ATP — чемпионат мира по автоматизированному доказательству теорем» . Предыдущие победители дивизиона CASC. Архивировано из оригинала 1 сентября 2018 года . Проверено 7 ноября 2018 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]