Введение

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

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

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

• Упражнение 3. Язык первого порядка: синтаксис (481мин.)
• • Теоретические сведения (291мин.)
  • Примеры решения некоторых типов упражнений (51мин.)
  • Упражнения для самостоятельного решения (127мин.)
• Упражнение 4. Гильбертовское исчисление первого порядка: построение доказательств и выводов с использованием основных правил вывода (304мин.)
• • Теоретические сведения (152мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (25мин.)
  • Упражнения для самостоятельного решения (114мин.)
• Упражнение 5. Гильбертовское исчисление первого порядка: установление существования доказательств и выводов с помощью допустимых правил вывода (241мин.)
• • Теоретические сведения (139мин.)
  • Примеры решения некоторых типов упражнений (25мин.)
  • Упражнения для самостоятельного решения (76мин.)
• Упражнение 6. Исчисление дедуктивных эквивалентностей. Предварённая и сколемовская нормальная форма (114мин.)
• • Теоретические сведения (63мин.)
  • Примеры решения некоторых типов упражнений (25мин.)
  • Упражнения для самостоятельного решения (25мин.)
• Упражнение 7. Моносукцедентное секвенциальное исчисление первого порядка (456мин.)
• • Теоретические сведения (317мин.)
  • Примеры решения некоторых типов упражнений (63мин.)
  • Упражнения для самостоятельного решения (63мин.)
• Упражнение 8. Многосукцедентное секвенциальное исчисление первого порядка (241мин.)
• • Теоретические сведения (190мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Упражнение 9. Генценовское исчисление натурального вывода (215мин.)
• • Теоретические сведения (89мин.)
  • Примеры решения некоторых типов упражнений (76мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 10. Метод аналитических таблиц для формул языка первого порядка (152мин.)
• • Теоретические сведения (76мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Упражнения для самостоятельного решения (25мин.)
• Упражнение 11. Понятие о математических теориях. Теория равенства (152мин.)
• • Теоретические сведения (114мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (25мин.)
• Упражнение 12. Язык термов сигнатуры σ (101мин.)
• • Теоретические сведения (63мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Тест:  ИСЧИСЛЕНИЯ МАТЕМАТИЧЕСКОЙ ЛОГИКИ (116мин.)

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

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

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

• Упражнение 15. Интуиционистские пропозициональные логики (342мин.)
• • Теоретические сведения (253мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Задачи для самостоятельного решения (63мин.)
• Упражнение 16. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop (241мин.)
• • Теоретические сведения (101мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Задачи для самостоятельного решения (89мин.)
• Упражнение 17. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения (317мин.)
• • Теоретические сведения (114мин.)
  • Примеры решения некоторых типов упражнений (101мин.)
  • Упражнения для самостоятельного решения (89мин.)
• Упражнение 18. Аналитические таблицы для интуиционистской логики (241мин.)
• • Теоретические сведения (127мин.)
  • Примеры решения некоторых типов упражнений (63мин.)
  • Задачи для самостоятельного решения (38мин.)
• Тест:  ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ (54мин.)

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

• Упражнение 19. Расширение языка первого порядка (139мин.)
• • Теоретические сведения (89мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 20. Формальный синтаксис модельных языков программирования: грамматические модели (329мин.)
• • Теоретические сведения (241мин.)
  • Упражнения для самостоятельного решения (76мин.)
• Упражнение 21. Содержательная операционная семантика модельных языков (203мин.)
• • Теоретические сведения (152мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 22. Аксиоматическая система Хоара для модельных языков Н и D (431мин.)
• • Теоретические сведения (279мин.)
  • Примеры решения некоторых типов упражнений (38мин.)
  • Упражнения для самостоятельного решения (101мин.)
• Упражнение 23. Аксиоматическая система Дейкстры. Wр-преобразователь предикатов (190мин.)
• • Теоретические сведения (127мин.)
  • Контрольные вопросы (13мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 24. Wp-семантика команды присваивания и композиции команд (203мин.)
• • Теоретические сведения (101мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (25мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 25. Wp-семантика команды выбора Дейкстры (165мин.)
• • Теоретические сведения (89мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (13мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 26. Wp-семантика команды цикла Дейкстры (355мин.)
• • Теоретические сведения (165мин.)
  • Контрольные вопросы (13мин.)
  • Примеры решения некоторых типов упражнений (63мин.)
  • Упражнения для самостоятельного решения (114мин.)
• Упражнение 27. Эвристические методы синтеза инвариантов цикла Дейкстры (177мин.)
• • Теоретические сведения (101мин.)
  • Примеры решения некоторых типов упражнений (25мин.)
  • Упражнения для самостоятельного решения (51мин.)
• Упражнение 28. Синтетический подход к формальной верификации программ (215мин.)
• • Теоретические сведения (101мин.)
  • Примеры решения некоторых типов упражнений (76мин.)
  • Упражнения для самостоятельного решения (38мин.)
• Тест:  АКСИОМАТИЧЕСКАЯ СЕМАНТИКА ЯЗЫКОВ ИМПЕРАТИВНОГО ПРОГРАММИРОВАНИЯ (116мин.)

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

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

Литература

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

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

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