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

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

Математическая логика
Бесплатно
13 недель13 недель
Сертификат гос. образцаСертификат гос. образца
Платный сертификатПлатный сертификат
РусскийРусский
ФГАОУ ВО «Санкт-Петербургский политехнический университет Петра Великого»
Открытое Образование

Описание:

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

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

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

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

Модуль 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