Электронный вариант 3-го издания этой книги (PDF)
Предисловие
Начальные соглашения об обозначениях
Глава 1. Исчисления высказываний
1.1. Пропозициональные формулы и булевы функции
1.1.1. Формальные языки
1.1.2. Язык логики высказываний
1.1.3. Семантика языка логики высказываний. Логические законы
1.1.4. Выражение булевой функции формулой. Дизъюнктивная и конъюнктивная нормальные формы. Полиномы Жегалкина
1.2. Общее понятие исчисления
1.2.1. Исчисление и вывод в исчислении
1.2.2. Вывод из гипотез
1.3. Исчисление высказываний гильбертовского типа
1.3.1. Формулировка исчисления
1.3.2. Корректность исчисления
1.3.3. Теорема о дедукции. Допустимые правила
1.3.4. Полнота исчисления
1.3.5. Поиск вывода и алгоритм Британского музея
1.4. Секвенциальное исчисление высказываний
1.4.1. Поиск контрпримера для пропозициональной формулы
1.4.2. Формулировка исчисления
1.4.3. Корректность и полнота исчисления
1.4.4. Допустимые правила
1.5. Метод резолюций для логики высказываний
Глава 2. Исчисления предикатов
2.1. Язык первого порядка
2.1.1. Формулы языка первого порядка
2.1.2. Вхождения предметных переменных в формулы
2.2. Семантика языка первого порядка
2.2.1. Интерпретация языка первого порядка
2.2.2. Примеры языков первого порядка и их интерпретаций
2.2.3. Формула, выражающая предикат
2.3. Свободные и правильные подстановки
2.3.1. Подстановка терма в формулу. Свободные подстановки
2.3.2. Конгруэнтные формулы. Правильные подстановки
2.4. Логические законы
2.5. Предварённая нормальная форма
2.6. Исчисление предикатов гильбертовского типа
2.6.1. Формулировка исчисления
2.6.2. Вывод из гипотез. Корректность исчисления. Теорема о дедукции. Допустимые правила
2.6.3. Полнота исчисления
2.6.4. Синтаксическая эквивалентность формул
2.7. Секвенциальное исчисление предикатов
2.7.1. Поиск контрпримера для формулы с кванторами
2.7.2. Формулировка исчисления
2.7.3. Корректность и полнота исчисления
2.7.4. Соотношение с исчислением предикатов гильбертовского типа
2.7.5. О поиске вывода в секвенциальном исчислении предикатов
Глава 3. Формальные аксиоматические теории
3.1. Основные определения
3.2. Теории с равенством
3.3. Элементарная арифметика
3.3.1. Формулировка теории
3.3.2. Нестандартная модель арифметики
3.3.3. Содержательные и формальные доказательства
3.4. Наивная теория множеств
3.4.1. Язык и аксиомы наивной теории множеств
3.4.2. Парадокс Рассела
3.5. Теория множеств Цермело-Френкеля ZF
3.5.1. Формулировка теории ZF
3.5.2. Отношения и функции в теории ZF
3.5.3. Числа в теории ZF
3.5.4. Аксиома выбора и теория ZFC
3.5.5. Теория ZFC как основание классической математики
Глава 4. Метод резолюций для логики предикатов
4.1. Скулемовская стандартная форма
4.2. Теорема Эрбрана
4.2.1. Эрбрановская интерпретация множества дизъюнктов
4.2.2. Семантические деревья
4.2.3. Теорема Эрбрана
4.2.4. Алгоритм проверки невыполнимости множества дизъюнктов
4.3. Унификация
4.3.1. Подстановки и унификаторы
4.3.2. Алгоритм унификации
4.4. Метод резолюций
4.4.1. Определение резолютивного вывода и корректность метода резолюций
4.4.2. Полнота метода резолюций
4.4.3. Алгоритм доказательства методом резолюций
4.5. Основы логического программирования
4.5.1. Логическая программа и её декларативная семантика
4.5.2. SLD-резолюция
4.5.3. Операционная семантика логической программы
Глава 5. Теория вычислимости
5.1. Определения понятия вычислимости
5.1.1. Машины Тьюринга
5.1.2. Нормальные алгоритмы
5.1.3. Лямбда-исчисление и лямбда-определимые функции
5.1.4. Частично рекурсивные функции
5.1.5. Тезис Чёрча
5.2. Разрешимые и перечислимые множества
5.2.1. Разрешимые и перечислимые множества натуральных чисел
5.2.2. Разрешимые и перечислимые числовые отношения
5.2.3. Теоремы о проекции
5.2.4. Разрешимые и перечислимые языки и словарные отношения
5.3. Нумерация вычислимых функций
5.3.1. Нумерация машин Тьюринга и вычислимых функций
5.3.2. Универсальные машины Тьюринга и универсальные функции
5.3.3. Теорема о параметризации
5.4. Неразрешимые проблемы. Сводимость
5.4.1. Понятие массовой проблемы
5.4.2. Проблемы самоприменимости, остановки и всюду определённости
5.4.3. Доказательство неразрешимости проблем методом сведения
5.4.4. m-сводимость и m-полнота
5.4.5. Теорема о рекурсии
5.5. Применения теории вычислимости
5.5.1. Проблема равенства для полугрупп
5.5.2. Проблема общезначимости и проблема выводимости для исчисления предикатов
5.5.3. Перечислимость теорем теории
5.5.4. Теоремы Гёделя о неполноте
Глава 6. Исчисление Хоара для доказательства корректности программ
6.1. Подходы к верификации программ
6.2. Программа и её операционная семантика
6.3. Аксиоматическая семантика программы
Приложение А. Свойства секвенциального исчисления предикатов и формальные аксиоматические теории на его основе
А.1. Некоторые свойства секвенциального исчисления предикатов
А.1.1. Допустимость правил добавления
А.1.2. Обратимость правил
А.1.3. Допустимость правил, формализующих некоторые обычные способы математических рассуждений
А.2. Формальные аксиоматические теории на основе секвенциального исчисления предикатов
А.2.1. Новые определения
А.2.2. Базовые теоремы
А.2.3. Примеры содержательного и формального доказательств в теории
Литература
Предметный указатель