Доказательство помощника - Proof assistant

Интерактивный сеанс доказательства в CoqIDE, показывающий сценарий доказательства слева и состояние доказательства справа.

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

Сравнение систем

Имя Последняя версия Разработчики) Язык реализации Функции
Логика высшего порядка Зависимые типы Маленькое ядро Доказательство автоматизации Доказательство отражением Генерация кода
ACL2 8,3 Мэтт Кауфманн и Джей Стротер Мур Common Lisp Нет Нетипизированный Нет да да Уже исполняемый
Агда 2.6.2 Ульф Норелл, Нильс Андерс Даниэльссон и Андреас Абель ( Чалмерс и Гётеборг ) Haskell да да да Нет Частичное Уже исполняемый
Альбатрос 0,4 Гельмут Брандл OCaml да Нет да да Неизвестный Еще не реализовано
Coq 8.13.2 INRIA OCaml да да да да да да
F * хранилище Microsoft Research и INRIA F * да да Нет да да да
HOL Light хранилище Джон Харрисон OCaml да Нет да да Нет Нет
HOL4 Кананаскис-13 (или репо) Майкл Норриш, Конрад Слинд и другие Стандартный ML да Нет да да Нет да
Идрис 2 0.4.0. Эдвин Брэди Идрис да да да Неизвестный Частичное да
Изабель Isabelle2021 (февраль 2021 г.) Ларри Полсон ( Кембридж ), Тобиас Нипков ( Мюнхен ) и Макариус Венцель Стандартный ML , Scala да Нет да да да да
Наклонять v3.4.2 Microsoft Research C ++ да да да да да Неизвестный
LEGO (не связан с Lego ) 1.3.1 Рэнди Поллак ( Эдинбург ) Стандартный ML да да да Нет Нет Нет
Мицар 8.1.05 Белостокский университет Свободный Паскаль Частичное да Нет Нет Нет Нет
NuPRL 5 Cornell University Common Lisp да да да да Неизвестный да
ПВС 6.0 SRI International Common Lisp да да Нет да Нет Неизвестный
Двенадцать 1.7.1 Франк Пфеннинг и Карстен Шюрманн Стандартный ML да да Неизвестный Нет Нет Неизвестный
  • ACL2  - язык программирования, логическая теория первого порядка и средство доказательства теорем (с интерактивным и автоматическим режимами) в традиции Бойера – Мура.
  • Coq  - который позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации.
  • Программа доказательства теорем HOL  - семейство инструментов, в конечном итоге созданных на основе средства доказательства теорем LCF . В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», гарантирующих логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства с относительно небольшим количеством взаимодействий с системой. Члены семьи включают:
  • IMPS, интерактивная система математических доказательств
  • Изабель - интерактивная программа доказательства теорем, преемница HOL. Основная кодовая база лицензируется BSD, но в дистрибутив Isabelle входит множество дополнительных инструментов с разными лицензиями.
  • Jape  - на основе Java.
  • Наклонять
  • ЛЕГО
  • Matita  - система освещения, основанная на исчислении индуктивных конструкций.
  • MINLOG  - Помощник доказательства, основанный на минимальной логике первого порядка.
  • Мицар  - Помощник по доказательству, основанный на логике первого порядка, в стиле естественной дедукции и теории множеств Тарского – Гротендика .
  • PhoX  - помощник по доказательству, основанный на расширяемой логике высшего порядка.
  • Система проверки прототипов (PVS) - язык и система доказательств, основанная на логике высшего порядка.
  • TPS и ETPS  - Интерактивные средства доказательства теорем также основаны на просто типизированном лямбда-исчислении, но основаны на независимой формулировке логической теории и независимой реализации.
  • Typelab
  • Тысячелистник

Музей средства доказательства теорем - это инициатива по сохранению источников систем доказательства теорем для будущего анализа, поскольку они являются важными культурными / научными артефактами. Он имеет источники многих из упомянутых выше систем.

Пользовательские интерфейсы

Популярным интерфейсом для помощников по доказательству является основанная на Emacs Proof General, разработанная в Эдинбургском университете . Coq включает CoqIDE, основанный на OCaml / Gtk . Isabelle включает Isabelle / jEdit, основанную на jEdit, и инфраструктуру Isabelle / Scala для обработки документов, ориентированных на проверку. Совсем недавно Макариус Венцель разработал расширение Visual Studio Code для Isabelle.

Смотрите также

Примечания

использованная литература

внешние ссылки

Каталоги