 | В этой статье слишком много ссылок на первоисточники . ( Май 2018 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
 | Эта статья может быть слишком технической, чтобы ее могло понять большинство читателей . ( Декабрь 2009 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
| Автор (ы) оригинала | Андрей Воронков [1] |
|---|---|
| Разработчики) | Команда вампиров |
| Стабильный выпуск | 4,4 / 2019-08-24 |
| Репозиторий |  |
| Написано в | C ++ |
| Доступно в | Лицензия вампира [2] |
| Тип | Автоматическое доказательство теорем |
| Интернет сайт | Впровер |
Вампир является автоматической теоремой доказывающим для первого порядка классической логики , разработанной в Департаменте компьютерных наук в Университете Манчестера . До версии 3 он разрабатывался Андреем Воронковым совместно с Криштофом Ходером, а ранее - с Александром Рязановым. Начиная с версии 4, в разработке участвовала более широкая международная команда, в том числе Лаура Ковач, Джайлс Регер и Мартин Суда. С 1999 года он выиграл по меньшей мере 53 трофея на «чемпионате мира по доказательству теорем» (соревнование CADE ATP System Competition ), включая наиболее престижное подразделение FOF и подразделение TFA по теоретическому обоснованию. [3] [4]
Фон [ править ]
Ядро Vampire реализует исчисления упорядоченного двоичного разрешения и суперпозиции для обработки равенства. Правило разделения и разделение отрицательного равенства можно смоделировать путем введения новых определений предикатов и динамического сворачивания таких определений. Алгоритм DPLL стиле расщепления также поддерживается. Для сокращения пространства поиска используется ряд стандартных критериев избыточности и методов упрощения: удаление тавтологии , разрешение подчинения , переписывание с помощью упорядоченных равенств единиц, ограничения базисности и несократимость условий замены. Используемый порядок редукции является стандартным порядком Кнута – Бендикса .
Для реализации всех основных операций над наборами терминов и предложений используется ряд эффективных методов индексирования . Специализация алгоритма времени выполнения используется для ускорения прямого сопоставления.
Хотя ядро системы работает только с клаузальными нормальными формами, компонент препроцессора принимает проблему в полном синтаксисе логики первого порядка, классифицирует ее и выполняет ряд полезных преобразований перед передачей результата в ядро. Когда теорема доказана, система производит поддающееся проверке доказательство, которое подтверждает как фазу клаузификации, так и опровержение конъюнктивной нормальной формы .
Помимо доказательства теорем, Vampire имеет и другие связанные функции, такие как создание интерполянтов .
Исполняемые файлы можно получить на сайте системы. [5] Несколько устаревшая версия доступна под Стандартной общественной лицензией ограниченного применения GNU как часть Sigma KEE . [6]
Ссылки [ править ]
- ^ «История» . vprover.github.io . Проверено 24 мая 2018 .
- ^ "Лицензия вампира" . vprover.github.io . Проверено 24 мая 2018 .
- ^ Рязанов, А .; Воронков, А. (2002). «Дизайн и реализация ВАМПИРА». AI Communications . 15 (2-3 / 2002): 91–110. ISSN 0921-7126 .
- ↑ Воронков, А. (1995). «Анатомия вампира». Журнал автоматизированных рассуждений . 15 (2): 237–265. DOI : 10.1007 / BF00881918 .
- ^ "Вампир" . vprover.github.io . Проверено 24 мая 2018 .
- ^ "CVS-информация для проекта sigmakee" . sigmakee.cvs.sourceforge.net . Проверено 24 мая 2018 .
Внешние ссылки [ править ]
- Официальный веб-сайт
