Математическая логика (318, 319/2, 241, 242) — различия между версиями

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
Строка 5: Строка 5:
 
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
 
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
  
 +
* 2017.05.15 16:25 Задачи 2, 3, 4, 5, 7 на дополнительные бонусы: обновлено количество предоставленных решений
 
* 2017.04.25 18:15 Исправлено условие задачи 5 экзамена (и аналогичной второй контрольной): достаточно сформулировать аксиому
 
* 2017.04.25 18:15 Исправлено условие задачи 5 экзамена (и аналогичной второй контрольной): достаточно сформулировать аксиому
* 2017.04.21 16:52 Задачи 2, 3, 5 на дополнительные бонусы: обновлено количество предоставленных решений
 
 
* 2017.04.24 16:45 Добавлена лекция 14
 
* 2017.04.24 16:45 Добавлена лекция 14
 
* 2017.04.23 21:17 Обновлены материалы семинара по аксиоматической теории множеств
 
* 2017.04.23 21:17 Обновлены материалы семинара по аксиоматической теории множеств
Строка 192: Строка 192:
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
  
'''Группа 318:''' 1
+
'''Группа 318:''' 2
  
 
'''Группа 241:''' 2
 
'''Группа 241:''' 2
Строка 206: Строка 206:
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
  
'''Группа 318:''' 1
+
'''Группа 318:''' 2
  
 
'''Группа 241:''' 2
 
'''Группа 241:''' 2
Строка 220: Строка 220:
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
  
'''Группа 318:''' 0
+
'''Группа 318:''' 1
  
 
'''Группа 241:''' 0
 
'''Группа 241:''' 0
Строка 239: Строка 239:
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
  
'''Группа 318:''' 0
+
'''Группа 318:''' 1
  
'''Группа 241:''' 1
+
'''Группа 241:''' 2
  
 
== Теорема о разрешимости доопределения теории ==
 
== Теорема о разрешимости доопределения теории ==
Строка 276: Строка 276:
 
=== Количество предоставленных решений ===
 
=== Количество предоставленных решений ===
  
'''Группа 318:''' 0
+
'''Группа 318:'''
 +
* лемма о диагонали: 1
 +
* утверждение об арифметизуемости: 1
 +
* рекурсивно перечислимое множество аксиом: 0
 +
* арифметика Пеано: 0
  
'''Группа 241:''' 0
+
'''Группа 241:'''
 +
* лемма о диагонали: 1
 +
* утверждение об арифметизуемости: 0
 +
* рекурсивно перечислимое множество аксиом: 0
 +
* арифметика Пеано: 0
  
 
<!--
 
<!--

Версия 16:26, 15 мая 2017

Обязательный курс для студентов 318 группы 6 семестра обучения, а также для студентов 241 группы (Математическая логика и теория алгоритмов). Курс читает В. В. Подымов.

Объявления

В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса

  • 2017.05.15 16:25 Задачи 2, 3, 4, 5, 7 на дополнительные бонусы: обновлено количество предоставленных решений
  • 2017.04.25 18:15 Исправлено условие задачи 5 экзамена (и аналогичной второй контрольной): достаточно сформулировать аксиому
  • 2017.04.24 16:45 Добавлена лекция 14
  • 2017.04.23 21:17 Обновлены материалы семинара по аксиоматической теории множеств
  • 2017.04.23 19:20 Описание задач 5, 6 экзамена (и аналогичных второй контрольной) исправлено для соответствия терминологии, используемой в лекциях
  • 2017.04.15 22:15 Проверена контрольная работа, итоги - в разделе "Контрольная работа"
  • 2017.04.13 15:00 Добавлены задачи 6, 7 на дополнительные бонусы
  • 2017.04.13 14:15 Задача 1 на дополнительные бонусы: обновлено количество предоставленных решений

Содержание

Слайды лекций

Здесь будут выкладываться слайды лекций по мере их чтения

Лекция 1. Что такое логика. Содержание курса. История логики. Логические парадоксы.

Лекция 2. Логика высказываний: синтаксис, семантика, выполнимость, общезначимость, метод семантических таблиц, алгоритм DPLL.

Лекция 3. Логика предикатов: синтаксис (термы и формулы), семантика (интерпретации и отношение выполнимости), модели, логическое следствие, проблема общезначимости формул.

Лекция 4. Подстановки. Метод семантических таблиц в логике предикатов, корректность табличного вывода.

Лекция 5. Полнота табличного вывода. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем. Теорема Чёрча.

Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.

Лекция 7. Задача унификации. Алгоритм унификации.

Лекция 8. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема Эрбрана.

Лекция 9. Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.

Лекция 10. Аксиоматические теории первого порядка. Теория частичных порядков. Основные свойства теорий: непротиворечивость, разрешимость, независимость, полнота. Теория равенства. Исчисление предикатов. Теорема Гёделя о полноте.

Лекция 11. Формальная арифметика. Явные логические определения. Теорема Гёделя о неполноте. Аксиомы равенства. Арифметика Пресбургера.

Лекция 12. Бескванторные теории с равенством. Линейная арифметика. Теория массивов. Теория равенства с неинтерпретируемыми функциями. Комбинация SMT и SAT.

Лекция 13. Наивная теория множеств: основные понятия, кардинальные числа, выразительные возможности, парадоксы.

Лекция 14. Доопределение теорий. Теория множеств Цермело-Френкеля: сигнатура, аксиомы, вопрос непротиворечивости.

Слайды 2015-2016 учебного года

Здесь временно хранятся ссылки на слайды, по которым рассказывался курс в 2015-2016 учебном году

15, 16, 17, 18.

Семинары

Семинары 1-4 проводятся по этому сборнику задач

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к расширенному сборнику задач

Материалы семинаров по основам аксиоматических теорий и задачам выполнимости формул.

Материалы семинара по аксиоматической теории множеств.

Контрольная работа

Результаты контрольной работы 10.04.2017.

Формат проведения и длительность контрольной работы: письменно, 95 минут.

В рамках контрольной работы требуется решить

  • три задачи:
    • построить формулу логики предикатов, адекватно описывающую высказывание, представленное на естественном языке;
    • проверить общезначимость формулы логики предикатов, используя метод семантических таблиц
      • (правила табличного вывода будут выданы вместе с заданием контрольной);
    • проверить общезначимость формулы логики предикатов, используя метод резолюций;
  • девять теоретических вопросов, проверяющих знание материала, изложенного в лекциях 2-9.

Контрольная работа оценивается по шкале от 0 до 15 баллов. Итоговые баллы за работу - это сумма баллов за задачи и теоретические вопросы.

Правильно решённая задача оценивается в 2 балла. Задача, решённая с ошибками, может быть оценена числом баллов от 0 до 2 в зависимости от качества и количества ошибок.

Правильно решённый теоретический вопрос оценивается в 1 балл. В каждом теоретическом вопросе предлагается несколько вариантов ответа. Среди этих ответов может быть один, ни одного или несколько правильных. Для правильного решения теоретического вопроса следует отметить все правильные ответы и только их. Обоснование того, почему выбраны или не выбраны те или иные ответы, не требуется.

По результатам контрольной работы определяется бонус или штраф, суммирующийся с баллами за экзаменационную работу:

  • набрано от 13 до 15 баллов: бонус +3 балла;
  • набрано от 10 до 12 баллов: бонус +1 балл;
  • набрано от 7 до 9 баллов: штраф -1 балл;
  • набрано 6 баллов или меньше: штраф -3 балла;
  • контрольная работа пропущена по неуважительной причине: штраф -3 балла;
  • контрольная работа пропущена по уважительной причине: бонус +0 баллов.

Экзамен

Формат проведения и длительность экзамена: письменно, 150 минут.

Экзаменационная работа оценивается по шкале от 0 до 40 баллов (промежуточные баллы). Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить. В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:

  • набрано 32 балла или больше: отлично;
  • набрано от 24 до 31 балла: хорошо;
  • набрано от 16 до 23 баллов: удовлетворительно;
  • набрано 15 баллов или меньше: неудовлетворительно.

Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе. Описание задач и оценки за их безошибочное решение:

  • Задача 1 (3 балла): предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке.
  • Задача 2 (3 балла): проверить общезначимость формулы логики предикатов методом семантических таблиц.
  • Задача 3 (3 балла): проверить общезначимость формулы логики предикатов методом резолюций.
  • Задача 4 (6 баллов): для заданной массовой задачи описать алгоритм построения бескванторной формулы линейной целочисленной арифметики (или формулы логики высказываний), такую что а) формула выполнима тогда и только тогда, когда задача имеет решение, и б) по выполняющему набору можно быстро получить ответ к задаче; выписать формулу, получаемую в результате работы алгоритма на заданных входных данных.
  • Задача 5 (3 балла): предложить аксиому, адекватно определяющую теоретико-множественное понятие или понятие, которое можно переформулировать в терминах теории множеств, в сигнатуре теории Цермело-Френкеля.
  • Задачи 6-10 (2 балла за каждую) состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, без пояснений (как правило - "да" или "нет" либо привести какой-либо пример).
  • Задачи 11-14 (3 балла за каждую): из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать (невыбранные ответы обосновывать не нужно).

Зачёт

В зачётную неделю будет проведена вторая контрольная работа. Эта работа будет содержать

  • две задачи, идентичные задачам 4, 5 экзамена:
    • правильно решённый аналог задачи 4 оценивается в 4 балла,
    • правильно решённый аналог задачи 5 оценивается в 2 балла
    • 9 теоретических вопросов по лекциям 10-18, аналогичные теоретическим вопросам первой контрольной работы.

Для получения зачёта необходимо набрать хотя бы две трети баллов суммарно за две контрольные работы и дополнительные бонусы, то есть не менее 20 баллов.

Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках

  • сохраняются баллы, полученные ранее за решение задач,
  • сохраняются дополнительные бонусы,
  • предоставляется возможность перерешать задачи, не решённые на полный балл,
  • сгорают баллы, полученные за теоретические вопросы.

Точный формат проведения дополнительных попыток получения зачёта будет определён позднее.

Дополнительные бонусы к экзамену и зачёту

Общее условие сдачи задач на дополнительные бонусы:

  • принцип сдачи задач:
    • идеи и выкладки, не требующие технических деталей, - устно;
    • если выкладки не воспроизводятся или не воспринимаются устно, то письменно;
  • при подготовке и сдаче можно пользоваться любыми материалами;
  • при сдаче проверяется понимание каждой детали решения задачи - следует быть к этому готовым;
  • задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения задачи.

Бонусы за решение задач сформулированы для одной учебной группы и получаются внутри одной группы независимо от другой (например, "первый предоставивший решение" трактуется как "первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241".

Условия задач и поощрения за их решения будут появляться в слайдах лекций и в этом разделе.

Полнота табличного вывода в логике предикатов

Описание задачи

Адаптировать доказательство теоремы полноты табличного вывода в логике предикатов к более общему случаю:

  • сигнатура алфавита состоит из
    • счётно-бесконечного числа констант: c1, c2, c3, ... ,
    • счётно-бесконечного числа функциональных символов: f1, f2, f3, ... ,
    • счётно-бесконечного числа предикатных символов: P1, P2, P3, ... ;
  • формулы исходной таблицы могут содержать свободные переменные;
  • исходная таблица содержит не более чем счётно-бесконечное число формул, и при этом
    • формулы в левой части таблицы нумерованы натуральными числами, и существует алгоритм, по натуральному числу i выдающий i-ю формулу (то есть в доказательстве можно говорить "``возьмём i-ю формулу из левой части исходной таблицы")
    • формулы в правой части таблицы нумерованы натуральными числами, и существует алгоритм, по натуральному числу i выдающий i-ю формулу (то есть в доказательстве можно говорить "``возьмём i-ю формулу из правой части исходной таблицы")

Бонусы за решение задачи:

  • первый предоставивший решение: +3 балла
  • второй предоставивший решение: +2 балла
  • третий предоставивший решение: +1 балл

Количество предоставленных решений

Группа 318: 1

Группа 241: 0

Утверждения об отношении равносильности

Описание задачи

Доказать два утверждения об отношении равносильности, сформулированные в лекции 6 с доказательством, помеченным словом "Самостоятельно".

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

Количество предоставленных решений

Группа 318: 2

Группа 241: 2

Фундированность троек чисел

Описание задачи

Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 7, сформулированная при доказательстве завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").

Бонус за решение задачи: +2 балла первым двум предоставившим решение задачи

Количество предоставленных решений

Группа 318: 2

Группа 241: 2

Неизоморфные элементарно эквивалентные интерпретации

Описание задачи

Привести пример двух неизоморфных элементарно эквивалентных интерпретаций, обосновать их неизоморфность и элементарную эквивалентность (см. лекцию 10).

Бонус за решение задачи: +2 балла первому предоставившему решение, +1 балл - второму.

Количество предоставленных решений

Группа 318: 1

Группа 241: 0

Теорема Гёделя о полноте

Описание задачи

Доказать теорему Гёделя о полноте (см. лекцию 10).

Бонусы за решение задачи:

  • +15 баллов первому предоставившему решение,
  • +12 баллов второму предоставившему решение,
  • +9 баллов третьему предоставившему решение,
  • +6 баллов четвёртому предоставившему решение,
  • +3 баллов пятому предоставившему решение.

Количество предоставленных решений

Группа 318: 1

Группа 241: 2

Теорема о разрешимости доопределения теории

Описание задачи

Завершить доказательство этой теоремы, предложенное в лекции 11, или предложить своё доказательство

Бонусы за решение задачи:

  • первый предоставивший решение: +3 балла
  • второй предоставивший решение: +2 балла
  • третий предоставивший решение: +1 балл

Количество предоставленных решений

Группа 318: 0

Группа 241: 0

Теорема Гёделя о неполноте

Описание задачи

Доказать теорему Гёделя о неполноте (см. лекцию 11) или адаптировать доказательство в лекции 11 к более простому утверждению: арифметика Пеано неполна.

Каждая часть доказательства оценивается отдельно:

  1. лемма о диагонали (описать требуемое предложение и пояснить его содержательный смысл): +2 балла первому решившему, +1 балл второму решившему;
  2. утверждение об арифметизуемости графика вычислимой функции: +3 балла первому решившему, +2 балла второму решившему, +1 балл третьему решившему;
  3. остальная часть доказательства: +4 балла первому решившему, +3 балла второму решившему, +2 балла третьему решившему, +1 балл четвёртому решившему;
  4. доказательство неполноты арифметики Пеано, кроме леммы о диагонали, утверждении об арифметизуемости графика вычислимой функции и других утверждений, встречающихся в курсе
    • не оценивается, если предоставлено решение пункта 3
    • +3 балла первому решившему, +2 балла второму решившему, +1 балл третьему решившему.

Количество предоставленных решений

Группа 318:

  • лемма о диагонали: 1
  • утверждение об арифметизуемости: 1
  • рекурсивно перечислимое множество аксиом: 0
  • арифметика Пеано: 0

Группа 241:

  • лемма о диагонали: 1
  • утверждение об арифметизуемости: 0
  • рекурсивно перечислимое множество аксиом: 0
  • арифметика Пеано: 0


Программа курса

Классические логики

  1. Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.
  2. Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
  3. Проблема выполнимости булевых формул: приложения, основные решающие алгоритмы (алгоритм локального поиска, алгоритм DPLL).
  4. Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
  5. Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
  6. Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
  7. Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теорема корректности табличного вывода, теорема полноты табличного вывода.
  8. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.
  9. Равносильные формулы. Теорема о равносильной замене.

Метод резолюций в логике предикатов

  1. Предварённая нормальная форма. Теорема о предварённой нормальной форме.
  2. Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
  3. Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.
  4. Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
  5. Лемма о связке. Алгоритм унификации. Теорема об унификации.
  6. Правило резолюции. Правило склейки. Резолютивный вывод. Теорема корректности резолютивного вывода.
  7. Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
  8. Лемма об основных дизъюнктах. Лемма о подъёме. Теорема полноты резолютивного вывода.
  9. Метод резолюций: общая схема, применение.
  10. Стратегии резолютивного вывода. Семантическая резолюция. Теорема полноты семантического резолютивного вывода. Входной резолютивный вывод.
  11. Резолютивный вывод как средство вычисления. Хорновские дизъюнкты.

Аксиоматические теории первого порядка

  1. Аксиомы. Аксиоматическая теория первого порядка: определение; выполнимость, общезначимость и противоречивость формул в теории. Проблемы общезначимости и выполнимости формул логики предикатов в теории.
  2. Основные свойства теорий: непротиворечивость, разрешимость, категоричность, полнота. Изоморфизм и элементарная эквивалентность интерпретаций. Связь изоморфизма интерпретаций, элементарной эквивалентности интерпретаций и полноты теорий.
  3. Теория частичных порядков. Теория равенства: непротиворечивость, разрешимость, некатегоричность.
  4. Исчисление предикатов: схемы аксиом, правило modus ponens, правило обобщения, логический вывод. Теорема Гёделя о полноте. Аксиоматические теории и исчисления.
  5. Формальная арифметика. Теорема Гёделя о неполноте. Нумерации Гёделя. Арифметизуемые отношения.
  6. Арифметика Пресбургера: непротиворечивость, разрешимость, полнота.
  7. Бескванторные теории первого порядка. Теории с равенством. Преимущества проблемы выполнимости формул в теории перед проблемой общезначимости.
  8. Теория равенства с неинтерпретируемыми функциями, разрешимость теории: сведение проблемы выполнимости в теории к проблеме выполнимости булевых формул.
  9. Линейная арифметика. Виды линейных арифметик. NP-полнота линейной целочисленной арифметики.
  10. Комбинация решающих алгоритмов для проблем выполнимости формул в теориях и в логике высказываний. Остовная проверка выполнимости формул в теориях. Интеграция алгоритмов проверки выполнимости формул в теориях в алгоритм DPLL.

Аксиоматическая теория множеств

  1. Наивная теория множеств. Сравнение мощностей множеств. Кардинальные числа в наивной теории множеств.
  2. Теорема Кантора. Теорема об объединении множества, неограниченного по мощности. Теорема Кантора-Бернштейна.
  3. Примеры кардинальных чисел. Конечность множеств мощности меньше счётной. Континуум-гипотеза в наивной теории множеств.
  4. Выразительные возможности наивной теории множеств: натуральные числа, кортежи, функции. Парадоксы теории множеств.
  5. Аксиоматические теории множеств. Теория Цермело-Френкеля: аксиомы и схемы аксиом, доказательство существования основных множеств наивной теории, исключение основных парадоксов теории множеств. Вопросы непротиворечивости теории Цермело-Френкеля.
  6. Определимость функций и отношений в теории. Применение определений для расширения теории.
  7. Аксиома выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и её отрицанием.
  8. Ординальные числа. Основные свойства ординальных чисел. Арифметика ординальных чисел.
  9. Теорема Цермело. Кардинальные числа в теории Цермело-Френкеля с аксиомой выбора.
  10. Континуум-гипотеза в теории Цермело-Френкеля с аксиомой выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и континуум-гипотезой, её отрицанием.

Неклассические прикладные логики

  1. Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
  2. Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара.
  3. Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
  4. Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача проверки выполнимости формул логики линейного времени на размеченных системах переходов.
  5. Позитивная форма формул логики линейного времени. Замыкание Фишера-Ладнера. Согласованные множества формул. Системы Хинтикки. Табличный метод проверки выполнимости формул логики линейного времени на размеченных системах переходов.

Рекомендованная литература

Основная литература

  1. Клини С. Математическая логика. М.:Мир, 1973, 480 с.
  2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
  3. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
  4. Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
  5. Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
  6. Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
  7. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

Дополнительная литература

  1. Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
  2. Верещагин Н.К., Шень А. Языки и исчисления. 2004.
  3. Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
  4. Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
  5. Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
  6. Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
  7. Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
  8. Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
  9. Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
  10. Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
  11. Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
  12. Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
  13. Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.