Типы автоматических доказателей теорем

20

Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начинающемся здесь .

Какие релевантные автоматические доказатели теорем? Я нашел обзор доказателей теорем

Это все еще актуально?

Какие из них все еще очень активны, т.е. какие в настоящее время используются за пределами группы, которая их создала?

Найти следующий вопрос серии здесь .

logic automated-theorem-proving proof-assistants Гай Кодер
источник

Ответы:

15

Категоризация в этом списке, безусловно, все еще актуальна.

Возможно, возникла одна новая категория, а именно, языки программирования с зависимой типизацией . Это, по сути, автоматизированные средства доказательства теорем, где основной целью является не доказательство теорем, а программирование. Из-за соответствия Карри-Говарда эти два понятия тесно переплетены. Конечной целью таких языков программирования является написание программ, которые имеют гораздо более строгие гарантии, чем обычные типизированные языки программирования. Люди также используют их для доказательства теорем. Некоторые новые системы, попадающие в эту категорию, включают Agda и Epigram, Одной из ключевых характеристик таких языков является то, что они прикладывают много усилий, чтобы программистам было проще определять индуктивные семейства типов данных. Простым примером является вектор, который зависит от натуральных чисел (определенных индуктивно).

Что касается тех, которые все еще очень активны, я думаю, что они все. Coq , Isabelle , Twelf и PVS часто используются в сообществе языков программирования. Мод широко используется в модельных системах. (Лично я использовал Coq и Мод .)

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

Доказатели теорем, упомянутые в «Обзоре доказательств теорем»:

  • ALF : подчинены ALFA, Coq и Agda.
  • ALFA : кажется, больше не поддерживается.
  • COQ : активно поддерживается.
  • MetaPRL : кажется, больше не поддерживается.
  • NuPRL : активно поддерживается.
  • HOL : активно поддерживается.
  • PVS : активно поддерживается.
  • Изабель : активно поддерживается.
  • Двенадцать : активно поддерживается.
  • ACL2 : активно поддерживается.
  • ИНКА : кажется, больше не поддерживается.
  • ГЭНДАЛЬФ : кажется, больше не поддерживается.
  • TPS : может все еще быть активным, но имеет только небольшое число подписчиков.
  • OTTER : может больше не поддерживаться.
  • SETHEO : заменено на E-SETHEO, которое, похоже, больше не поддерживается.
  • СПАСС : кажется, все еще активен.
  • EQP : кажется, больше не поддерживается.
  • МОД : очень активно поддерживается.
  • ОМЕГА : кажется, больше не поддерживается.
  • Мизар : активно поддерживается.

Несомненно, существует много новых автоматических средств проверки теорем, которые не были упомянуты в этом списке.

Для полноты, как предположил Рафаэль , существуют доказательства архивации сайтов, выполненные с использованием различных инструментов. Например:

Дэйв Кларк
источник
2
Вероятно, полезно ссылаться на (списки) доказательств, где использовались соответствующие инструменты, например, Архив формальных доказательств для Изабель.
Рафаэль
@GuyCoder: по какой-то причине ваши дополнения были удалены. Я добавил их обратно.
Дейв Кларк,
«Некоторые новые системы, попадающие в эту категорию, включают Agda и Epigram.»: Кажется, исчезли. Есть ли новое место для Eprigram? Или близкая альтернатива?
Hibou57
1
«Что касается тех, которые все еще очень активны, я думаю, что они все. Coq, Isabelle, Twelf и PVS »: известно, что у PVS есть ошибки в отношении надежности. В отличие от Изабель и Кок, PVS не соответствует архитектуре микроядра. Найдите критерий де Брюйна, чтобы узнать, почему он важен.
Hibou57
1
Наряду с Agda и (несуществующей?) Epigram, существует язык программирования ATS , который, согласно списку рассылки, по-видимому, активен до 2014 года.
Hibou57