Математическая логика (318, 319/2, 241, 242) — различия между версиями
PodymovVV (обсуждение | вклад) м |
PodymovVV (обсуждение | вклад) |
||
Строка 1: | Строка 1: | ||
+ | [[Категория:Лекционные курсы кафедры МК]] | ||
+ | |||
Обязательный курс для студентов 318 группы 6 семестра обучения, ''а также для студентов 241 группы (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]]. | Обязательный курс для студентов 318 группы 6 семестра обучения, ''а также для студентов 241 группы (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]]. | ||
Строка 5: | Строка 7: | ||
''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса'' | ''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса'' | ||
− | * | + | * 2018.02.11 23:28 Страница подготовлена к началу весеннего семестра 2017/2018 учебного года |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
= Слайды лекций = | = Слайды лекций = | ||
Строка 17: | Строка 13: | ||
''Здесь будут выкладываться слайды лекций по мере их чтения'' | ''Здесь будут выкладываться слайды лекций по мере их чтения'' | ||
− | + | == Временный архив слайдов: 2016-2017 учебный год == | |
− | '''[[Media: Mathlog_318_lecture_2.pdf| | + | '''[[Media: Mathlog_318_lecture_1.pdf|1]]''', |
− | + | '''[[Media: Mathlog_318_lecture_2.pdf|2]]''', | |
− | '''[[Media: Mathlog_318_lecture_3.pdf| | + | '''[[Media: Mathlog_318_lecture_3.pdf|3]]''', |
− | + | '''[[Media: Mathlog_318_lecture_4.pdf|4]]''', | |
− | '''[[Media: Mathlog_318_lecture_4.pdf| | + | '''[[Media: Mathlog_318_lecture_5.pdf|5]]''', |
− | + | '''[[Media: Mathlog_318_lecture_6.pdf|6]]''', | |
− | '''[[Media: Mathlog_318_lecture_5.pdf| | + | '''[[Media: Mathlog_318_lecture_7.pdf|7]]''', |
− | + | '''[[Media: Mathlog_318_lecture_8.pdf|8]]''', | |
− | '''[[Media: Mathlog_318_lecture_6.pdf| | + | '''[[Media: Mathlog_318_lecture_9.pdf|9]]''', |
− | + | '''[[Media: Mathlog_318_lecture_10.pdf|10]]''', | |
− | '''[[Media: Mathlog_318_lecture_7.pdf| | + | '''[[Media: Mathlog_318_lecture_11.pdf|11]]''', |
− | + | '''[[Media: Mathlog_318_lecture_12.pdf|12]]''', | |
− | '''[[Media: Mathlog_318_lecture_8.pdf| | + | '''[[Media: Mathlog_318_lecture_13.pdf|13]]''', |
− | + | '''[[Media: Mathlog_318_lecture_14.pdf|14]]''', | |
− | '''[[Media: Mathlog_318_lecture_9.pdf| | + | '''[[Media: Mathlog_318_lecture_16_17.pdf|16-17]]'''. |
− | + | ||
− | '''[[Media: Mathlog_318_lecture_10.pdf| | + | |
− | + | ||
− | '''[[Media: Mathlog_318_lecture_11.pdf| | + | |
− | + | ||
− | '''[[Media: Mathlog_318_lecture_12.pdf| | + | |
− | + | ||
− | '''[[Media: Mathlog_318_lecture_13.pdf| | + | |
− | + | ||
− | '''[[Media: Mathlog_318_lecture_14.pdf| | + | |
− | + | ||
− | + | ||
− | + | ||
− | '''[[Media: Mathlog_318_lecture_16_17.pdf| | + | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
= Семинары = | = Семинары = | ||
Строка 64: | Строка 37: | ||
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]] | Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]] | ||
− | + | ''Материалы остальных семинаров будут появляться по мере проведения занятий.'' | |
− | + | ||
− | + | ||
= Контрольная работа = | = Контрольная работа = | ||
− | |||
− | |||
Формат проведения и длительность контрольной работы: письменно, 95 минут. | Формат проведения и длительность контрольной работы: письменно, 95 минут. | ||
Строка 92: | Строка 61: | ||
В каждом теоретическом вопросе предлагается несколько вариантов ответа. | В каждом теоретическом вопросе предлагается несколько вариантов ответа. | ||
Среди этих ответов может быть один, ни одного или несколько правильных. | Среди этих ответов может быть один, ни одного или несколько правильных. | ||
− | Для правильного решения теоретического вопроса следует отметить ''все'' правильные ответы и только их. | + | Для правильного решения теоретического вопроса следует отметить '''все''' правильные ответы и только их. |
− | Обоснование того, почему выбраны или не выбраны те или иные ответы, ''не требуется''. | + | Обоснование того, почему выбраны или не выбраны те или иные ответы, '''не требуется'''. |
− | + | ''Группа 241:'' баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для зачёта. | |
+ | ''Группа 318:'' по результатам контрольной работы определяется <span style="background:#DDFFDD">бонус</span> или <span style="background:#FFDDDD">штраф</span>, суммирующийся с баллами за экзаменационную работу: | ||
* набрано от 13 до 15 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>; | * набрано от 13 до 15 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>; | ||
* набрано от 10 до 12 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>; | * набрано от 10 до 12 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>; | ||
Строка 106: | Строка 76: | ||
= Экзамен = | = Экзамен = | ||
− | + | Формат проведения и длительность экзамена: письменно, 120 минут. | |
− | + | Экзаменационная работа оценивается по шкале '''от 0 до 30 баллов''' (''промежуточные баллы''). | |
− | + | ||
− | Экзаменационная работа оценивается по шкале '''от 0 до | + | |
Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить. | Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить. | ||
В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен: | В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен: | ||
− | + | * набрано хотя бы 25 баллов: '''отлично'''; | |
− | * набрано | + | * набрано хотя бы 20, но менее 25 баллов: '''хорошо'''; |
− | * набрано | + | * набрано хотя бы 15, но менее 20 баллов: '''удовлетворительно'''; |
− | * набрано | + | * набрано менее 15 баллов: '''неудовлетворительно'''. |
− | * набрано 15 баллов | + | |
Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе. | Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе. | ||
Описание задач и оценки за их безошибочное решение: | Описание задач и оценки за их безошибочное решение: | ||
− | |||
* '''Задача 1 (3 балла)''': предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке. | * '''Задача 1 (3 балла)''': предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке. | ||
* '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц. | * '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц. | ||
* '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций. | * '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций. | ||
− | * '''Задача 4 ( | + | * '''Задача 4 (3 балла)''': ''точная формулировка будет определена по окончании лекций и семинаров''. |
− | * '''Задача 5 (3 балла)''': | + | * '''Задача 5 (3 балла)''': ''точная формулировка будет определена по окончании лекций и семинаров''. |
− | * '''Задачи 6- | + | * '''Задачи 6-9 (2 балла за каждую)''' состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, '''без пояснений''' (как правило - "да" или "нет", либо привести какой-либо пример). |
− | * '''Задачи | + | * '''Задачи 10-12 (3 балла за каждую)''': из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать ('''невыбранные ответы обосновывать не нужно'''). |
= Зачёт = | = Зачёт = | ||
В зачётную неделю будет проведена вторая контрольная работа. Эта работа будет содержать | В зачётную неделю будет проведена вторая контрольная работа. Эта работа будет содержать | ||
− | * | + | * Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла. |
− | + | * Пять теоретических вопросов по лекциям 10-18 по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл. | |
− | + | ||
− | * | + | |
− | Для получения зачёта необходимо набрать хотя бы две трети баллов суммарно за две контрольные работы и дополнительные бонусы, то есть '''не менее | + | Для получения зачёта необходимо набрать хотя бы две трети баллов суммарно за две контрольные работы и дополнительные бонусы, то есть '''не менее 18 баллов'''. |
− | Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках | + | Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках: |
− | * | + | * Сохраняются баллы за каждую задачу, суммарный балл за теоретические вопросы первой контрольной работы, суммарный балл за теоретические вопросы второй контрольной работы. |
− | + | * Предоставляется возможность поднять каждый из этих баллов, решив соответствующие части новых вариантов контрольных работ. | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
= Дополнительные бонусы к экзамену и зачёту = | = Дополнительные бонусы к экзамену и зачёту = | ||
Строка 160: | Строка 120: | ||
'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый предоставивший решение''" трактуется как "''первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241''". | '''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый предоставивший решение''" трактуется как "''первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241''". | ||
− | ''Условия задач и поощрения за их решения будут появляться в слайдах лекций и в этом разделе.'' | + | ''Условия задач и поощрения за их решения будут появляться в слайдах лекций и в этом разделе по мере проведения занятий.'' |
+ | |||
+ | <!-- | ||
== Полнота табличного вывода в логике предикатов == | == Полнота табличного вывода в логике предикатов == | ||
Строка 334: | Строка 296: | ||
<s>'''Группа 241:''' AX, AG</s> (''уже не актуально'') | <s>'''Группа 241:''' AX, AG</s> (''уже не актуально'') | ||
− | |||
− | |||
== Законы темпоральной логики == | == Законы темпоральной логики == | ||
Строка 358: | Строка 318: | ||
* Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. <span style="background:#DDFFDD">+2 балла</span> каждому решившему. | * Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. <span style="background:#DDFFDD">+2 балла</span> каждому решившему. | ||
* Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. <span style="background:#DDFFDD">+3 балла</span> каждому решившему. | * Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. <span style="background:#DDFFDD">+3 балла</span> каждому решившему. | ||
+ | |||
--> | --> | ||
= Программа курса = | = Программа курса = | ||
+ | |||
+ | ''Раздел будет дополняться по мере проведения занятий.'' | ||
== Классические логики == | == Классические логики == | ||
Строка 389: | Строка 352: | ||
<li> Резолютивный вывод как средство вычисления. Хорновские дизъюнкты. | <li> Резолютивный вывод как средство вычисления. Хорновские дизъюнкты. | ||
</ol> | </ol> | ||
+ | |||
+ | <!-- | ||
== Аксиоматические теории первого порядка == | == Аксиоматические теории первого порядка == | ||
Строка 426: | Строка 391: | ||
<li> Позитивная форма формул логики линейного времени. Замыкание Фишера-Ладнера. Согласованные множества формул. Системы Хинтикки. Табличный метод проверки выполнимости формул логики линейного времени на размеченных системах переходов. | <li> Позитивная форма формул логики линейного времени. Замыкание Фишера-Ладнера. Согласованные множества формул. Системы Хинтикки. Табличный метод проверки выполнимости формул логики линейного времени на размеченных системах переходов. | ||
</ol> | </ol> | ||
+ | |||
+ | --> | ||
= Рекомендованная литература = | = Рекомендованная литература = | ||
Строка 453: | Строка 420: | ||
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с. | # Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с. | ||
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с. | # Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с. | ||
− | |||
− |
Версия 23:28, 11 февраля 2018
Обязательный курс для студентов 318 группы 6 семестра обучения, а также для студентов 241 группы (Математическая логика и теория алгоритмов). Курс читает В. В. Подымов.
Объявления
В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса
- 2018.02.11 23:28 Страница подготовлена к началу весеннего семестра 2017/2018 учебного года
Содержание
Слайды лекций
Здесь будут выкладываться слайды лекций по мере их чтения
Временный архив слайдов: 2016-2017 учебный год
1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16-17.
Семинары
Семинары 1-4 проводятся по этому сборнику задач
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к расширенному сборнику задач
Материалы остальных семинаров будут появляться по мере проведения занятий.
Контрольная работа
Формат проведения и длительность контрольной работы: письменно, 95 минут.
В рамках контрольной работы требуется решить
- три задачи:
- построить формулу логики предикатов, адекватно описывающую высказывание, представленное на естественном языке;
- проверить общезначимость формулы логики предикатов, используя метод семантических таблиц
- (правила табличного вывода будут выданы вместе с заданием контрольной);
- проверить общезначимость формулы логики предикатов, используя метод резолюций;
- девять теоретических вопросов, проверяющих знание материала, изложенного в лекциях 2-9.
Контрольная работа оценивается по шкале от 0 до 15 баллов. Итоговые баллы за работу - это сумма баллов за задачи и теоретические вопросы.
Правильно решённая задача оценивается в 2 балла. Задача, решённая с ошибками, может быть оценена числом баллов от 0 до 2 в зависимости от качества и количества ошибок.
Правильно решённый теоретический вопрос оценивается в 1 балл. В каждом теоретическом вопросе предлагается несколько вариантов ответа. Среди этих ответов может быть один, ни одного или несколько правильных. Для правильного решения теоретического вопроса следует отметить все правильные ответы и только их. Обоснование того, почему выбраны или не выбраны те или иные ответы, не требуется.
Группа 241: баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для зачёта.
Группа 318: по результатам контрольной работы определяется бонус или штраф, суммирующийся с баллами за экзаменационную работу:
- набрано от 13 до 15 баллов: бонус +3 балла;
- набрано от 10 до 12 баллов: бонус +1 балл;
- набрано от 7 до 9 баллов: штраф -1 балл;
- набрано 6 баллов или меньше: штраф -3 балла;
- контрольная работа пропущена по неуважительной причине: штраф -3 балла;
- контрольная работа пропущена по уважительной причине: бонус +0 баллов.
Экзамен
Формат проведения и длительность экзамена: письменно, 120 минут.
Экзаменационная работа оценивается по шкале от 0 до 30 баллов (промежуточные баллы). Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить. В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:
- набрано хотя бы 25 баллов: отлично;
- набрано хотя бы 20, но менее 25 баллов: хорошо;
- набрано хотя бы 15, но менее 20 баллов: удовлетворительно;
- набрано менее 15 баллов: неудовлетворительно.
Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе. Описание задач и оценки за их безошибочное решение:
- Задача 1 (3 балла): предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке.
- Задача 2 (3 балла): проверить общезначимость формулы логики предикатов методом семантических таблиц.
- Задача 3 (3 балла): проверить общезначимость формулы логики предикатов методом резолюций.
- Задача 4 (3 балла): точная формулировка будет определена по окончании лекций и семинаров.
- Задача 5 (3 балла): точная формулировка будет определена по окончании лекций и семинаров.
- Задачи 6-9 (2 балла за каждую) состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, без пояснений (как правило - "да" или "нет", либо привести какой-либо пример).
- Задачи 10-12 (3 балла за каждую): из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать (невыбранные ответы обосновывать не нужно).
Зачёт
В зачётную неделю будет проведена вторая контрольная работа. Эта работа будет содержать
- Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла.
- Пять теоретических вопросов по лекциям 10-18 по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл.
Для получения зачёта необходимо набрать хотя бы две трети баллов суммарно за две контрольные работы и дополнительные бонусы, то есть не менее 18 баллов.
Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках:
- Сохраняются баллы за каждую задачу, суммарный балл за теоретические вопросы первой контрольной работы, суммарный балл за теоретические вопросы второй контрольной работы.
- Предоставляется возможность поднять каждый из этих баллов, решив соответствующие части новых вариантов контрольных работ.
Дополнительные бонусы к экзамену и зачёту
Общее условие сдачи задач на дополнительные бонусы:
- принцип сдачи задач:
- идеи и выкладки, не требующие технических деталей, - устно;
- если выкладки не воспроизводятся или не воспринимаются устно, то письменно;
- при подготовке и сдаче можно пользоваться любыми материалами;
- при сдаче проверяется понимание каждой детали решения задачи - следует быть к этому готовым;
- задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения задачи.
Бонусы за решение задач сформулированы для одной учебной группы и получаются внутри одной группы независимо от другой (например, "первый предоставивший решение" трактуется как "первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241".
Условия задач и поощрения за их решения будут появляться в слайдах лекций и в этом разделе по мере проведения занятий.
Программа курса
Раздел будет дополняться по мере проведения занятий.
Классические логики
- Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.
- Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
- Проблема выполнимости булевых формул: приложения, основные решающие алгоритмы (алгоритм локального поиска, алгоритм DPLL).
- Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
- Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
- Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
- Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теорема корректности табличного вывода, теорема полноты табличного вывода.
- Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.
- Равносильные формулы. Теорема о равносильной замене.
Метод резолюций в логике предикатов
- Предварённая нормальная форма. Теорема о предварённой нормальной форме.
- Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
- Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.
- Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
- Лемма о связке. Алгоритм унификации. Теорема об унификации.
- Правило резолюции. Правило склейки. Резолютивный вывод. Теорема корректности резолютивного вывода.
- Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
- Лемма об основных дизъюнктах. Лемма о подъёме. Теорема полноты резолютивного вывода.
- Метод резолюций: общая схема, применение.
- Стратегии резолютивного вывода. Семантическая резолюция. Теорема полноты семантического резолютивного вывода. Входной резолютивный вывод.
- Резолютивный вывод как средство вычисления. Хорновские дизъюнкты.
Рекомендованная литература
Основная литература
- Клини С. Математическая логика. М.:Мир, 1973, 480 с.
- Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
- Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
- Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
- Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.
- Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.
- Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.
Дополнительная литература
- Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
- Верещагин Н.К., Шень А. Языки и исчисления. 2004.
- Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
- Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
- Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
- Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
- Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
- Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.
- Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.
- Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.
- Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.
- Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.
- Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.