И (обеспечивает теорема)
E — это высокопроизводительное средство доказательства теорем для полной логики первого порядка с равенством. [1] Он основан на эквационном исчислении суперпозиции и использует чисто эквациональную парадигму. Она была интегрирована в другие средства доказательства теорем и вошла в число лучших систем на нескольких конкурсах по доказательству теорем. E разработан Стефаном Шульцем, первоначально работавшим в группе автоматического рассуждения , Мюнхенского технического университета а сейчас в Кооперативном государственном университете Баден-Вюртемберга в Штутгарте.
Система [ править ]
Система основана на эквационном исчислении суперпозиции . В отличие от большинства других современных пруверов, реализация фактически использует чисто эквациональную парадигму и моделирует неэквациональные выводы посредством соответствующих выводов равенства. Значительные инновации включают в себя переписывание общих терминов (когда множество возможных эквациональных упрощений выполняется за одну операцию), [2] несколько эффективных структур данных индексации терминов для ускорения вывода, расширенные стратегии выбора литералов вывода и различные варианты использования методов машинного обучения для улучшения поведения поиска. [2] [3] [4] Начиная с версии 2.0, E поддерживает многосортную логику . [5]
E реализован на языке C и переносится на большинство вариантов UNIX и среду Cygwin . Он доступен под лицензией GNU GPL . [6]
Соревнования [ править ]
Система прувера стабильно показывает хорошие результаты в системном конкурсе CADE ATP , выиграв категорию CNF/MIX в 2000 году и с тех пор входя в число лучших систем. [7] В 2008 году он занял второе место. [8] В 2009 году он занял второе место в категориях FOF (полная логика первого порядка) и UEQ (единичная эквациональная логика) и третье место (после двух версий Vampire ) в CNF (клаузальная логика). [9] Она повторила свои результаты в FOF и CNF в 2010 году и получила специальную награду как «лучшая в целом» система. [10] В 2011 году CASC-23 E выиграл дивизион CNF и занял вторые места в UEQ и LTB. [11]
Приложения [ править ]
E был интегрирован в несколько других средств доказательства теорем. он лежит Вместе с Vampire , SPASS , CVC4 и Z3 в основе стратегии Изабель « Кувалда » . [12] [13] E также является механизмом рассуждения в SInE. [14] и ЛЕО-II [15] и используется в качестве системы классификации для iProver. [16]
Приложения E включают рассуждения о больших онтологиях, [17] проверка программного обеспечения, [18] и сертификация программного обеспечения. [19]
Ссылки [ править ]
- ^ Шульц, Стефан (2002). «E - Средство доказательства теорем Брейниака». Журнал искусственных коммуникаций . 15 (2/3): 111–126.
- ^ Jump up to: а б Шульц, Стефан (2008). «Описания системы для участников: E 1.0pre и EP 1.0pre» . Архивировано из оригинала 15 июня 2009 года . Проверено 24 марта 2009 г.
- ^ Шульц, Стефан (2004). «Описание системы: E 0,81». Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 3097. стр. 223–228. дои : 10.1007/978-3-540-25984-8_15 . ISBN 978-3-540-22345-0 .
- ^ Шульц, Стефан (2001). «Изучение знаний по управлению поиском для доказательства теорем». КИ 2001: Достижения в области искусственного интеллекта . Конспекты лекций по информатике. Том. 2174. стр. 320–334. дои : 10.1007/3-540-45422-5_23 . ISBN 978-3-540-42612-7 .
- ^ «новости на сайте E» . Проверено 10 июля 2017 г.
- ^ Шульц, Стефан (2008). «Средство доказательства теоремы для уравнений E» . Проверено 24 марта 2009 г.
- ^ Сатклифф, Джефф. «Соревнования по системе CADE ATP» . Архивировано из оригинала 2 марта 2009 года . Проверено 24 марта 2009 г.
- ^ «Подразделение ФОФ ЦАСК в 2008 году» . Архивировано из оригинала 15 июня 2009 года . Проверено 19 декабря 2009 г.
- ^ Сатклифф, Джефф (2009). «Четвертый конкурс автоматизированных систем доказательства теорем IJCAR — CASC-J4» . AI-коммуникации . 22 (1): 59–72. дои : 10.3233/AIC-2009-0441 . Проверено 16 декабря 2009 г.
- ^ Сатклифф, Джефф (2010). «Соревнования по системе CADE ATP» . Университет Майами. Архивировано из оригинала 29 июня 2010 года . Проверено 20 июля 2010 г.
- ^ Сатклифф, Джефф (2011). «Соревнования по системе CADE ATP» . Университет Майами. Архивировано из оригинала 12 августа 2011 года . Проверено 14 августа 2011 г.
- ^ Полсон, Лоуренс К. (2008). «Автоматизация интерактивных доказательств: методы, уроки и перспективы» (PDF) . Инструменты и методы проверки системной инфраструктуры – Фестиваль в честь профессора Майкла Дж. К. Гордона FRS : 29–30 . Проверено 19 декабря 2009 г.
- ^ Мэн, Цзя; Лоуренс К. Полсон (2004). Эксперименты по поддержке интерактивного доказательства с использованием разрешения . Конспекты лекций по информатике. Том. 3097. Спрингер. стр. 372–384. CiteSeerX 10.1.1.62.5009 . дои : 10.1007/978-3-540-25984-8_28 . ISBN 978-3-540-22345-0 .
- ^ Сатклифф, Джефф; и др. (2009). 4-е соревнование IJCAR по системе ATP (PDF) . Архивировано из оригинала (PDF) 17 июня 2009 года . Проверено 18 декабря 2009 г.
- ^ Бенцмюллер, Кристоф; Лоуренс К. Полсон; Фрэнк Тайсс; Арно Фицке (2008). «LEO-II - Кооперативное автоматическое средство доказательства теорем для классической логики высшего порядка (описание системы)». Автоматизированное рассуждение (PDF) . Конспекты лекций по информатике. Том. 5195. Спрингер. стр. 162–170. дои : 10.1007/978-3-540-71070-7_14 . ISBN 978-3-540-71069-1 . Архивировано из оригинала (PDF) 15 июня 2011 года . Проверено 20 декабря 2009 г.
- ^ Коровин, Константин (2008). «iProver — средство доказательства теорем для логики первого порядка, основанное на реализации экземпляров». Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 5195. стр. 292–298. дои : 10.1007/978-3-540-71070-7_24 . ISBN 978-3-540-71069-1 .
- ^ Рамачандран, Дипак; Пейс Рейган; Кейт Гулсбери (2005). «Первосортный ResearchCyc: выразительность и эффективность в онтологии здравого смысла» (PDF) . Семинар AAAI по контекстам и онтологиям: теория, практика и приложения . АААИ.
- ^ Ранисе, Сильвио; Дэвид Дехарб (2003). «Применение доказательства облегченной теоремы для отладки и проверки программ с указателями» . Электронные заметки по теоретической информатике . 86 (1). 4-й международный семинар по доказательству теорем первого порядка: Elsevier: 109–119. дои : 10.1016/S1571-0661(04)80656-X .
{{cite journal}}: CS1 maint: местоположение ( ссылка ) - ^ Денни, Юэн; Бернд Фишер; Йохан Шуман (2006). «Эмпирическая оценка автоматизированных средств доказательства теорем при сертификации программного обеспечения» . Международный журнал по инструментам искусственного интеллекта . 15 (1): 81–107. CiteSeerX 10.1.1.163.4861 . дои : 10.1142/s0218213006002576 . Архивировано из оригинала 24 февраля 2012 года . Проверено 19 декабря 2009 г.