Описание:Цель учебного курса – ознакомить студентов, специализирующихся в области программирования, с теми разделами математической логики и теории алгоритмов, которые наиболее широко используются в теории и практике современного программирования. К числу этих разделов относятся
классическая логика предикатов первого порядка, рассматриваемая как формальный язык представления знаний,
аппарат логического вывода, рассматриваемый как метод дедуктивного извлечения знаний,
метод резолюций – наиболее распространенный и эффективный подход к автоматическому доказательству теорем,
концепция алгоритма и универсальных моделей вычислений,
теория рекурсивных функций и методы доказательства алгоритмической неразрешимости математических проблем
сложность вычислений и комбинаторные методы оценки сложности математитческих задач.
Основное внимание уделяется
1) алгоритмическим аспектам математической логики и тем задачам информатики, в решении которых математическая логика применяется наиболее успешно и
2) . элементам теории рекурсивных функций и теории сложности вычислений, составляющим теоретические основы современного программирования.
Учебный курс состоит из четырех частей. В первой части курса вводится синтаксис и семантика логики предикатов первого порядка, определяется отношение выполнимости формул. Вводятся понятия модели, выполнимых и общезначимых формул, рассматривается теорема о логическом следствии и объясняется ее прикладное значение. Для решения проблемы общезначимости в классической логике предикатов первого порядка вводятся понятие семантической таблицы рассматривается система правил табличного вывода. Доказываются теоремы корректности и полноты введенной системы правил табличного вывода, а также ряд следствий из этих теорем (теорема Левенгейма-Сколема, теорема Мальцева и др.).
Вторая часть курса посвящена методу резолюций в классической логике предикатов первого порядка. Вводятся понятия равносильных формул, предваренной нормальной формы, сколемовской стандартной формы. Доказываются теоремы о приведении замкнутых формул логики предикатов к указанным формам. Вводится понятие эрбрановской интерпретации и доказывается теорема Эрбрана. Вводится понятие унификации логических выражений, рассматривается алгоритм вычисления наиболее общего унификатора. Вводится правило резолюции, на основе которого определяется резолютивный вывод. Доказываются теоремы корректности и полноты резолютивного вывода. Рассматриваются стратегии построения резолютивного вывода. Объясняются прикладные возможности резолютивного вывода для построения автоматических систем доказательства теорем и дедуктивного извлечения знаний.
В третьей части курса дается обзор основных направлений развития математической логики. Рассматривается устройство систем логического вывода, применение математической логики для построения аксиоматических теорий в математике. Основное внимание уделяется формальной арифметике: рассматривается теорема Геделя о неполноте формальной арифметики и ее общематематическое значение. Приводится описание интуиционистской логики, обсуждаются ее особенности и возможные приложения в программировании. Рассматриваются различные семейства модальных логик (эпистемические, темпоральные, динамические) и обсуждаются их приложения в информатике. В заключение курса рассказывается о математических принципах применения неклассических логик (логики Хоара и темпоральной логики линейного времени) для верификации последовательных и параллельных программ.
В четвертой части курса рассказывается о моделях вычислений, используемых для формализации понятий «эффективно вычислимой функции» и «алгоритма». Рассматриваются машины Тьюринга, машины Поста, нормальные алгорифмы Маркова, выражения лямбда исчисления. Вводится понятие вычислимой по Тьюрингу арифметической функции. На примерах некоторых арифметических функций показано, что перечисленные модели вычислений имеют одинаковые вычислительные возможности. Приводятся также примеры арифметических функций, которые невозможно реализовать ни в одной из указанных моделей вычислений. На множестве арифметических функций вводятся операции вводятся операции суперпозиции, минимизации и примитивной рекурсии, определяются классы примитивно рекурсивных и частично рекурсивных функций. Доказана теорема о совпадении классов арифметических функций, вычислимых по Тьюрингу, и класса частично арифметических функций. Введено понятие универсальной машины Тьюринга. Большое внимание уделяется применению метода сводимости для доказательства нерекурсивности некоторых функций и отношений, связанных с решением задач анализа поведения программ.
В заключение курса дается краткое введение в теорию сложности вычислений. Рассматриваются различные меры сложности вычислений, классы сложности, примеры задач комбинаторики, теории графов, теории автоматов из различных классов сложности.