Вампир (доказательство теоремы)

• Обзор Vampire

  • Vampire – это автоматическое средство доказательства теорем для классической логики первого порядка. 
  • Разработано на факультете компьютерных наук Манчестерского университета, начиная с версии 4 в разработке участвовала международная команда. 
  • С 1999 года команда выиграла множество трофеев в соревнованиях по системе CADE ATP. 

• Ядро Vampire

  • Реализует вычисления упорядоченного двоичного разрешения и суперпозиции. 
  • Поддерживает разделение по алгоритму в стиле DPLL. 
  • Использует стандартные критерии избыточности и методы упрощения для сокращения пространства поиска. 
  • Применяет стандартный порядок Кнута-Бендикса для сокращения сроков. 
  • Эффективные методы индексации используются для выполнения основных операций с терминами и предложениями. 

• Компонент препроцессора

  • Принимает проблему в полном синтаксисе логики первого порядка и выполняет полезные преобразования перед передачей ядру. 

• Функции Vampire

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

• Доступность и лицензирование

  • Исполняемые файлы доступны на веб-сайте системы. 
  • С ноября 2020 года Vampire выпускается под измененной версией лицензии BSD 3-clause, разрешающей коммерческое использование. 

• Рекомендации

  • Статья является заглушкой и предлагает помощь в расширении Википедии.