Адрес e-mail:

Интерактивное доказывание теорем (Е.В. Дашков, осень 2018)

Лектор - доц. Е.В. Дашков

Спецкурс проходит по четвергам в 18:30 в ауд. 417 ГК. Начало - 13.09.2018.

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


Интерактивное доказывание теорем применяется как для проверки «слишком длинных» доказательств (например, в известной проблеме четырех красок), так и для верификации компьютерных программ. Последнее означает, что требуемые свойства программы выражаются в виде формального утверждения, которое доказывается с помощью интерактивной системы. (При этом важно иметь математизированное представление программы, что естественно делается в русле функционального программирования.) Таким образом программа доказуемо избавляется от ряда ошибок. Это особенно важно при разработке ключевых компонентов операционных систем, компиляторов и т. п.


В курсе предполагается научиться работать с популярной системой интерактивного доказывания теорем Coq, в частности, верифицировать теоремы формальной логики, элементарной арифметики, а также простые алгоритмы.


Курс имеет практическую ориентацию; теоретические сведения будут весьма ограничены. Знакомство слушателей с логикой высказываний и предикатов предполагается; знакомство с лямбда-исчислениями и функциональным.





Если вы заметили в тексте ошибку, выделите её и нажмите Ctrl+Enter.

МФТИ в социальных сетях

soc-vk soc-fb soc-tw soc-li soc-li soc-yt
Яндекс.Метрика