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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
м
Строка 40: Строка 40:
 
'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Наивная теория множеств. Кардинальные числа в наивной теории множеств. Выразительные возможности теории множеств. Парадоксы теории множеств.
 
'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Наивная теория множеств. Кардинальные числа в наивной теории множеств. Выразительные возможности теории множеств. Парадоксы теории множеств.
  
''Слайды остальных лекций будут появляться здесь по мере проведения лекций.''
+
''Версии лекций [[Media: Mathlog_318_lecture_14.pdf|14]], [[Media: Mathlog_318_lecture_15.pdf|15]], [[Media: Mathlog_318_lecture_16.pdf|16]], [[Media: Mathlog_318_lecture_17.pdf|17]] и [[Media: Mathlog_318_lecture_18.pdf|18]] с непоправленными опечатками и недоделанным оформлением, но содержащие весь необходимый материал.''
 
+
''На всякий случай выложены предварительные версии лекций [[Media: Mathlog_318_lecture_14.pdf|14]], [[Media: Mathlog_318_lecture_15.pdf|15]], [[Media: Mathlog_318_lecture_16.pdf|16]], [[Media: Mathlog_318_lecture_17.pdf|17]] и [[Media: Mathlog_318_lecture_18.pdf|18]]. Эти слайды ещё будут исправляться.''
+
  
 
= Семинары =
 
= Семинары =

Версия 14:27, 8 июня 2016

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

Объявления

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

  • 2016.06.07 17:56 Поправлены неточности в лекции 13
  • 2016.06.03 03:14 Добавлена программа курса
  • 2016.06.03 00:02 Обновлена информация о задачах
  • 2016.06.02 23:56 Обновлена информация об экзамене
  • 2016.06.02 22:55 Добавлены материалы всех семинаров
  • 2016.05.20 13:42 Добавлен черновой вариант лекции 18

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

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

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

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

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

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

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

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

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

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

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

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

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

Лекция 13. Наивная теория множеств. Кардинальные числа в наивной теории множеств. Выразительные возможности теории множеств. Парадоксы теории множеств.

Версии лекций 14, 15, 16, 17 и 18 с непоправленными опечатками и недоделанным оформлением, но содержащие весь необходимый материал.

Семинары

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

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

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

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

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

Результаты контрольной работы от 1 апреля 2016 года.

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

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

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

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

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

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

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

Лекция 10.

Доказать теорему Гёделя о полноте.

Справившиеся с задачей раньше остальных имеют возможность выбрать один бонус из нескольких видов. Все виды бонусов и возможности их выбрать - ниже.

  • "Отлично" за экзамен может выбрать один решивший задачу. бонус занят
  • "Хорошо" за экзамен могут выбрать двое решивших задачу. оба бонуса заняты
  • Бонус +5 баллов может выбрать сколько угодно решивших задачу.

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

Лекция 11.

  • Доказать теорему Гёделя о неполноте (целиком): +5 баллов каждому решившему
  • Частичное доказательство теоремы, если теорема целиком не доказана:
    • Обосновать утверждение об арифметизуемости графика вычислимой функции: +2 балла каждому решившему
    • Доказать лемму о диагонали и пояснить содержательный смысл формулы, определяемой леммой: +1 балл каждому решившему

Арифметика Пеано

Адаптировать набросок доказательства теоремы Гёделя о неполноте (лекция 11) к обоснованию неполноты арифметики Пеано. Обосновать справедливость модифицированных частей (без теоремы Гёделя о полноте, если она возникнет в процессе адаптации). +3 балла каждому решившему.

Описание арифметики Пеано здесь.

Эпистемическая логика

Описать ход рассуждений мудрецов в задаче о трёх мудрецах (лекция 16) в виде наборов модальных формул (знаний) и законов преобразования знаний, содержательно пояснить эти формулы и законы. +2 балла каждому решившему.

Законы темпоральной логики

Все пункты задачи относятся к законам темпоральной логики (лекция 17).

  • Выбрать одну пару двойственных левых частей для предполагаемых законов дистрибутивности (1+2, 3+4, 5+6, 7+8), сформулировать правые части, описывающие дистрибутивность операций в естественном понимании, и доказать и/или опровергнуть полученные законы.
  • Доказать закон неподвижной точки для одного из операторов U, R.
  • Сформулировать закон, не более тривиальный, чем законы дистрибутивности для темпоральных операторов, и доказать его.

Один сдающий может выбрать только один закон (или пару законов дистрибутивности), не выбранный ранее другими сдавшими. +1 балл каждому решившему.

Уже решённые пункты:

  • законы дистрибутивности 1+2, 3+4

Model checking для LTL

Доказать (додоказать) утверждение, представленное в слайдах лекции 18.

  • Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. +2 балла каждому решившему.
  • Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. +3 балла каждому решившему.

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

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

  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 с.