Курс математической логики и теории вычислимости, Герасимов А.С., 2011

Курс математической логики и теории вычислимости, Герасимов А.С., 2011.
     
   Настоящее учебное пособие предназначено для изучения математической логики и теории алгоритмов. В нём описаны языки логики высказываний и логики предикатов первого порядка, семантика этих языков. На основе общего понятия исчисления изложены исчисления гильбертовского типа, секвенциальные исчисления и метод резолюций как способы формального математического доказательства. Рассмотрены основные формальные аксиоматические теории — элементарная арифметика и теория множеств Цермело-Френкеля. Теория алгоритмов представлена теорией вычислимости, в рамках которой дано несколько точных определений понятия алгоритма и доказана неразрешимость некоторых проблем. Дополнительная глава посвящена исчислению для формального доказательства правильности программ некоторого императивного языка программирования. В данной книге имеется более 190 упражнений.
Это учебное пособие адресовано в первую очередь студентам, специализирующимся по информатике, но будет полезно студентам разных математических специальностей (направлений подготовки), а также всем желающим начать систематическое изучение математической логики.




Вывод из гипотез.
Для дальнейшего изложения нам понадобится понятие вывода из гипотез. Сейчас мы проиллюстрируем это понятие на доступном примере. Пусть мы желаем с помощью вывода в исчислении Pal получать не только палиндромы, но и слова, в каждом из которых в середине стоит слово ab, а в остальном такие слова строятся как палиндромы. Примерами таких слов являются слова ab, babb. aaba, baobab. Тогда, чтобы воспользоваться исчислением Pal. можно предположить, что слово ab является дополнительной аксиомой этого исчисления, иначе говоря, считать ab гипотезой. Уточним этот пример, дав следующие определения.

Пусть С — исчисление в языке L, Г — произвольное множество слов языка L. Выводом из Г в исчислении С называется конечная последовательность слов, каждое из которых является аксиомой, принадлежит Г или получается из предшествующих слов этой последовательности по некоторому правилу вывода исчисления С. Число членов этой последовательности называется длиной этого вывода из Г. Элементы множества Г называются гипотезами вывода из Г.

ОГЛАВЛЕНИЕ.
Предисловие.
Начальные соглашения об обозначениях.
Глава 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. Примеры содержательного и формального доказательств в теории.
Литература.
Предметный указатель.



Бесплатно скачать электронную книгу в удобном формате, смотреть и читать:
Скачать книгу Курс математической логики и теории вычислимости, Герасимов А.С., 2011 - fileskachat.com, быстрое и бесплатное скачивание.

Скачать pdf
Ниже можно купить эту книгу, если она есть в продаже, и похожие книги по лучшей цене со скидкой с доставкой по всей России.Купить книги


Скачать - pdf - Яндекс.Диск.






Теги: учебник по математике :: математика :: Герасимов :: теорема Эрбрана