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

Об академической конференции см. Интерактивное доказательство теорем (конференция).
Не путать с Интерактивная система доказательств.
Интерактивный сеанс доказательства в CoqIDE, показывающий сценарий доказательства слева и состояние доказательства справа.

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

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

Смотрите также: Зависимый тип § Сравнение, и Автоматическое доказательство теорем § Сравнение
имяПоследняя версияРазработчики)Язык реализацииособенности
Логика высшего порядкаЗависимые типыМаленькое ядроДоказательство автоматизацииДоказательство отражениемГенерация кода
ACL28.2Мэтт Кауфманн и Дж. Стротер МурCommon LispНетНетипизированныйНетдада[1]Уже исполняемый
Агда2.6.0.1Ульф Норелл, Нильс Андерс Даниэльссон и Андреас Абель (Чалмерс и Гетеборг )HaskellдададаНетЧастичноеУже исполняемый
Альбатрос0.4Гельмут БрандлOCamlдаНетдадаНеизвестноЕще не реализовано
Coq8.11.0INRIAOCamlдададададада
F *хранилищеMicrosoft Research и INRIAF *дадаНетдада[2]да
HOL LightхранилищеДжон ХаррисонOCamlдаНетдадаНетНет
HOL4Кананаскис-13 (или репо)Майкл Норриш, Конрад Слинд и другиеСтандартный MLдаНетдадаНетда
Идрис1.3.3Эдвин БрэдиHaskellдададаНеизвестноЧастичноеУже исполняемый
ИзабельIsabelle2020 (апрель 2020 г.)Ларри Полсон (Кембридж ), Тобиас Нипков (München ) и Макариус ВенцельСтандартный ML, ScalaдаНетдададада
Худойv3.4.2[3]Microsoft ResearchC ++дададададаНеизвестно
ЛЕГО (не связан с компанией LEGO)1.3.1Рэнди Поллак (Эдинбург )Стандартный MLдададаНетНетНет
Мицар8.1.05Белостокский университетFree PascalЧастичноедаНетНетНетНет
NuPRL5Корнелл УниверситетCommon LispдадададаНеизвестнода
ПВС6.0SRI InternationalCommon LispдадаНетдаНетНеизвестно
Двенадцать1.7.1Фрэнк Пфеннинг и Карстен ШюрманнСтандартный MLдадаНеизвестноНетНетНеизвестно
  • ACL2 - язык программирования, логическая теория первого порядка и средство доказательства теорем (с интерактивным и автоматическим режимами) в традиции Бойера – Мура.
  • Coq - который позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации.
  • Средства доказательства теорем HOL - Семейство инструментов, в конечном итоге Инструмент доказательства теорем LCF. В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом взаимодействии с системой. Члены семьи включают:
  • IMPS, Интерактивная система математических доказательств[4]
  • Изабель является интерактивным средством доказательства теорем, преемником HOL. Основная кодовая база лицензируется BSD, но дистрибутив Isabelle включает в себя множество дополнительных инструментов с разными лицензиями.
  • Jape - На основе Java.
  • ЛЕГО
  • Матита - Световая система, основанная на исчислении индуктивных конструкций.
  • MINLOG - Помощник доказательства, основанный на минимальной логике первого порядка.
  • Мицар - Помощник доказательства, основанный на логике первого порядка, в естественный вычет стиль и Теория множеств Тарского – Гротендика.
  • PhoX - Помощник доказательства, основанный на расширяемой логике более высокого порядка.
  • Система проверки прототипа (PVS) - язык и система доказательств, основанная на логике высшего порядка.
  • TPS и ETPS - Интерактивные средства доказательства теорем также основаны на простом типизированном лямбда-исчислении, но на основе независимого формулировка логической теории и самостоятельной реализации.
  • Typelab
  • Тысячелистник

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

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

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

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

Заметки

  1. ^ Хант, Уоррен; Мэтт Кауфманн; Роберт Беллармин Круг; Дж. Мур; Эрик В. Смит (2005). «Мета-рассуждение в ACL2» (PDF). Конспект лекций Springer по информатике. 3603: 163–178.
  2. ^ Ищите "доказательства размышлениями": arXiv:1803.06547
  3. ^ "Страница релизов средства доказательства теорем бережливого производства". GitHub.
  4. ^ Фермер, Уильям М .; Guttman, Joshua D .; Тайер, Ф. Хавьер (1993). «IMPS: интерактивная система математических доказательств». Журнал автоматизированных рассуждений. 11 (2): 213–248. Дои:10.1007 / BF00881906. Получено 22 января 2020.
  5. ^ Венцель, Макариус. "Изабель". Получено 2 ноября 2019.

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

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

Каталоги