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