СПбГУ, СПб, 2010, составлены самим лектором Братчиковым И.Л.
Конспект-учебник имеет следующую структуру:
Введение
Основы математической логики
Силлогизмы Аристотеля
Исчисление высказываний
Формулы исчисления высказываний
Интерпретация формул исчисления высказываний
Семантические деревья и алгоритм Куайна
Теорема об общезначимости
Эквивалентные преобразования в исчислении высказываний
Упрощение релейно-контактных схем
Дизъюнктивные и конъюнктивные нормальные формы
Метод Куайна–Мак-Класки
Свойства кнф. Аналитический метод нормализации
Алгоритм Девиса-Патнема
Проблема дедукции
Метод резолюций
Единичная резолюция
Входная линейная резолюция Исчисление предикатов
Формулы исчисления предикатов
Интерпретация формул исчисления предикатов
Общезначимые схемы с кванторами в исчислении предикатов
Сколемовские и клаузальные формы
Эрбрановский универсум
Связь между произвольными и H-интерпретациями
Подстановка и конкретизация
Фундаментальная конкретизация
Доказательство невыполнимости с помощью фундаментальной конкретизации
Алгоритм унификации
Пример применения метода резолюций в исчислении предикатов Язык Пролог
Модели представления знаний в исчислении предикатов
Основы языка Пролог (стандарт)
Синтаксис языка
Типы вопросов
Рекурсия. Декларативная и процедурная семантики
Встроенные предикаты (Арифметика, Предикаты сравнения, Предикаты ввода-вывода, Предикат отсечения, Пример применения предиката отсечения, Тождественно ложный предикат)
Примеры
Списки
Основы Турбо-Пролога
Интерфейс пользователя
Структура программ на Турбо-Прологе (Раздел Domains – описание нестандартных типов констант, Раздел Database – описание динамической базы данных, Раздел Predicates – описание предикатов, Раздел Clauses – база знаний, Вопросы)
Примеры (Родственные отношения, Библиотечные каталоги, Целые числа в заданном интервале, Простые числа, Ханойские башни) Аксиоматические системы
Простая аксиоматическая система
Метатеоремы (теорема Эрбрана-Тарского, правило замены, принцип подстановки)
Аксиоматическая система натурального вывода
Аксиоматические системы для исчисления предикатов
Простая аксиоматическая система
Аксиоматическая система натурального вывода
Теории первого порядка Введение в теорию алгоритмов
Вычислимость и разрешимость
Машины Поста и Тьюринга
Машина Поста
Программа машины Поста
Машина Тьюринга
Определение машины Тьюринга как виртуального вычислительного устройства
Формальное определение машины Тьюринга
Классы формальных языков
Классы машин Тьюринга и их свойства
Автомат с линейно-ограниченной памятью (ЛО-автоматы)
Двухленточная машина Тьюринга
Автоматы с магазинной памятью (МП-автоматы)
Нормальные алгорифмы маркова
Заключение
Введение
Основы математической логики
Силлогизмы Аристотеля
Исчисление высказываний
Формулы исчисления высказываний
Интерпретация формул исчисления высказываний
Семантические деревья и алгоритм Куайна
Теорема об общезначимости
Эквивалентные преобразования в исчислении высказываний
Упрощение релейно-контактных схем
Дизъюнктивные и конъюнктивные нормальные формы
Метод Куайна–Мак-Класки
Свойства кнф. Аналитический метод нормализации
Алгоритм Девиса-Патнема
Проблема дедукции
Метод резолюций
Единичная резолюция
Входная линейная резолюция Исчисление предикатов
Формулы исчисления предикатов
Интерпретация формул исчисления предикатов
Общезначимые схемы с кванторами в исчислении предикатов
Сколемовские и клаузальные формы
Эрбрановский универсум
Связь между произвольными и H-интерпретациями
Подстановка и конкретизация
Фундаментальная конкретизация
Доказательство невыполнимости с помощью фундаментальной конкретизации
Алгоритм унификации
Пример применения метода резолюций в исчислении предикатов Язык Пролог
Модели представления знаний в исчислении предикатов
Основы языка Пролог (стандарт)
Синтаксис языка
Типы вопросов
Рекурсия. Декларативная и процедурная семантики
Встроенные предикаты (Арифметика, Предикаты сравнения, Предикаты ввода-вывода, Предикат отсечения, Пример применения предиката отсечения, Тождественно ложный предикат)
Примеры
Списки
Основы Турбо-Пролога
Интерфейс пользователя
Структура программ на Турбо-Прологе (Раздел Domains – описание нестандартных типов констант, Раздел Database – описание динамической базы данных, Раздел Predicates – описание предикатов, Раздел Clauses – база знаний, Вопросы)
Примеры (Родственные отношения, Библиотечные каталоги, Целые числа в заданном интервале, Простые числа, Ханойские башни) Аксиоматические системы
Простая аксиоматическая система
Метатеоремы (теорема Эрбрана-Тарского, правило замены, принцип подстановки)
Аксиоматическая система натурального вывода
Аксиоматические системы для исчисления предикатов
Простая аксиоматическая система
Аксиоматическая система натурального вывода
Теории первого порядка Введение в теорию алгоритмов
Вычислимость и разрешимость
Машины Поста и Тьюринга
Машина Поста
Программа машины Поста
Машина Тьюринга
Определение машины Тьюринга как виртуального вычислительного устройства
Формальное определение машины Тьюринга
Классы формальных языков
Классы машин Тьюринга и их свойства
Автомат с линейно-ограниченной памятью (ЛО-автоматы)
Двухленточная машина Тьюринга
Автоматы с магазинной памятью (МП-автоматы)
Нормальные алгорифмы маркова
Заключение