Вампир (доказатель теорем) - Vampire (theorem prover)
| Автор (ы) оригинала | Андрей Воронков |
|---|---|
| Разработчики) | Команда вампиров |
| Стабильный выпуск | 4.5.1 / 2020-07-15 |
| Репозиторий |
|
| Написано в | C ++ |
| Доступно в | Лицензия вампира |
| Тип | Автоматическое доказательство теорем |
| Веб-сайт | Впровер |
Вампир является автоматической теоремой доказывающим для первого порядка классической логики , разработанной в Департаменте компьютерных наук в Университете Манчестера . До версии 3 он разрабатывался Андреем Воронковым совместно с Криштофом Ходером, а ранее - с Александром Рязановым. Начиная с версии 4, в разработке участвовала более широкая международная команда, в том числе Лаура Ковач, Джайлс Регер и Мартин Суда. С 1999 года он выиграл по меньшей мере 53 трофея на «чемпионате мира по доказательству теорем» (соревнование CADE ATP System Competition ), включая наиболее престижное подразделение FOF и подразделение TFA по теоретическому обоснованию.
Задний план
Ядро Vampire реализует исчисления упорядоченного двоичного разрешения и суперпозиции для обработки равенства. Правило разделения и разделение отрицательного равенства можно смоделировать путем введения новых определений предикатов и динамического сворачивания таких определений. Алгоритм DPLL стиле расщепления также поддерживается. Для сокращения пространства поиска используется ряд стандартных критериев избыточности и методов упрощения: удаление тавтологии , разрешение подчинения , переписывание с помощью упорядоченных равенств единиц, ограничения базисности и несводимость условий замены. Используемый порядок редукции является стандартным порядком Кнута – Бендикса .
Для реализации всех основных операций над наборами терминов и предложений используется ряд эффективных методов индексирования . Специализация алгоритма времени выполнения используется для ускорения прямого сопоставления.
Хотя ядро системы работает только с клаузальными нормальными формами, компонент препроцессора принимает проблему в полном синтаксисе логики первого порядка, классифицирует ее и выполняет ряд полезных преобразований перед передачей результата в ядро. Когда теорема доказана, система производит поддающееся проверке доказательство, которое подтверждает как фазу клаузификации, так и опровержение конъюнктивной нормальной формы .
Помимо доказательства теорем, Vampire имеет и другие связанные функции, такие как создание интерполянтов .
Исполняемые файлы можно получить на сайте системы. Несколько устаревшая версия доступна под Стандартной общественной лицензией ограниченного применения GNU как часть Sigma KEE .
Рекомендации
Внешние ссылки
 |
Эта статья о логике - незавершенная . Вы можете помочь Википедии, расширив ее . |