В информатике и математической логике помощник по доказательству или интерактивное средство доказательства теорем - это программный инструмент, который помогает в разработке формальных доказательств путем взаимодействия человека и машины. Это включает в себя какой - то редактор интерактивного доказательства или другой интерфейс , с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в, и некоторые шаги , предлагаемые, компьютера .
Сравнение систем
Имя | Последняя версия | Разработчики) | Язык реализации | Функции | |||||
---|---|---|---|---|---|---|---|---|---|
Логика высшего порядка | Зависимые типы | Маленькое ядро | Доказательство автоматизации | Доказательство отражением | Генерация кода | ||||
ACL2 | 8,3 | Мэтт Кауфманн и Джей Стротер Мур | Common Lisp | Нет | Нетипизированный | Нет | да | Да [1] | Уже исполняемый |
Агда | 2.6.0.1 | Ульф Норелл, Нильс Андерс Даниэльссон и Андреас Абель ( Чалмерс и Гётеборг ) | Haskell | да | да | да | Нет | Частичное | Уже исполняемый |
Альбатрос | 0,4 | Гельмут Брандл | OCaml | да | Нет | да | да | Неизвестный | Еще не реализовано |
Coq | 8.11.0 | INRIA | OCaml | да | да | да | да | да | да |
F * | хранилище | Microsoft Research и INRIA | F * | да | да | Нет | да | Да [2] | да |
HOL Light | хранилище | Джон Харрисон | OCaml | да | Нет | да | да | Нет | Нет |
HOL4 | Кананаскис-13 (или репо) | Майкл Норриш, Конрад Слинд и другие | Стандартный ML | да | Нет | да | да | Нет | да |
Идрис | 2 0.3.0. | Эдвин Брэди | Идрис | да | да | да | Неизвестный | Частичное | да |
Изабель | Isabelle2021 (февраль 2021 г.) | Ларри Полсон ( Кембридж ), Тобиас Нипков ( Мюнхен ) и Макариус Венцель | Стандартный ML , Scala | да | Нет | да | да | да | да |
Худой | v3.4.2 [3] | 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 . В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства с относительно небольшим количеством взаимодействий с системой. Члены семьи включают:
- HOL4 - «основной потомок», все еще находится в стадии активной разработки. Поддержка как Moscow ML, так и Poly / ML . Имеет лицензию в стиле BSD .
- HOL Light - процветающая «минималистичная вилка». На основе OCaml .
- ProofPower - стал проприетарным, затем вернулся к открытым исходным кодом. На основе Standard ML .
- IMPS, интерактивная система математических доказательств [4]
- Изабель - интерактивная программа доказательства теорем, преемница 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. [5]
Смотрите также
- Автоматическое доказательство теорем
- Компьютерное доказательство
- Манифест QED
- Формальная проверка
- Выполнимость по модулю теорий
- Metamath - язык для разработки формализованной математики, сопровождаемый средством проверки доказательств для этого языка и несколькими базами данных с тысячами доказанных теорем.
Заметки
- ^ Хант, Уоррен; Мэтт Кауфманн; Роберт Беллармин Круг; Дж. Мур; Эрик В. Смит (2005). «Мета-рассуждение в ACL2» (PDF) . Доказательство теорем в логиках высокого порядка . Конспект лекций по информатике. 3603 . С. 163–178. DOI : 10.1007 / 11541868_11 . ISBN 978-3-540-28372-0.
- ^ Найдите "доказательства по размышлению": arXiv : 1803.06547
- ^ "Страница релизов средства доказательства теорем бережливого производства" . GitHub .
- ^ Фермер, Уильям М .; Guttman, Joshua D .; Тайер, Ф. Хавьер (1993). «IMPS: интерактивная система математических доказательств» . Журнал автоматизированных рассуждений . 11 (2): 213–248. DOI : 10.1007 / BF00881906 . S2CID 3084322 . Проверено 22 января 2020 года .
- ^ Венцель, Макариус. «Изабель» . Дата обращения 2 ноября 2019 .
Рекомендации
- Хенк Барендрегт и Герман Гёверс (2001). «Доказательства-помощники, использующие системы зависимых типов» . В Справочнике по автоматизированному мышлению .
- Фрэнк Пфеннинг (2001). «Логические рамки» . В Справочнике по автоматизированному мышлению .
- Фрэнк Пфеннинг (1996). «Практика логических рамок».
- Роберт Л. Констебль (1998). «Виды информатики, философии и логики». В Справочнике по теории доказательств .
- Х. Гёверс. « Доказательства помощников: история, идеи и будущее ».
- Freek Wiedijk. " Семнадцать испытателей мира "
Внешние ссылки
- «Введение» в сертифицированное программирование с зависимыми типами .
- Введение в Coq Proof Assistant (с общим введением в интерактивное доказательство теорем)
- Интерактивное доказательство теорем для пользователей Agda
- Список инструментов для доказательства теорем
- Каталоги
- Цифровая математика по категориям: Доказательства тактики
- Автоматизированные системы и группы дедукции
- Системы доказательства теорем и автоматизированные системы рассуждений
- База данных существующих механизированных систем рассуждений
- NuPRL: Другие системы
- Конкретные логические структуры и реализации
- DMOZ : Наука: Математика: Логика и основы: Вычислительная логика: Логические основы