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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Кок в спешке Ив Берто, или
• первая часть « Доказательства ассистента для логики высшего порядка » Тобиаса Нипкова, Лоуренса К. Полсона и Маркуса Вензеля.

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

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

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

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

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

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

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

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

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

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

Существует множество систем для интерактивного доказательства теорем (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.

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

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

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

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

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

$\lambda$

• Габриэль Кларамунт - Введение в Coq - Часть 1 из 2 - λC 2017
• Габриэль Кларамунт - Введение в Coq - Часть 2 из 2 - λC 2017

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

• Летняя школа DeepSpec, 13-28 июля 2017 г.
• Летняя школа DeepSpec, 16-27 июля 2018 года

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

• Coq Intensive

• Проверенные функциональные алгоритмы