Программирование: математическая логика
-
Скопировать в буфер библиографическое описание
Программирование: математическая логика : учебное пособие для среднего профессионального образования / М. В. Швецкий, М. В. Демидов, А. В. Голанова, И. А. Кудрявцева. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2024. — 675 с. — (Профессиональное образование). — ISBN 978-5-534-13248-9. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/542173 (дата обращения: 11.12.2024).
- Добавить в избранное
2-е изд., пер. и доп. Учебное пособие для СПО
- Поделиться
- Курс с экзаменом
-
Швецкий М. В., Демидов М. В., Голанова А. В., Кудрявцева И. А.
2024
Страниц
675
Обложка
Мягкая
Гриф
Гриф УМО СПО
ISBN
978-5-534-13248-9
Библиографическое описание
Программирование: математическая логика : учебное пособие для среднего профессионального образования / М. В. Швецкий, М. В. Демидов, А. В. Голанова, И. А. Кудрявцева. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2024. — 675 с. — (Профессиональное образование). — ISBN 978-5-534-13248-9. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/542173 (дата обращения: 11.12.2024).
Тематика/подтематика
Учебное пособие представляет собой систему упражнений и лабораторных работ по курсу «Математическая логика и теория алгоритмов», содержащих теоретические сведения по общей теории исчислений, исчислениям математической логики, элементам интуиционистской логики, аксиоматической семантике языков императивного программирования. В пособие включено значительное количество задач и упражнений для самостоятельного решения.
- Введение
-
Часть 1. ОБЩАЯ ТЕОРИЯ ИСЧИСЛЕНИЙ
-
Упражнение 1. Слова в алфавите
-
Теоретические сведения
- Предварительные наблюдения
- Исходные понятия и представления
- Синтаксическая переменная
- Предметный язык и метаязык
- Алфавит. Буква
- Слово в алфавите
- Соглашения об обозначениях
- Основные операции над словами в алфавите
- Предикат "равенство слов в алфавите"
- Алгебраическая операция приписывания слов
- Подслова и их вхождения в слово
- Операция замены подслов
- Операция подстановки слова вместо буквы
- Варианты операции подстановки
- Числовые функции, определённые на множестве слов
- Функции, частично определённые на множестве слов
- Комментарий для любителей алгебры. Полугруппа. Моноид слов
- Метод математической индукции как распознающая процедура
- Контрольные вопросы
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
-
Упражнение 2. Индуктивное определение множества слов в алфавите. Исчисления на словах в алфавите. Формальные доказательства в исчислениях на словах в алфавите
-
Теоретические сведения
- Индуктивное определение множества слов в алфавите
- Пример индуктивного определения множества слов
- Индукция по построению множества объектов
- Исчисление математических объектов
- Определение множества слов в алфавите с помощью исчисления на словах
- Доказательство в исчислении на словах
- Вывод из посылок в исчислении на словах
- Допустимые правила в исчислении на словах
- Определение функции индукцией по построению множества слов
- Из истории создания буквенного исчисления
- Контрольные вопросы
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
-
Упражнение 1. Слова в алфавите
-
Часть 2. ИСЧИСЛЕНИЯ МАТЕМАТИЧЕСКОЙ ЛОГИКИ
-
Упражнение 3. Язык первого порядка: синтаксис
-
Теоретические сведения
- Алфавит. Сигнатура
- Термы сигнатуры σ
- Индукция по построению множества термов
- Формулы сигнатуры σ
- Индукция по построению множества формул
- Язык формальных систем нулевого и первого порядка
- Запись формул в метаязыке
- Синтаксическая однозначность представления выражений
- Синтаксическая однозначность представления вхождений термов и формул
- Синтаксическое сохранение выражений при замене вхождений подвыражений
- Свободные и связанные вхождения переменных
- Свободные и связанные переменные
- Операция "подстановка терма вместо свободной переменной в выражение"
- Термы, допустимые для подстановки вместо переменных в формулу
- Операция "подстановка предметной переменной вместо свободной переменной в выражение"
- Операция "одновременная подстановка термов вместо свободных переменных в выражение"
- Операция "переименование связанных переменных в формуле"
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
-
Упражнение 4. Гильбертовское исчисление первого порядка: построение доказательств и выводов с использованием основных правил вывода
-
Теоретические сведения
- Аксиомные схемы и правила вывода гильбертовского исчисления первого порядка
- Линейное доказательство и линейный вывод из множества гипотез
- Древесное доказательство и древесный вывод из множества гипотез
- Индукция по построению доказательства
- Соглашения об обозначениях при построении доказательств и выводов
- Гёделева нумерация языка формальной системы первого порядка
- Контрольные вопросы
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 5. Гильбертовское исчисление первого порядка: установление существования доказательств и выводов с помощью допустимых правил вывода
- Упражнение 6. Исчисление дедуктивных эквивалентностей. Предварённая и сколемовская нормальная форма
-
Упражнение 7. Моносукцедентное секвенциальное исчисление первого порядка
-
Теоретические сведения
- Секвенции. Секвенциальные схемы
- Смысл понятия "секвенция"
- Аксиомная схема. Основные правила вывода
- Содержательный смысл основных правил вывода
- Доказуемые (выводимые) секвенции. Доказуемые формулы
- Допустимые правила вывода
- Доказательство допустимых правил вывода методом подъёма
- Теорема Генцена об устранении сечения
- Отношение дедуктивной эквивалентности. Дедуктивно эквивалентные формулы
- Связь секвенциального и гильбертовского исчислений
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 8. Многосукцедентное секвенциальное исчисление первого порядка
-
Упражнение 9. Генценовское исчисление натурального вывода
-
Теоретические сведения
- Фигуры заключения для интуиционистского исчисления натурального вывода
- Фигуры заключения для классического исчисления натурального вывода
- Фигуры прямого и косвенного заключения
- Правила заключения. Правила вывода
- Неформальное описание понятия "вывод"
- Неформальное описание процесса построения вывода
- Биографические сведения
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 10. Метод аналитических таблиц для формул языка первого порядка
- Упражнение 11. Понятие о математических теориях. Теория равенства
- Упражнение 12. Язык термов сигнатуры σ
-
Упражнение 3. Язык первого порядка: синтаксис
- Часть 3. АВТОМАТИЗАЦИЯ ПОИСКА ЛОГИЧЕСКОГО ВЫВОДА
-
Часть 4. ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ
- Упражнение 15. Интуиционистские пропозициональные логики
- Упражнение 16. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop
- Упражнение 17. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва - Дж. Худельмайера без правила сокращения
- Упражнение 18. Аналитические таблицы для интуиционистской логики
-
Часть 5. АКСИОМАТИЧЕСКАЯ СЕМАНТИКА ЯЗЫКОВ ИМПЕРАТИВНОГО ПРОГРАММИРОВАНИЯ
- Упражнение 19. Расширение языка первого порядка
- Упражнение 20. Формальный синтаксис модельных языков программирования: грамматические модели
- Упражнение 21. Содержательная операционная семантика модельных языков
-
Упражнение 22. Аксиоматическая система Хоара для модельных языков Н и D
-
Теоретические сведения
- Концепция доказательного программирования
- Из истории доказательного программирования
- Понятие "спецификация программы"
- Понятие "верификация программы"
- Подходы к формальной верификации
- Понятие "тройка Хоара"
- Дедуктивная семантика языка программирования
- Аксиоматическая система Хоара
- Понятие "инвариант цикла"
- Понятие "завершение программы"
- Понятие "частично правильная программа"
- Технология доказательства частичной правильности программы в системе Хоара
- Технология доказательства полной правильности программы в системе Хоара
- О неполноте системы Хоара
- Недетерминированные программы в системе Хоара
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
-
Упражнение 23. Аксиоматическая система Дейкстры. Wр-преобразователь предикатов
-
Теоретические сведения
- Wp-преобразователь предикатов
- Sp-преобразователь предикатов
- Дедуктивная семантика команды
- Доказуемая программа в системе Дейкстры
- Аксиоматическая система Дейкстры
- Структурные допустимые правила вывода
- Wp-семантика простейших команд
- Wp-семантика команды ввода
- Wp-семантика команды вывода
- Допустимые правила о подпрограммах
- Контрольные вопросы
- Упражнения для самостоятельного решения
-
Теоретические сведения
-
Упражнение 24. Wp-семантика команды присваивания и композиции команд
-
Теоретические сведения
- Аксиома и wp-семантика композиции команд
- Аксиома и wp-семантика команды присваивания
- Sp-семантика команды присваивания и композиции команд
- Аксиома обновления элемента массива
- Wp-семантика команды присваивания элементу массива
- Синтез команд присваивания
- Понятие "уравнение в отношениях выводимости" в языке Н
- Контрольные вопросы
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 25. Wp-семантика команды выбора Дейкстры
- Упражнение 26. Wp-семантика команды цикла Дейкстры
- Упражнение 27. Эвристические методы синтеза инвариантов цикла Дейкстры
- Упражнение 28. Синтетический подход к формальной верификации программ
-
Часть 6. ЭЛЕМЕНТЫ МОДАЛЬНОЙ ЛОГИКИ
-
Упражнение 29. Модальные логики: аналитические таблицы для модальной логики, нормальные модальные исчисления K, T, В, S4, S5
-
Теоретические сведения
- Математические сведения
- Модальности. Модальная логика
- Синтаксис пропозициональной модальной логики
- Модель Крипке для формул модальной пропозициональной логики
- Аналитические таблицы для пропозициональной модальной логики
- Нормальные модальные исчисления
- Характеризация отношений достижимости с помощью модальных формул
- Связи интуиционистской и модальной логики
- Корректность и полнота нормальных модальных исчислений
- Биографические сведения
- Примеры решения некоторых типов упражнений
- Задачи для самостоятельного решения
-
Теоретические сведения
- Упражнение 30. Конструирование свойств шкал Крипке
-
Упражнение 29. Модальные логики: аналитические таблицы для модальной логики, нормальные модальные исчисления K, T, В, S4, S5
- Литература
- Новые издания по дисциплине "Программирование" и смежным дисциплинам
Профессиональное образование
-
Программирование: комбинаторная логика
2-е изд., пер. и доп. Учебное пособие для СПО
-
Программирование: теория типов
2-е изд., пер. и доп. Учебное пособие для СПО