Введение

Часть 1. ОБЩАЯ ТЕОРИЯ ИСЧИСЛЕНИЙ

• Упражнение 1. Слова в алфавите (486мин.)
• • Теоретические сведения (396мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Упражнение 2. Индуктивное определение множества слов в алфавите. Исчисления на словах в алфавите. Формальные доказательства в исчислениях на словах в алфавите (307мин.)
• • Теоретические сведения (204мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (64мин.)
• Тест:  ОБЩАЯ ТЕОРИЯ ИСЧИСЛЕНИЙ (86мин.)

Часть 2. ИСЧИСЛЕНИЯ МАТЕМАТИЧЕСКОЙ ЛОГИКИ

• Упражнение 3. Язык первого порядка: синтаксис (486мин.)
• • Теоретические сведения (294мин.)
  • Примеры решения некоторых типов упражнений (51мин.)
  • Упражнения для самостоятельного решения (128мин.)
• Упражнение 4. Гильбертовское исчисление первого порядка: построение доказательств и выводов с использованием основных правил вывода (307мин.)
• • Теоретические сведения (153мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (115мин.)
• Упражнение 5. Гильбертовское исчисление первого порядка: установление существования доказательств и выводов с помощью допустимых правил вывода (243мин.)
• • Теоретические сведения (141мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (77мин.)
• Упражнение 6. Исчисление дедуктивных эквивалентностей. Предварённая и сколемовская нормальная форма (115мин.)
• • Теоретические сведения (64мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (26мин.)
• Упражнение 7. Моносукцедентное секвенциальное исчисление первого порядка (460мин.)
• • Теоретические сведения (320мин.)
  • Примеры решения некоторых типов упражнений (64мин.)
  • Упражнения для самостоятельного решения (64мин.)
• Упражнение 8. Многосукцедентное секвенциальное исчисление первого порядка (243мин.)
• • Теоретические сведения (192мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Упражнение 9. Генценовское исчисление натурального вывода (217мин.)
• • Теоретические сведения (89мин.)
  • Примеры решения некоторых типов упражнений (77мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 10. Метод аналитических таблиц для формул языка первого порядка (153мин.)
• • Теоретические сведения (77мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Упражнения для самостоятельного решения (26мин.)
• Упражнение 11. Понятие о математических теориях. Теория равенства (153мин.)
• • Теоретические сведения (115мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (26мин.)
• Упражнение 12. Язык термов сигнатуры σ (102мин.)
• • Теоретические сведения (64мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Тест:  ИСЧИСЛЕНИЯ МАТЕМАТИЧЕСКОЙ ЛОГИКИ (116мин.)

Часть 3. АВТОМАТИЗАЦИЯ ПОИСКА ЛОГИЧЕСКОГО ВЫВОДА

• Лабораторная работа 13. Поиск логических выводов в режиме диалога "Человек-Компьютер": система Deductio, гильбертовское исчисление (217мин.)
• • Теоретические сведения (64мин.)
  • Примеры решения некоторых типов упражнений (102мин.)
  • Задачи для самостоятельного решения (38мин.)
• Лабораторная работа 14. Поиск логических выводов в режиме диалога "Человек-Компьютер": система Deductio, генценовское исчисление натурального вывода (294мин.)
• • Теоретические сведения (26мин.)
  • Примеры решения некоторых типов упражнений (217мин.)
  • Задачи для самостоятельного решения (51мин.)
• Тест:  АВТОМАТИЗАЦИЯ ПОИСКА ЛОГИЧЕСКОГО ВЫВОДА (24мин.)

Часть 4. ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ

• Упражнение 15. Интуиционистские пропозициональные логики (345мин.)
• • Теоретические сведения (256мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Задачи для самостоятельного решения (64мин.)
• Упражнение 16. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (243мин.)
• • Теоретические сведения (102мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Задачи для самостоятельного решения (89мин.)
• Упражнение 17. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (320мин.)
• • Теоретические сведения (115мин.)
  • Примеры решения некоторых типов упражнений (102мин.)
  • Упражнения для самостоятельного решения (89мин.)
• Упражнение 18. Аналитические таблицы для интуиционистской логики (243мин.)
• • Теоретические сведения (128мин.)
  • Примеры решения некоторых типов упражнений (64мин.)
  • Задачи для самостоятельного решения (38мин.)
• Тест:  ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ (54мин.)

Часть 5. АКСИОМАТИЧЕСКАЯ СЕМАНТИКА ЯЗЫКОВ ИМПЕРАТИВНОГО ПРОГРАММИРОВАНИЯ

• Упражнение 19. Расширение языка первого порядка (141мин.)
• • Теоретические сведения (89мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 20. Формальный синтаксис модельных языков программирования: грамматические модели (332мин.)
• • Теоретические сведения (243мин.)
  • Упражнения для самостоятельного решения (77мин.)
• Упражнение 21. Содержательная операционная семантика модельных языков (204мин.)
• • Теоретические сведения (153мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 22. Аксиоматическая система Хоара для модельных языков Н и D (435мин.)
• • Теоретические сведения (281мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Упражнения для самостоятельного решения (102мин.)
• Упражнение 23. Аксиоматическая система Дейкстры. Wр-преобразователь предикатов (192мин.)
• • Теоретические сведения (128мин.)
  • Контрольные вопросы (13мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 24. Wp-семантика команды присваивания и композиции команд (204мин.)
• • Теоретические сведения (102мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 25. Wp-семантика команды выбора Дейкстры (166мин.)
• • Теоретические сведения (89мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 26. Wp-семантика команды цикла Дейкстры (358мин.)
• • Теоретические сведения (166мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (64мин.)
  • Упражнения для самостоятельного решения (115мин.)
• Упражнение 27. Эвристические методы синтеза инвариантов цикла Дейкстры (179мин.)
• • Теоретические сведения (102мин.)
  • Примеры решения некоторых типов упражнений (26мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 28. Синтетический подход к формальной верификации программ (217мин.)
• • Теоретические сведения (102мин.)
  • Примеры решения некоторых типов упражнений (77мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Тест:  АКСИОМАТИЧЕСКАЯ СЕМАНТИКА ЯЗЫКОВ ИМПЕРАТИВНОГО ПРОГРАММИРОВАНИЯ (116мин.)

Часть 6. ЭЛЕМЕНТЫ МОДАЛЬНОЙ ЛОГИКИ

• Упражнение 29. Модальные логики: аналитические таблицы для модальной логики, нормальные модальные исчисления K, T, В, S4, S5 (524мин.)
• • Теоретические сведения (332мин.)
  • Примеры решения некоторых типов упражнений (77мин.)
  • Задачи для самостоятельного решения (102мин.)
• Упражнение 30. Конструирование свойств шкал Крипке (141мин.)
• • Теоретические сведения (38мин.)
  • Примеры решения некоторых типов упражнений (51мин.)
  • Задачи для самостоятельного решения (51мин.)
• Тест:  ЭЛЕМЕНТЫ МОДАЛЬНОЙ ЛОГИКИ (34мин.)

Литература

Новые издания по дисциплине "Программирование" и смежным дисциплинам

Завершение курса

• Тест:  Итоговое тестирование (70мин.)