наверх

Математическая логика

 width=
5 дней
До конца записи

Целью освоения учебной дисциплины "Математическая логика" является формирование представлений о классической логике и применение ее в информатике.

О курсе

Технологии в информатике меняются очень быстро. Инженер-программист должен осваивать новые информационные технологии каждые 2-5 лет. Однако при этом концептуальные, базисные теоретические основы информационных технологий остаются неизменными.

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

Курс состоит из трех частей. Первая часть посвящена базе математической логики – теории двоичных функций. Вторая часть излагает базовые разделы математической логики, наиболее часто применяемые в практике информационных технологий: методы формализации умозаключений, алгоритмы формального логического вывода, аксиоматические теории. Заключительная часть посвящена методам верификации распределенных алгоритмов и систем.

Формат

Курс включает в себя лекции и контрольные работы.

Все материалы, необходимые для изучения курса, доступны студентам в электронном виде. Они основываются на книгах Ю.Г. Карпова: "Теория автоматов" и "Model checking. Верификация параллельных и распределенных программных систем". Но мы приветствуем любознательных студентов, жадно изучающих книги по математической логике.

Требования

Достаточно знания математики в объеме средней школы. В первом разделе излагается материал из курса "Дискретная математика", в объеме необходимом для уверенного использования его в "Математической логике". Студенты, знакомые с дискретной математикой, могут пропустить этот раздел, сдав контрольные работы.

Программа курса

Модуль 1. Введение в теорию двоичных функций

  • Тема 1. Булевы функции
  • Тема 2. Нормальные формы представления булевых функций
  • Тема 3. Теорема Поста
  • Тема 4. Применение булевых функций
  • Тема 5. Бинарные решающие диаграммы
  • Тема 6. Конечные автоматы и их применение

Модуль 2. Логика высказываний

  • Тема 7. Основные понятия логики высказываний
  • Тема 8. Логический вывод в логике высказываний

Модуль 3. Логика предикатов

  • Тема 9. Основные понятия логики предикатов
  • Тема 10. Логический вывод в логике предикатов

Модуль 4. Аксиоматические теории. Исчисление высказываний

  • Тема 11. Основные компоненты аксиоматических теорий
  • Тема 12. Теорема Геделя о полноте

Модуль 5. Дедуктивная верификация программ

  • Тема 13. Программа как преобразователь предикатов
  • Тема 14. Индуктивный метод Флойда

Модуль 6. Проверка корректности реагирующих программ

  • Тема 15. Темпоральные логики LTL, CTL
  • Тема 16. Алгоритм проверки выполнимости для CTL

Результаты обучения

В результате изучения дисциплины студент должен:

  • знать понятия, определения, термины, методы, алгоритмы, способы решения задач логики высказываний; логики предикатов и соответствующих исчислений.
  • уметь оценить сложность алгоритмов, выделить легко и трудноразрешимые задачи, оценить классы задач P и NP.
  • овладеть базовыми методами и алгоритмами проверки логического следования, проверки корректности программ, способами определения сложности вычислений и организации эффективных алгоритмов.

Формируемые компетенции

ОПК-1 способность использовать базовые знания естественных наук, математики и информатики, основные факты, концепции, принципы теорий, связанных с фундаментальной информатикой и информационными технологиями

ПК-2 способность понимать, совершенствовать и применять современный математический аппарат, фундаментальные концепции и системные методологии, международные и профессиональные стандарты в области информационных технологий

ПК-6 способность эффективно применять базовые математические знания и информационные технологии при решении проектно-технических и прикладных задач, связанных с развитием и использованием информационных технологий

  • 13 недель

    длительность курса

  • 3 зачётных единицы

    для зачета в своем вузе

Карпов Юрий Глебович

Доктор технических наук, Профессор
Должность: Профессор СПбПУ

Шошмина Ирина Владимировна

Кандидат технических наук
Должность: Старший преподаватель

Сертификат

Для получения сертификата общая оценка должна быть выше 68%.

Похожие курсы