Программирование: математическая логика
-
Скопировать в буфер библиографическое описание
Программирование: математическая логика : учебное пособие для вузов / М. В. Швецкий, М. В. Демидов, А. В. Голанова, И. А. Кудрявцева. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2020. — 675 с. — (Высшее образование). — ISBN 978-5-534-11009-8. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/439066 (дата обращения: 16.08.2024).
- Добавить в избранное
2-е изд., пер. и доп. Учебное пособие для вузов
- Поделиться
Страниц
675
Обложка
Мягкая
Гриф
Гриф УМО ВО
ISBN
978-5-534-11009-8
Библиографическое описание
Программирование: математическая логика : учебное пособие для вузов / М. В. Швецкий, М. В. Демидов, А. В. Голанова, И. А. Кудрявцева. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2020. — 675 с. — (Высшее образование). — ISBN 978-5-534-11009-8. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/439066 (дата обращения: 16.08.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-е изд., пер. и доп. Учебное пособие для вузов