Вампир (обеспечивает теорема)

Оригинальный автор(ы)	Andrei Voronkov
Разработчик(и)	Команда вампиров
Стабильная версия	4.5.1 / 2020-07-15
Репозиторий	github .с /vprover /вампир ;
Написано в	С++
Доступно в	модифицированная вампиром Лицензия BSD,
Тип	Автоматизированное доказательство теорем
Веб-сайт	впроверить .github .что

Vampire — это автоматическое средство доказательства теорем для первого порядка, классической логики разработанное на факультете компьютерных наук университета Манчестерского . До версии 3 он был разработан Андреем Воронковым совместно с Криштофом Ходером, а ранее — с Александром Рязановым. Начиная с версии 4, в разработке принимала участие более широкая международная команда, включая Лауру Ковач, Джайлса Регера и Мартина Суда. С 1999 года он выиграл как минимум 53 трофея на системном соревновании CADE ATP , «кубке мира для доказывающих теорем», включая самый престижный дивизион FOF и дивизион TFA с теоретическими рассуждениями. ^[3]^[4]

Предыстория [ править ]

Vampire Ядро реализует вычисления упорядоченного двоичного разрешения и суперпозиции (для обработки равенства). Правило разделения и разделение по отрицательному равенству можно смоделировать путем введения новых определений предикатов и динамического свертывания таких определений. алгоритма в стиле DPLL Также поддерживается разделение . Для сокращения пространства поиска используется ряд стандартных критериев избыточности и методов упрощения: тавтологии удаление , разрешение включения , перезапись с помощью упорядоченных равенств единиц, ограничения базисности и неприводимость терминов замены . Упорядочение редукции по термам представляет собой стандартное упорядочение Кнута-Бендикса .

ряд эффективных методов индексации используется Для реализации всех основных операций над наборами терминов и предложений . Специализация алгоритма времени выполнения используется для ускорения прямого сопоставления.

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

Помимо доказательства теорем, Vampire имеет и другие связанные функции, такие как генерация интерполянтов .

Исполняемые файлы можно получить с сайта системы. ^[5] По состоянию на ноябрь 2020 года Vampire выпускается под модифицированной версией лицензии BSD из 3 пунктов, которая прямо разрешает коммерческое использование. Предыдущие версии были доступны по частной некоммерческой лицензии.

Ссылки [ править ]

^ «История» . vprover.github.io . Проверено 24 мая 2018 г.
^ «Лицензия вампира (Модифицированная BSD)» . vprover.github.io . Проверено 2 ноября 2022 г.
^ Рязанов А.; Воронков, А. (2002). «Проектирование и реализация ВАМПИРА». AI-коммуникации . 15 (2–3/2002): 91–110. ISSN 0921-7126 .
^ Воронков, А. (1995). «Анатомия вампира». Журнал автоматизированного рассуждения . 15 (2): 237–265. дои : 10.1007/BF00881918 . S2CID 1541122 .
^ «Вампир» . vprover.github.io . Проверено 2 ноября 2022 г.

Внешние ссылки [ править ]

Официальный сайт

Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

Эта о бесплатном программном обеспечении с открытым исходным кодом статья незавершена . Вы можете помочь Википедии, расширив ее .

[1] «История» . vprover.github.io . Проверено 24 мая 2018 г.

[2] «Лицензия вампира (Модифицированная BSD)» . vprover.github.io . Проверено 2 ноября 2022 г.

[riaznov-3] Рязанов А.; Воронков, А. (2002). «Проектирование и реализация ВАМПИРА». AI-коммуникации . 15 (2–3/2002): 91–110. ISSN 0921-7126 .

[4] Воронков, А. (1995). «Анатомия вампира». Журнал автоматизированного рассуждения . 15 (2): 237–265. дои : 10.1007/BF00881918 . S2CID 1541122 .

[5] «Вампир» . vprover.github.io . Проверено 2 ноября 2022 г.

[1]

[2]

[3]

[4]

[5]