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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
м
Строка 22: Строка 22:
 
''Здесь временно хранятся ссылки на слайды, по которым рассказывался курс в 2015-2016 учебном году''
 
''Здесь временно хранятся ссылки на слайды, по которым рассказывался курс в 2015-2016 учебном году''
  
'''[[Media: Mathlog_318_lecture_3.pdf|3]]''',
 
 
'''[[Media: Mathlog_318_lecture_4.pdf|4]]''',
 
'''[[Media: Mathlog_318_lecture_4.pdf|4]]''',
 
'''[[Media: Mathlog_318_lecture_5.pdf|5]]''',
 
'''[[Media: Mathlog_318_lecture_5.pdf|5]]''',

Версия 10:26, 20 февраля 2017

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

Объявления

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

  • 2017.02.15 22:00 Немного подправлены слайды лекций 1, 2
  • 2017.01.06 18:25 Страница подготовлена к грядущему семестру

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

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

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

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

Лекция 3.

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

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

4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18.

Семинары

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

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

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

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

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

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

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

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

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

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


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

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

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