Конечно-доменный поиск модели для чистой логики первого порядка с равенством
Paradox — это конечно-доменная модель поиска для чистой логики первого порядка (FOL) с равенством, разработанная Коэном Линдстрёмом Классеном и Никласом Сёренссоном в Технологическом университете Чалмерса . [1] [2] Она может участвовать в качестве части автоматизированной системы доказательства теорем . [2] Программное обеспечение в основном написано на языке программирования Haskell . [3] Она распространяется в соответствии с условиями GNU General Public License и является бесплатной. [4]
Функции
Разработчики Paradox описали программное обеспечение как метод в стиле Mace , в честь одноименного инструмента МакКьюна. [5] [6] Paradox представил новые методы, которые помогают снизить вычислительную сложность задачи поиска модели : [5]
- определения терминов , новый метод сокращения переменных,
- Инкрементная проверка выполнимости , которая сначала работает с небольшими доменами, а затем постепенно увеличивает размер домена, повторно используя информацию, полученную из предыдущих неудачных поисков,
- статическое снижение симметрии , которое добавляет дополнительные ограничения,
- сортировка вывода , которая работает с несортированными задачами.
Paradox был разработан до версии 4, последняя версия эффективна при поиске моделей для языка веб-онтологий OWL2. [7]
Соревнование
Paradox был победителем в ежегодном конкурсе CADE ATP System Competition , ежегодном конкурсе по автоматизированному доказательству теорем, в период с 2003 по 2012 год. [8]
Ссылки
- ^ "Paradox". Chalmers University of Technology . Архивировано из оригинала 8 января 2007 года . Получено 26 мая 2007 года .
- ^ ab Pudlák, Petr (17 июля 2007 г.). "Семантический выбор предпосылок для автоматического доказательства теорем" (PDF) . В Urban, J.; Sutcliffe, G.; Schulz, S. (ред.). Труды семинара CADE-21 по эмпирически успешным автоматизированным рассуждениям в больших теориях . 21-я международная конференция по автоматизированной дедукции. Труды семинара CEUR. Том 257. Бремен. стр. 27–44. ISSN 1613-0073. S2CID 16318678. Архивировано из оригинала (PDF) 7 ноября 2018 г. . Получено 7 ноября 2011 г. .
- ^ "Entrants' System Descriptions". Университет Майами . Paradox 3.0. Архивировано из оригинала 7 ноября 2018 года . Получено 7 ноября 2018 года .
- ^ "Paradox". Chalmers University of Technology . Архивировано из оригинала 15 января 2007 года . Получено 30 апреля 2020 года .
- ^ ab Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding" (PDF) . S2CID 15694927. Архивировано из оригинала (PDF) 11 ноября 2018 г. . Получено 11 ноября 2018 г. .
- ^ "Automated Theorem Proving" (PDF) . Australian National University College of Engineering & Computer Science . стр. 73–74. Архивировано (PDF) из оригинала 11 ноября 2018 г. . Получено 11 ноября 2018 г. .
- ^ Шнайдер, Майкл; Сатклифф, Джефф (2011). «Рассуждение на языке онтологии OWL 2 Full Ontology с использованием автоматизированного доказательства теорем первого порядка». arXiv : 1108.0155 [cs.AI].
- ^ "The CADE ATP System Competition - The World Championship for Automated Theorem Proving". Победители предыдущего дивизиона CASC. Архивировано из оригинала 1 сентября 2018 года . Получено 7 ноября 2018 года .
