|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Математическая логика и логическое программированиеучебный курс
- Авторы: Захарьящев М.В., Захаров В.А.
- Год создания: 1998
- Организация: МГУ имени М.В. Ломоносова
- Описание: Цель учебного курса – ознакомить студентов, специализирующихся в области программирования, с теми разделами математической логики, которые наиболее широко используются в теории и практике современного программирования. К числу этих разделов относятся классическая логика предикатов первого порядка, рассматриваемая как формальный язык представления знаний, аппарат логического вывода, рассматриваемый как метод дедуктивного извлечения знаний, метод резолюций – наиболее распространенный и эффективный подход к автоматическому доказательству теорем, логическое программирование – одна из трех основных парадигм современного программирования, неклассические (модальные, темпоральные, динамические и др.) логики, предоставляющие удобный и действенный аппарат спецификации и анализа поведения программ. Основное внимание уделяется алгоритмическим аспектам математической логики и тем задачам информатики, в решении которых математическая логика применяется наиболее успешно. Учебный курс состоит из четырех частей. В первой части курса вводится синтаксис и семантика логики предикатов первого порядка, определяется отношение выполнимости формул. Вводятся понятия модели, выполнимых и общезначимых формул, рассматривается теорема о логическом следствии и объясняется ее прикладное значение. Для решения проблемы общезначимости в классической логике предикатов первого порядка вводятся понятие семантической таблицы рассматривается система правил табличного вывода. Доказываются теоремы корректности и полноты введенной системы правил табличного вывода, а также ряд следствий из этих теорем (теорема Левенгейма-Сколема, теорема Мальцева и др.). Вторая часть курса посвящена методу резолюций в классической логике предикатов первого порядка. Вводятся понятия равносильных формул, предваренной нормальной формы, сколемовской стандартной формы. Доказываются теоремы о приведении замкнутых формул логики предикатов к указанным формам. Вводится понятие эрбрановской интерпретации и доказывается теорема Эрбрана. Вводится понятие унификации логических выражений, рассматривается алгоритм вычисления наиболее общего унификатора. Вводится правило резолюции, на основе которого определяется резолютивный вывод. Доказываются теоремы корректности и полноты резолютивного вывода. Рассматриваются стратегии построения резолютивного вывода. Объясняются прикладные возможности резолютивного вывода для построения автоматических систем доказательства теорем и дедуктивного извлечения знаний. В третьей части курса рассказывается о математических основах логического программирования. Вводится синтаксис хорновских логических программ и определяются две семантики логических программ – декларативная и операционная. Доказываются теоремы корректности и полноты операционной семантики относительно декларативной. Рассматриваются стратегии вычислений логических программ и доказывается теорема о вычислительной универсальности хорновских логических программ. На основании этого доказывается теорема Черча об алгоритмической неразрешимости проблемы общезначимости в классической логике предикатов. Рассматриваются дополнительные средства логического программирования (операторы отсечения и отрицания, встроенные предикаты), прагматика логического программирования. В четвертой части курса дается обзор основных направлений развития математической логики. Рассматривается устройство систем логического вывода, применение математической логики для построения аксиоматических теорий в математике. Основное внимание уделяется формальной арифметике: рассматривается теорема Геделя о неполноте формальной арифметики и ее общематематическое значение. Приводится описание интуиционистской логики, обсуждаются ее особенности и возможные приложения в программировании. Рассматриваются различные семейства модальных логик (эпистемические, темпоральные, динамические) и обсуждаются их приложения в информатике. В заключение курса рассказывается о математических принципах применения неклассических логик (логики Хоара и темпоральной логики линейного времени) для верификации последовательных и параллельных программ.
- Добавил в систему: Захаров Владимир Анатольевич
Преподавание курса
- с 1 сентября 2022 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, вариативной части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2022 - 31 августа 2023 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, вариативной части, семинары, 18 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2021 - 20 декабря 2021 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2021 - 20 декабря 2021 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, семинары, 48 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2020 - 20 декабря 2020 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2020 - 20 декабря 2020 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, семинары, 48 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2019 - 20 декабря 2019 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, семинары, 48 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2019 - 20 декабря 2019 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2018 - 20 декабря 2018 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2017 - 20 декабря 2017 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2016 - 31 августа 2022 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, вариативной части, семинары, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2016 - 20 декабря 2016 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2016 - 20 декабря 2016 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, семинары, 48 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2015 - 30 июня 2016 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, вариативной части, семинары, 72 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2015 - 20 декабря 2015 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2015 - 20 декабря 2015 Захаров Владимир Анатольевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, базовой части, семинары, 80 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- с 7 февраля 2015 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, вариативной части, лекции, 54 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- с 7 февраля 2015 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра математической кибернетики
- обязательная, вариативной части, семинары, 18 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2012 - 20 декабря 2014 Подымов Владислав Васильевич
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, вариативной части, семинары, 36 часов
- Авторы: Захарьящев М.В., Захаров В.А.
- 1 сентября 2001 - 31 декабря 2013 Селезнева Светлана Николаевна
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики
- обязательная, базовой части, семинары, 36 часов
- Авторы: Захарьящев М.В., Захаров В.А.