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

От / / Оставьте комментарий

Вампир (доказательство теоремы) Обзор Vampire Vampire — это автоматическое средство доказательства теорем для классической логики первого порядка.  Разработано на факультете […]

Department of Computer Science, Free and open-source software stubs, Free software programmed in C++, Logic stubs, Software using the BSD license, Theorem proving software systems, University of Manchester, Бесплатное программное обеспечение, Департамент компьютерных наук Манчестерского университета, Заглушки бесплатного программного обеспечения и программного обеспечения с открытым исходным кодом, использующее лицензию BSD, Логические заглушки, написанное на C++., Программное обеспечение, Программные системы для доказательства теорем

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

  • Обзор Vampire

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

  • Ядро Vampire

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

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

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

  • Функции Vampire

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

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

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

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

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

Полный текст статьи:

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

Похожие статьи:

  1. Калифорнийские полимустанги Мустанги Кэл-Поли История Калифорнийского политехнического университета Основан в 1894 году, является государственным университетом.  Расположен в городе...
  2. Вспомогательная функция Вспомогательная функция Интерполяционные определители и их применение Интерполяционные определители — это многочлены, которые используются для интерполяции...
  3. Предикат (грамматика) Сказуемое (грамматика) Одушевленность и падежи Одушевленность: существительные могут быть одушевленными или неодушевленными.  Дательный падеж: изменение падежа...
  4. Калифорнийский университет в Лос-Анджелесе Брюинз Лос-Анджелес Брюинз История Калифорнийского университета в Лос-Анджелесе Калифорнийский университет в Лос-Анджелесе был основан в 1880 году...
  5. Список рекордов НХЛ (команда) Список рекордов НХЛ (команды) Рекорды НХЛ «Монреаль Канадиенс» — самая титулованная команда с 24 Кубками Стэнли. ...
  6. E (теорема обеспечивает) E (доказательство теоремы) Обзор системы E E — инструмент для доказательства теорем в полной логике первого...
  7. Теорема Диаконеску Теорема Дьяконеску Основы конструктивного анализа Конструктивный анализ — это математическая теория, которая использует конструктивные методы для...
  8. Логика второго порядка Логика второго порядка Логика второго порядка — это расширение логики первого порядка, позволяющее количественно оценивать свойства...
  9. Профессионализм в области разработки программного обеспечения Профессионализм в разработке программного обеспечения Профессиональное лицензирование в разработке программного обеспечения Профессиональное лицензирование в разработке ПО...
  10. Логика высшего порядка Логика высшего порядка Логика высшего порядка (HOL) отличается от логики первого порядка дополнительными квантификаторами и более...
  11. Регулирование и лицензирование в области машиностроения Регулирование и лицензирование в области машиностроения Общие сведения о лицензировании инженеров В разных странах существуют различные...
  12. Описательная теория сложности Описательная теория сложности Основы логики первого порядка Логика первого порядка (FO) — это формальная система, которая...
  13. Логика первого порядка Логика первого порядка Определение логики первого порядка Логика первого порядка — это формальная система, которая включает...
  14. Логика первого порядка Логика первого порядка Определение логики первого порядка Логика первого порядка — это формальная система, которая включает...
  15. Аризона Уайлдкэтс Аризонские дикие кошки История и достижения Университета Аризоны Университет Аризоны был основан в 1885 году и...
  16. Автоматическое доказательство теорем Автоматизированное доказательство теоремы Автоматизированные системы проверки теорем используются для решения математических задач.  Теории первого порядка, такие...
  17. Калифорнийский штат Бейкерсфилд Роудраннерс Калифорнийский университет Бейкерсфилд Роудраннерс История и достижения Калифорнийского государственного университета в Бейкерсфилде CSU Bakersfield — университет,...
  18. Стратегия сокращения Стратегия сокращения выбросов Основы лямбда-исчисления Лямбда-исчисление — это формальное исчисление, основанное на лямбда-абстракции и рекурсии.  Редукция...
  19. Непервая упорядочиваемость Невозможность предварительной настройки Определение непервоначальной упорядочиваемости Утверждение не может быть адекватно зафиксировано формулой логики первого порядка. ...
  20. Описательная теория сложности Описательная теория сложности Основы логики первого порядка Логика первого порядка (FO) — это формальная система, которая...
  21. Логика первого порядка Логика первого порядка Логика первого порядка — формальная система для описания и доказательства утверждений.  Язык логики...
  22. Многозначная логика Многозначная логика Определение и история многозначной логики Многозначная логика — это формальная система, которая позволяет использовать...

Оставьте комментарий

Прокрутить вверх