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

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

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

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

• ACL2  - язык программирования, логическая теория первого порядка и средство доказательства теорем (с интерактивным и автоматическим режимами) в традиции Бойера – Мура.
• Coq  - который позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации.
• Устройство доказательства теорем HOL  - семейство инструментов, в конечном итоге созданное на основе средства доказательства теорем LCF . В этих системах логическим ядром является библиотека их языка программирования. Теоремы представляют собой новые элементы языка и могут быть введены только с помощью «стратегий», которые гарантируют логическую корректность. Составление стратегии дает пользователям возможность создавать важные доказательства при относительно небольшом взаимодействии с системой. Члены семьи включают:
  • HOL4  - «основной потомок», все еще находится в стадии активной разработки. Поддержка как Moscow ML, так и Poly / ML . Имеет лицензию в стиле BSD .
  • HOL Light  - процветающая «минималистичная вилка». На основе OCaml .
  • ProofPower  - стал проприетарным, затем вернулся к открытому исходному коду . На основе Standard ML .
• 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.

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

• Автоматическое доказательство теорем
• Компьютерное доказательство
• Манифест QED
• Формальная проверка
• Выполнимость по модулю теорий
• Metamath  - язык для разработки формализованной математики, сопровождаемый средством проверки доказательств для этого языка и несколькими базами данных с тысячами доказанных теорем.

Ноты

Ссылки

• Хенк Барендрегт и Герман Гёверс (2001). «Доказательства-помощники, использующие системы зависимых типов» . В Справочнике по автоматизированному мышлению .
• Фрэнк Пфеннинг (2001). «Логические рамки» . В Справочнике по автоматизированному мышлению .
• Фрэнк Пфеннинг (1996). «Практика логических рамок».
• Роберт Л. Констебль (1998). «Виды информатики, философии и логики». В Справочнике по теории доказательств .
• Х. Гёверс. « Доказательства помощников: история, идеи и будущее ».
• Freek Wiedijk. " Семнадцать испытателей мира "

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

• «Введение» в сертифицированное программирование с зависимыми типами .
• Введение в Coq Proof Assistant (с общим введением в интерактивное доказательство теорем)
• Интерактивное доказательство теорем для пользователей Agda
• Список инструментов для доказательства теорем

Каталоги

• Цифровая математика по категориям: Доказательства тактики
• Системы и группы автоматизированных выводов
• Системы доказательства теорем и автоматизированные системы рассуждений
• База данных существующих механизированных систем рассуждений
• NuPRL: Другие системы
• Конкретные логические структуры и реализации
• DMOZ : Наука: Математика: Логика и основы: Вычислительная логика: Логические основы