Автоматизированное доказательство теорем

44

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

Обратите внимание, что эти темы нелегко усваиваются без знания (математической) логики. Если у вас есть проблемы с основными терминами, пожалуйста, ознакомьтесь с ними, например, « Логика в информатике » М. Хута и М. Райана (в частности, главы 1, 2 и 4) или «Введение в математическую логику и теорию типов » П. Эндрюс.
Краткое введение в логику высшего порядка (HOL) смотрите здесь .

Я посмотрел на Кока и прочитал первую главу введения в Изабель среди других; Типы автоматических доказателей теорем

Я знаю Пролог несколько десятилетий и сейчас изучаю F #, поэтому ML, O'Caml и LISP - это бонус. Хаскелл другой зверь.

У меня есть следующие книги

«Справочник по автоматическому мышлению» под редакцией Алана Робинсона и Андрея Ворнкова

«Справочник по практической логике и автоматическому рассуждению» Джона Харрисона

«Переписывание терминов и все такое» Франца Баадера и Тобиаса Нипкова

  1. Каковы различия между Кок и Изабель?

  2. Должен ли я учить Изабель или Coq, или оба?

  3. Есть ли преимущество в том, чтобы сначала изучать Изабель или Кока?

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

Гай Кодер
источник
7
Важно отметить, что инструменты, о которых вы говорите, - это не автоматические проверяющие, а вспомогательные помощники (хотя сами по себе они могут легко доказать).
Рафаэль
@DaveClarke Дублировать?
Рафаэль
@ Рафаэль: Да (кроме теперь мой ответ содержит новые данные).
Дейв Кларк
@DaveClarke Как вы думаете, мы должны закрыть это и объединить два?
Рафаэль
@ Рафаэль: Да. Я только что скопировал текст ответа здесь в мой ответ на другой вопрос.
Дейв Кларк

Ответы:

25

Я предпочитаю Coq, но я думаю, что другие предпочитают Изабель. Одна из странных вещей, которые я обнаружил в Изабель, заключается в том, что существует двухуровневый синтаксис, где некоторые из ваших определений должны быть заключены в двойные кавычки. Нет такой ерунды в Coq.

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

Одна из стратегий состоит в том, чтобы сделать простое учебное пособие на обоих языках и следовать тому, которое кажется лучшим. Например,

Вот сообщение в блоге, в котором кратко сравниваются два человека, который в конечном итоге предпочитает Изабель.

Убедитесь, что вы используете правильную IDE (например, ProofGeneral ), а не выполняете действия в командной строке.

Еще один способ попасть в Coq - попробовать онлайн-книгу « Основы программного обеспечения» Бенджамина Пирса и др. Он предоставляет отличный учебник с множеством предоставленных деталей. Основное внимание уделяется семантике языка программирования, но многие основы (и более) Coq и полуавтоматического доказательства теорем рассматриваются на этом пути.

Дэйв Кларк
источник
4
ProofGeneral - это круто, как только вы его приручите! Что касается синтаксиса Изабель: iirc, вещи в двойных кавычках - это то, о чем вы говорите, формулы. Все остальное - контрольный контроль. Хотя четкое различие было неплохим, но двойные кавычки (и, как следствие, отсутствие подсветки синтаксиса внутри кавычек), вероятно, не лучший способ реализовать это.
Рафаэль
4
В прошлом году мы создали вики Isabelle / HOL для курса; у этого есть некоторые хорошие обзоры, трудно найти иначе.
Рафаэль
18

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

Когда я впервые начал изучать теорию, связанную с доказательством теорем, первой книгой, которую я прочитал (хотя и довольно устарел?), Была отличная логика Мелвина Фиттинга первого порядка и автоматическое доказательство теорем. Эта книга была действительно превосходной, в ней были рассмотрены темы, которые вы увидите, связанные с логикой низшего порядка, где вы действительно можете получить достаточную автоматизацию. Тип логики, которую вы изучаете, должен быть продиктован тем, о чем вы хотите рассуждать, а не столько теоремой, доказывающей ради этого. Например, в то время как логика первого порядка дает вам достаточную выразительность и способность к рассуждению, большинство сообщества языков программирования (где я попал в эти дни) отошло от более старой школы доказательства теорем и проверки моделей (которые входят в ведро вещей, которые более разрешимы, но менее выразительны).

Однако не следует понимать, что такие вещи, как рассуждения первого порядка и проверка моделей, не были чрезвычайно полезны на практике. Они были! Вы можете взглянуть на ACL2 как на пример испытателя, построенного на основе логики первого порядка, который добился удивительного успеха в промышленной сфере. Наряду с этим, было также удивительное количество развития в решении SMT. Современные решатели SMT построены на основе очень мощных решателей SAT (в основном, благодаря открытиям в течение последних двадцати лет для улучшений DPLL) и нашли широкое применение в таких вещах, как символьное выполнение.

Однако, как я уже сказал, хотя более традиционное «доказательство теорем» - это весело, есть еще много чего нужно выучить. Например, изучение Coq имеет мало общего с изучением инструментов автоматизации, которые оно дает вам, и имеет гораздо больше общего с изучением теории типов, на которой она основана (исчисление предикатов коиндуктивных конструкций). Если вы не привыкли к конструктивной логике, изоморфизму Карри Ховарда или теории типов, вам будет интересно изучать эти инструменты, но я с трудом могу подумать, что они слишком тесно связаны с тем, что вы видите в первом томе. из справочника.

Так что решайте, что вы хотите сделать: проверяйте модели и теоремы в логике первого порядка или используйте мощную теорию типов, чтобы рассуждать о правильности ваших программ (или теорем в конструктивной логике). Если это первое, узнайте о более автоматизированных методах, основанных на дедукции, если это второе, узнайте больше о Coq, HOL и т. Д. Кстати, если вы хотите изучить Coq, хотя приведенные выше ссылки хороши, я думаю, что Есть две действительно основные ссылки для изучения Coq:

Книга Бенджамина Пирса по основам программного обеспечения (доктор Пирс - отличный писатель, и я бы посоветовал вам также взглянуть на его более популярную "кирпичную книгу", если вы еще этого не сделали).

Сертифицированное программирование с зависимыми типами (Адам Члипала также неплохо пишет, хотя его книги предполагают немного большую зрелость и интеллект, чем, возможно, более простое введение Пирса).

Кристофер Мичински
источник
15

Существует множество систем для интерактивного доказательства теорем (ITP) - см. Также конференцию с таким названием - Coq, Изабель, HOL, ACL2, PVS и т. Д.

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

Там также может быть "функция убийцы", которая вам действительно нужна для вашей работы.

Это также помогает иметь коллег-экспертов по одной из этих систем.

  • Каковы различия между Кок и Изабель?

Оба являются потомками системы LCF из Стэнфорда / Эдинбурга / Кембриджа. В 1985 году Дж. Уэт и Л. Полсон вместе работали над последней версией Кембриджского LCF. Затем произошел раскол в направлении Coc / CIC / COQ (сейчас Coq) во Франции и Изабель в Кембридже и Мюнхене. Обратите внимание, что HOL4, HOL-Light, HOL-XYZ являются другими родственными потомками LCF.

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

  • Должен ли я учить Изабель или Coq, или оба?

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

  • Есть ли преимущество в том, чтобы сначала изучать Изабель или Кока?

Я так не думаю. Может быть опасность, что вы застрянете с тем, который пытаетесь первым, и не будете пытаться вторым, или если вы слишком рано разочаруетесь с первым и уволите его слишком рано. В любом случае вам потребуется время и настойчивость, чтобы стать продуктивным с любой из систем.

Со времени Proof General в качестве «IDE» уже упоминалось: Proof General / Emacs был стандартным унифицирующим интерфейсом для Coq и Isabelle на протяжении многих лет, но я бы никогда не назвал его IDE. Существует также CoqIDE с "IDE" в названии, но это относительно простой редактор поверх виджетов Gtk. Текущая версия Isabelle включает Isabelle / jEdit, в названии которой нет слова "IDE", но она предназначена для того, чтобы приближать то, что вы обычно видите в Netbeans или IntelliJ IDEA - для проверочных текстов вместо кода Java.

Макарий
источник
10

Вот несколько хороших видеоуроков Coq от Andrej Bauer. Это никоим образом не завершено, но я думаю, что это хорошее введение.

Daniil
источник
1
Большой! Обратите внимание на центральное предложение в «Первом доказательстве с Coq»: «Подумайте, как бы вы сделали это на бумаге». Лучший совет.
Рафаэль
4

Это введение в Изабель довольно исчерпывающее.

Также см. Это введение в Изабель

В общем, с Изабель сравнительно легко начать, так как есть много доступных примеров. Например, на официальном сайте

PS - Я никоим образом не связан с Изабель, я теоретик в формальных методах, но я знаю, что Изабель часто выступает в качестве отправной точки по умолчанию.

Shaull
источник
1
«Я знаю, что Изабель часто выступает в качестве начальной точки по умолчанию». Я бы сказал, что HOL часто выступает в качестве начальной точки по умолчанию, а в качестве помощника по проверке это скорее Coq, который часто используется по умолчанию. Думая об этом, это забавно ... самая известная логика (HOL, более известная, чем CoC) и самый известный помощник по проверке (Coq, более известный, чем Изабель), не совпадают (Coq основан на CoC и Изабель на HOL).
Hibou57
2

λ

Кроме того, в Фондовом программном обеспечении Летней школы DeepSpec есть несколько классных лекций:

Некоторые из лекций, основанных на серии программных основ, уже упоминались.

Aristu
источник