Текущая версия на 13:28, 23 апреля 2024

Актуальность информации: весенний семестр 2023/2024 учебного года.

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

Содержание

1 Слайды лекций
- 1.1 Прошлогодние слайды
2 Семинары
3 Контрольные работы
4 Зачёт
5 Экзамен
- 5.1 Контрольная работа для экзамена
6 Премиальные задачи
7 Программа курса
8 Рекомендованная литература
- 8.1 Основная литература
- 8.2 Дополнительная литература

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

Блок 1 (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.

Блок 2. Логика высказываний: синтаксис, семантика.

Блок 3. Логика предикатов: синтаксис, семантика.

Блок 4. Как формализовать предложение на языке логики предикатов (пример).

Блок 5. Логика высказываний: выполнимые и общезначимые формулы.

Блок 6. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).

Блок 7. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?

Блок 8. Метод семантических таблиц: семантические таблицы.

Блок 9. Подстановки (основные определения).

Блок 10. Метод семантических таблиц: табличный вывод.

Блок 11. Метод семантических таблиц: корректность табличного вывода.

Блок 12. Метод семантических таблиц: полнота табличного вывода.

Блок 13. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.

Блок 14. Общая схема метода резолюций.

Блок 15. Равносильность формул.

Блок 16. Предварённая нормальная форма (ПНФ).

Блок 17. Сколемовская стандартная форма (ССФ).

Блок 18. Системы дизъюнктов.

Блок 19. Композиция подстановок. Постановка задачи унификации.

Блок 20. Алгоритм унификации атомарных формул.

Блок 21. Монотонность и транзитивность отношения логического следования.

Блок 22. Резолютивный вывод. Корректность резолютивного вывода.

Блок 23. Обоснование общезначимости формулы методом резолюций (пример).

Блок 24. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

Блок 25. Теорема Эрбрана. Полнота резолютивного вывода.

Блок 26. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

Блок 27. Как устроены математические доказательства. Логические исчисления.

Блок 28. Натуральное исчисление высказываний: основные определения.

Блок 29. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.

Блок 30. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.

Блок 31. Натуральное исчисление предикатов: основные определения, корректность.

Блок 32. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).

Блок 33. Натуральное исчисление предикатов: полнота.

Блок 34. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

Блок 35. Машины Тьюринга (МТ).

Блок 36. Теорема Чёрча.

Блок 37. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

Блок 38. Основные свойства аксиоматических теорий.

Блок 39. Арифметические интерпретации и теории.

Блок 40. Определения и выразимость.

Блок 41. Формальная арифметика. Теорема Гёделя о неполноте.

Блок 42. Арифметика Пресбургера.

Блок 43. Модальные логики.

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

Прошлогодние слайды

Блок 44. Эпистемические логики.

Блок 45. Темпоральные логики.

Блок 46. Интуиционистская логика.

Блок 47. Формальная верификация.

Блок 48. Модельные императивные программы. Постановка задачи верификации программ.

Блок 49. Логика Хоара. Автоматизация проверки правильности программ.

Блок 50. Проверка правильности распределённых систем. Пара слов о методе model checking.

Блок 51. Размеченные системы переходов.

Блок 52. Спецификация систем при помощи темпоральных логик.

Блок 53. Алгоритм model checking для CTL.

Семинары

Материалы семинаров будут обновляться по мере проведения занятий

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

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

Материалы семинара 5-6 (натуральное исчисление).

Контрольные работы

Контрольные работы проводятся письменно, длительность каждой - 90 минут.

В контрольных работах встретятся 4 типовые задачи со следующими темами:

Формализовать в логике предикатов предложение, записанное на естественном языке.
Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
Обосновать общезначимость формулы логики предикатов методом резолюций.
Доказать формулу в натуральном исчислении предикатов.

Оценка решений типовых задач:

Максимальная оценка - 4 балла.
Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.

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

Первая контрольная работа будет содержать

3 типовые задачи по темам 1-3 и
9 теоретических вопросов по прочитанным лекциям.

Вторая контрольная работа будет содержать

4 типовые задачи по всем темам и
5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.

Остальные контрольные работы будут содержать

4 типовые задачи по всем темам и
14 теоретических вопросов по всем лекциям.

Зачёт

На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре. При проставлении зачёта учитывается 6 технических оценок:

Четыре оценки за типовые задачи, по одной за каждую задачу.
Оценка за знание теории. Максимум - 14 баллов.
Оценка за решение премиальных задач.

Для получения зачёта требуется получить два результата:

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

Баллы за типовые задачи и за теорию набираются на контрольных работах.

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

При проставлении зачёта учитывается максимальная оценка за теорию среди полученных

суммарно за первые две контрольные работы и
за каждую из следующих контрольных работ.

Экзамен

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

Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов. К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за контрольную работу. Согласно набранной сумме технических баллов выставляется оценка:

хотя бы 30: отлично;
хотя бы 23, но менее 30: хорошо;
хотя бы 16, но менее 23: удовлетворительно;
менее 16: неудовлетворительно.

Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:

Каждая из задач 1-4 оценивается в 4 балла. Темы задач:
1. Формализовать в логике предикатов предложение, записанное на естественном языке.
2. Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
3. Обосновать общезначимость формулы логики предикатов методом резолюций.
4. Доказать формулу в натуральном исчислении предикатов.
Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:
1. Сформулировать утверждение, определение и т.п.
2. Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
3. Аргументировать (обосновать) ответ на вопрос.
Каждая из задач 8-10 оценивается в 4 балла и устроена так:
- Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и обосновать выбранные ответы.
- Невыбранные ответы обосновывать не нужно.

Контрольная работа для экзамена

На оценку за экзамен влияет первая контрольная работа. Максимальная техническая оценка за эту работу - 21 балл. В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:

Набрано хотя бы 19 баллов: бонус +3 балла;
Набрано хотя бы 16, но менее 19 баллов: бонус +2 балла;
Набрано хотя бы 13, но менее 16 баллов: бонус +1 балл;
Набрано хотя бы 10, но менее 13 баллов: 0 баллов;
Набрано хотя бы 7, но менее 10 баллов: штраф -1 балл;
Набрано хотя бы 4, но менее 7 баллов: штраф -2 балла;
Набрано менее 4 баллов: штраф -3 балла;
Неявка без уважительной причины: штраф -3 балла;
Неявка по уважительной причине: 0 баллов.

Премиальные задачи

Общие условия сдачи решений премиальных задач:

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

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

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

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

Программа будет обновляться согласно фактически прочитанному материалу

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

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

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

Предварённая нормальная форма. Теорема о предварённой нормальной форме.
Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
Лемма о связке. Алгоритм унификации. Теорема об унификации.
Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
Метод резолюций: общая схема, применение.

Логические исчисления

Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
Натуральное исчисление предикатов. Корректность и полнота исчисления.
Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).

Аксиоматические теории

Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
Определения и выразимость в интерпретациях. Теорема о подстановке определения.
Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
Арифметика Пресбургера, её разрешимость и выразительность.

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

Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
Интуиционистская логика.
Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.

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

Текущая версия на 13:28, 23 апреля 2024

Содержание

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

Прошлогодние слайды

Семинары

Контрольные работы

Зачёт

Экзамен

Контрольная работа для экзамена

Премиальные задачи

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

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

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

Логические исчисления

Аксиоматические теории

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

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

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

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

Навигация

Персональные инструменты

Пространства имён

Варианты

Просмотры

Действия

Поиск

Навигация

Инструменты

@@ Строка 1: / Строка 1: @@
 [[Категория:Лекционные курсы кафедры МК]]
+Актуальность информации: весенний семестр 2023/2024 учебного года.
-Обязательный курс для студентов 318 группы 6 семестра обучения, ''а также для студентов 241 группы (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
+Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].
-'''Объявления'''
-''В этом разделе будут выкладываться объявления о текущих изменениях в курсе и на странице курса''
-* 2018.05.21 17:27 Обновлена статистика сданных задач на дополнительные бонусы
-* 2018.05.07 04:10 Выложены условия задач 8, 9, 10, 11 на дополнительные бонусы
-* 2018.05.07 04:10 Выложены слайды лекции 14-15
-* 2018.04.27 14:10 Выложены материалы семинара 6 (натуральное исчисление)
-* 2018.04.25 20:10 Лекция 13: исправлены ошибки в определении натурального исчисления
-* 2018.04.24 14:37 Сформулированы условия задач 4, 5 экзамена (они же - задачи второй контрольной работы)
-* 2018.03.02 14:05 Внесена небольшая правка в лекцию 3: добавлено (довольно естественное и само собой напрашивающееся, но по неведомым причинам забытое) обозначение для истинности в интерпретации
-* 2018.02.11 23:28 Страница подготовлена к началу весеннего семестра 2017/2018 учебного года
 = Слайды лекций =
-'''[[Media: Mathlog_318_lecture_1.pdf|Лекция 1]]''' (вводная). Что такое логика? Содержание лекций. История логики. Логические парадоксы.
+[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.
-'''[[Media: Mathlog_318_lecture_2.pdf|Лекция 2.]]''' Логика высказываний: синтаксис, семантика, выполнимость, общезначимость. Метод семантических таблиц в логике высказываний.
+[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.
-'''[[Media: Mathlog_318_lecture_3.pdf|Лекция 3.]]''' Логика предикатов: синтаксис (термы, формулы), семантика (интерпретации, отношение выполнимости), выполнимость, общезначимость, модели.
+[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.
-'''[[Media: Mathlog_318_lecture_4.pdf|Лекция 4.]]''' Логическое следствие. Проблема общезначимости формул. Подстановки. Метод семантических таблиц в логике предикатов. Корректность табличного вывода.
+[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).
-'''[[Media: Mathlog_318_lecture_5.pdf|Лекция 5.]]''' Полнота табличного вывода в логике предикатов. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча. Автоматизация доказательства теорем.
+[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.
-'''[[Media: Mathlog_318_lecture_6.pdf|Лекция 6.]]''' Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предварённая нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов. Задача унификации.
+[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).
-'''[[Media: Mathlog_318_lecture_7.pdf|Лекция 7.]]''' Алгоритм унификации.
+[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?
-'''[[Media: Mathlog_318_lecture_8.pdf|Лекция 8.]]''' Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема Эрбрана.
+[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.
-'''[[Media: Mathlog_318_lecture_9.pdf|Лекция 9.]]''' Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.
+[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).
-'''[[Media: LectLog20.pdf|Лекция 10 (Захаров В.А.).]]''' Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.
+[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.
-'''[[Media: Mathlog_318_lecture_11_12.pdf|Лекция 11-12.]]''' Аксиоматические теории. Основные свойства теорий. Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте. Определимость. Арифметика Пресбургера.
+[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.
-'''[[Media: Mathlog_318_lecture_13.pdf|Лекция 13.]]''' Исчисления предикатов. Исчисление Гильберта. Теорема Гёделя о полноте. Натуральное исчисление.
+[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.
-'''[[Media: Mathlog_318_lecture_14_15.pdf|Лекция 14-15.]]''' Модальные логики. Эпистемические логики. Темпоральные логики. Логика линейного времени (LTL). Логика деревьев вычислений (CTL). Верификация распределённых систем. Задача верификации для LTL. Табличный алгоритм верификации для LTL.
+[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.
-== Временный архив слайдов: 2016-2017 учебный год ==
+[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.
-'''[[Media: Mathlog_318_lecture_10.pdf|10]]''',
+[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.
-'''[[Media: Mathlog_318_lecture_11.pdf|11]]''',
-'''[[Media: Mathlog_318_lecture_12.pdf|12]]''',
-'''[[Media: Mathlog_318_lecture_14.pdf|14]]''',
-'''[[Media: Mathlog_318_lecture_16_17.pdf|16-17]]'''.
-= Семинары =
+[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).
-Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
+[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).
-Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
+[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.
-[[Media:Mllp_318_seminar_definability.pdf| Материалы семинара 5 (определимость).]]
+[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.
-[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 6 (натуральное исчисление).]]
+[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.
-= Контрольная работа =
+[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.
-Формат проведения и длительность контрольной работы: письменно, 95 минут.
+[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.
-В рамках контрольной работы требуется решить
+[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).
-* '''три задачи''':
+[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.
-** построить формулу логики предикатов, адекватно описывающую высказывание, представленное на естественном языке;
-** проверить общезначимость формулы логики предикатов, используя метод семантических таблиц
-*** (правила табличного вывода будут выданы вместе с заданием контрольной);
-** проверить общезначимость формулы логики предикатов, используя метод резолюций;
-* '''девять теоретических вопросов''', проверяющих знание материала, изложенного в лекциях 2-9.
-Контрольная работа оценивается по шкале '''от 0 до 15 баллов'''.
+[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.
-Итоговые баллы за работу - это сумма баллов за задачи и теоретические вопросы.
-Правильно решённая задача оценивается в '''2 балла'''.
+[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.
-Задача, решённая с ошибками, может быть оценена числом баллов от 0 до 2 в зависимости от качества и количества ошибок.
-Правильно решённый теоретический вопрос оценивается в '''1 балл'''.
+[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.
-В каждом теоретическом вопросе предлагается несколько вариантов ответа.
-Среди этих ответов может быть один, ни одного или несколько правильных.
-Для правильного решения теоретического вопроса следует отметить '''все''' правильные ответы и только их.
-Обоснование того, почему выбраны или не выбраны те или иные ответы, '''не требуется'''.
-'''Группа 241:''' баллы, набранные за контрольную работу, суммируются с другими баллами, требуемыми для зачёта.
+[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.
-'''Группа 318:''' по результатам контрольной работы определяется <span style="background:#DDFFDD">бонус</span> или <span style="background:#FFDDDD">штраф</span>, суммирующийся с баллами за экзаменационную работу:
+[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.
-* набрано от 13 до 15 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
-* набрано от 10 до 12 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
-* набрано от 7 до 9 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
-* набрано 6 баллов или меньше: штраф <span style="background:#FFDDDD">-3 балла</span>;
-* контрольная работа пропущена по неуважительной причине: штраф <span style="background:#FFDDDD">-3 балла</span>;
-* контрольная работа пропущена по уважительной причине: бонус <span style="background:#DDFFDD">+0 баллов</span>.
-= Экзамен =
+[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.
-Формат проведения и длительность экзамена: письменно, 120 минут.
+[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.
-Экзаменационная работа оценивается по шкале '''от 0 до 30 баллов''' (''промежуточные баллы'').
+[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).
-Итоговые баллы за экзаменационную работу - это сумма промежуточных баллов, бонусов и штрафов по итогам контрольной работы, а также других бонусов, если удалось их получить.
-В зависимости от полученных итоговых баллов за экзаменационную работу выставляется оценка за экзамен:
-* набрано хотя бы 25 баллов: '''отлично''';
-* набрано хотя бы 20, но менее 25 баллов: '''хорошо''';
-* набрано хотя бы 15, но менее 20 баллов: '''удовлетворительно''';
-* набрано менее 15 баллов: '''неудовлетворительно'''.
-Промежуточные баллы складываются из баллов, полученных за решение каждой задачи в работе.
+[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.
-Описание задач и оценки за их безошибочное решение:
-* '''Задача 1 (3 балла)''': предложить формулу логики предикатов, адекватно описывающую заданное утверждение, записанное на естественном языке.
-* '''Задача 2 (3 балла)''': проверить общезначимость формулы логики предикатов методом семантических таблиц.
-* '''Задача 3 (3 балла)''': проверить общезначимость формулы логики предикатов методом резолюций.
-* '''Задача 4 (3 балла)''': предложить аксиому, определяющую арифметическое понятие в заданной сигнатуре.
-* '''Задача 5 (3 балла)''': предложить доказательство формулы в натуральном исчислении предикатов.
-* '''Задачи 6-8 (2 балла за каждую)''' состоят из двух частей: а) сформулировать теорему или определение, рассказанные в лекциях; б) ответить на вопрос, так или иначе связанный с первой частью, '''без пояснений''' (как правило - "да" или "нет", либо привести какой-либо пример).
-* '''Задачи 9-11 (3 балла за каждую)''': из предложенных вариантов ответа на заданный вопрос выбрать правильные (один, несколько или ни одного), правильность каждого выбранного ответа обосновать ('''невыбранные ответы обосновывать не нужно''').
-= Зачёт =
+[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.
-В зачётную неделю будет проведена вторая контрольная работа. Эта работа будет содержать
+[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).
-* Две задачи, идентичные задачам 4, 5 экзамена, каждая из которых оценивается в 2 балла.
-* Пять теоретических вопросов по лекциям, проведённым после контрольной работы, аналогичные теоретическим вопросам первой контрольной работы. Каждый теоретический вопрос оценивается в 1 балл.
-Для получения зачёта необходимо набрать хотя бы две трети баллов суммарно за две контрольные работы и дополнительные бонусы, то есть '''не менее 16 баллов'''.
+[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.
-Не получившим зачёт по результатам второй контрольной работы будут предоставлены дополнительные попытки получения зачёта. На этих попытках:
+[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.
-* Сохраняются баллы за каждую задачу, суммарный балл за теоретические вопросы первой контрольной работы, суммарный балл за теоретические вопросы второй контрольной работы.
-* Предоставляется возможность поднять каждый из этих баллов, решив соответствующие части новых вариантов контрольных работ.
-= Дополнительные бонусы к экзамену и зачёту =
+[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.
-Общее условие сдачи задач на дополнительные бонусы:
+[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.
-* принцип сдачи задач:
-** идеи и выкладки, не требующие технических деталей, - устно;
-** если выкладки не воспроизводятся или не воспринимаются устно, то письменно;
-* при подготовке и сдаче можно пользоваться любыми материалами;
-* при сдаче проверяется понимание каждой детали решения задачи - следует быть к этому готовым;
-* задача считается решённой, если не осталось неотвеченных вопросов по обоснованию всех шагов решения задачи.
-'''Бонусы за решение задач сформулированы для одной учебной группы''' и получаются внутри одной группы независимо от другой (например, "''первый предоставивший решение''" трактуется как "''первый предоставивший решение из группы 318, а также первый предоставивший решение из группы 241''".
+[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.
-== Полнота табличного вывода в логике предикатов ==
+[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.
-=== Описание задачи ===
+[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.
-Адаптировать доказательство теоремы полноты табличного вывода в логике предикатов к более общему случаю:
+[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.
-* сигнатура алфавита состоит из
-** счётно-бесконечного числа констант,
-** счётно-бесконечного числа функциональных символов каждой местности,
-** счётно-бесконечного числа предикатных символов каждой местности;
-* формулы исходной таблицы могут содержать свободные переменные;
-* исходная таблица содержит не более чем счётно-бесконечное число формул, и при этом
-** формулы в левой части таблицы нумерованы натуральными числами, и существует алгоритм, по натуральному числу i выдающий i-ю формулу (то есть в доказательстве можно говорить "''возьмём i-ю формулу из левой части исходной таблицы''")
-** формулы в правой части таблицы нумерованы натуральными числами, и существует алгоритм, по натуральному числу i выдающий i-ю формулу (то есть в доказательстве можно говорить "''возьмём i-ю формулу из правой части исходной таблицы''")
-Бонусы за решение задачи:
+''Слайды будут появляться по мере чтения лекций.''
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
-* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
-=== Количество предоставленных решений ===
+== Прошлогодние слайды ==
-'''Группа 318:''' 0
+[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.
-'''Группа 241:''' 0
+[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.
-== Утверждения об отношении равносильности ==
+[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.
-=== Описание задачи ===
+[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.
-Доказать два утверждения об отношении равносильности, сформулированные в лекции 6 с доказательством, помеченным словом "Самостоятельно".
+[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.
-Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение задачи
+[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.
-=== Количество предоставленных решений ===
+[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.
-'''Группа 318:''' 1
+[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.
-'''Группа 241:''' 2 (''решения больше не принимаются'')
+[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.
-== Фундированность троек чисел ==
+[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.
-=== Описание задачи ===
+= Семинары =
-Доказать фундированность троек неотрицательных целых чисел относительно лексикографического порядка (лемма в лекции 7, сформулированная при доказательстве завершаемости алгоритма унификации, обоснование которой помечено словами "Попробуйте сами").
+''Материалы семинаров будут обновляться по мере проведения занятий''
-Бонусы за решение задачи:
+Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
-=== Количество предоставленных решений ===
+Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]
-'''Группа 318:''' 1
+[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]
-'''Группа 241:''' 2 (''решения больше не принимаются'')
+= Контрольные работы =
-== Полнота семантической резолюции ==
+Контрольные работы проводятся письменно, длительность каждой - 90 минут.
-=== Описание задачи ===
+В контрольных работах встретятся 4 типовые задачи со следующими темами:
+# Формализовать в логике предикатов предложение, записанное на естественном языке.
+# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
+# Обосновать общезначимость формулы логики предикатов методом резолюций.
+# Доказать формулу в натуральном исчислении предикатов.
-Доказать теорему полноты семантической резолюции (лекция 9).
+Оценка решений типовых задач:
+* Максимальная оценка - 4 балла.
+* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.
+* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.
+* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.
-Бонусы за решение задачи:
+Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
+Правильно решённый теоретический вопрос оценивается в 1 балл.
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
-* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
-=== Количество предоставленных решений ===
+'''Первая контрольная работа''' будет содержать
+* 3 типовые задачи по темам 1-3 и
+* 9 теоретических вопросов по прочитанным лекциям.
-'''Группа 318:''' 0
+'''Вторая контрольная работа''' будет содержать
+* 4 типовые задачи по всем темам и
+* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.
-'''Группа 241:''' 0
+'''Остальные контрольные работы''' будут содержать
+* 4 типовые задачи по всем темам и
+* 14 теоретических вопросов по всем лекциям.
-== Неизоморфные элементарно эквивалентные интерпретации ==
+= Зачёт =
-=== Описание задачи ===
+На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.
+При проставлении зачёта учитывается 6 технических оценок:
+* Четыре оценки за типовые задачи, по одной за каждую задачу.
+* Оценка за знание теории. Максимум - 14 баллов.
+* Оценка за решение премиальных задач.
-Привести пример двух неизоморфных элементарно эквивалентных интерпретаций, обосновать их неизоморфность и элементарную эквивалентность (см. '''лекцию 11-12''').
+Для получения зачёта требуется получить два результата:
+# Набрать хотя бы 11 баллов за типовые задачи.
+# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).
-Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> '''первому''' предоставившему решение.
+Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].
-=== Количество предоставленных решений ===
+Для решения каждой типовой задачи будет предложено несколько попыток.
+При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.
-'''Группа 318:''' 1 (''решения больше не принимаются'')
+При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных
+* суммарно за первые две контрольные работы и
+* за каждую из следующих контрольных работ.
-'''Группа 241:''' 1 (''решения больше не принимаются'')
+= Экзамен =
-== Теорема Гёделя о неполноте ==
+Формат проведения и длительность экзамена: письменно, 120 минут.
-=== Описание задачи ===
+Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.
+К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа для экзамена|контрольную работу]].
+Согласно набранной сумме технических баллов выставляется оценка:
+* хотя бы 30: '''отлично''';
+* хотя бы 23, но менее 30: '''хорошо''';
+* хотя бы 16, но менее 23: '''удовлетворительно''';
+* менее 16: '''неудовлетворительно'''.
-Доказать теорему Гёделя о неполноте ('''лекция 11-12'''): либо адаптировать доказательство в лекции к общему случаю и доказать лемму о диагонали и утверждение об арифметизуемости графика, либо предоставить своё доказательство.
+Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:
+* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:
+*# Формализовать в логике предикатов предложение, записанное на естественном языке.
+*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.
+*# Обосновать общезначимость формулы логики предикатов методом резолюций.
+*# Доказать формулу в натуральном исчислении предикатов.
+* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:
+*# Сформулировать утверждение, определение и т.п.
+*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
+*# Аргументировать (обосновать) ответ на вопрос.
+* Каждая из задач 8-10 оценивается в 4 балла и устроена так:
+** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.
+** Невыбранные ответы обосновывать не нужно.
-Бонусы за решение задачи:
+== Контрольная работа для экзамена ==
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+14 баллов</span>
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
-* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
-=== Количество предоставленных решений ===
+На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].
+Максимальная техническая оценка за эту работу - 21 балл.
+В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:
+* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;
+* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;
+* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;
+* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;
+* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;
+* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;
+* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;
+* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;
+* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.
-'''Группа 318:''' 0
+= Премиальные задачи =
-'''Группа 241:''' 0
+Общие условия сдачи решений премиальных задач:
+* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение.
+* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.
+* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.
+* Решение принимается, когда по нему не остаётся неотвеченных вопросов.
-== Теорема Гёделя о полноте ==
+'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.
+Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".
-=== Описание задачи ===
+Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.
-Доказать теорему Гёделя о полноте (см. '''лекцию 13''').
+= Программа курса =
-Бонусы за решение задачи:
+''Программа будет обновляться согласно фактически прочитанному материалу''
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+11 баллов</span>
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+8 баллов</span>
-* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+5 баллов</span>
-=== Количество предоставленных решений ===
-'''Группа 318:''' 1
-'''Группа 241:''' 1
-== Свойства шкал Крипке ==
-=== Описание задачи ===
-Доказать утверждения о рефлексивности, транзитивности и симметричности шкал Крипке, сформулированные в разделе "Эпистемические логики" '''лекции 14-15'''
-Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
-=== Количество предоставленных решений ===
-'''Группа 318:''' 1
-'''Группа 241:''' 2 (''решения больше не принимаются'')
-== Мудрецы ==
-=== Описание задачи ===
-Описать и содержательно пояснить законы рассуждений и ход рассуждений мудрецов в ''задаче о трёх мудрецах'' ('''лекция 14-15''') в терминах эпистемической логики.
-Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> первым '''двум''' предоставившим решение.
-=== Количество предоставленных решений ===
-'''Группа 318:''' 0
-'''Группа 241:''' 0
-== Законы темпоральных логик ==
-=== Описание задачи ===
-* Выбрать один темпоральный оператор логики линейного времени.
-** Если выбран оператор U, то также выбрать ''право'' или ''лево''.
-* Доказать или опровергнуть два закона дистрибутивности, сформулированные для выбранного оператора в '''лекции 14-15'''.
-** Если выбран оператор U, то это два закона дистрибутивности для ''правого'' или ''левого'' аргумента, в зависимости от сделанного выбора.
-Бонус за решение задачи: <span style="background:#DDFFDD">+1 балл</span> '''каждому''' предоставившему решение.
-Ограничение: доказательство или опровержение каждого закона дистрибутивности принимается только один раз.
-=== Операторы, для которых решения уже предоставлены ===
-'''Группа 318:''' -
-'''Группа 241:''' '''F'''
-== Табличный алгоритм верификации для LTL ==
-=== Описание задачи ===
-Ответить на существенную часть вопросов, сформулированных на последнем слайде '''лекции 14-15'''
-Бонус за решение задачи: '''обсуждается индивидуально'''.
-<!--
-== Теорема о разрешимости доопределения теории ==
-=== Описание задачи ===
-Завершить доказательство этой теоремы, предложенное в '''лекции 11''', или предложить своё доказательство
-Бонусы за решение задачи:
-* '''первый''' предоставивший решение: <span style="background:#DDFFDD">+3 балла</span>
-* '''второй''' предоставивший решение: <span style="background:#DDFFDD">+2 балла</span>
-* '''третий''' предоставивший решение: <span style="background:#DDFFDD">+1 балл</span>
-=== Количество предоставленных решений ===
-'''Группа 318:''' 0
-<s>'''Группа 241:''' 0</s> (''уже не актуально'')
-== Логика Хоара ==
-=== Описание задачи ===
-Доказать корректность одного из правил логики Хоара ('''лекция 16-17''').
-Бонус за решение задачи: <span style="background:#DDFFDD">+2 балла</span> за доказательство корректности каждого правила, кроме SKIP и AS. За задачу можно получить '''не более двух баллов'''. Доказательство корректности каждого правила принимается '''не более одного раза''' в группе.
-=== Количество предоставленных решений ===
-'''Группа 318:''' 0
-<s>'''Группа 241:''' INF, IF</s> (''уже не актуально'')
-== Законы темпоральной логики ==
-Все пункты задачи относятся к ''законам темпоральной логики'' ('''лекция 17''').
-* Выбрать одну пару двойственных левых частей для предполагаемых законов дистрибутивности (1+2, 3+4, 5+6, 7+8), сформулировать правые части, описывающие дистрибутивность операций в естественном понимании, и доказать и/или опровергнуть полученные законы.
-* Доказать закон неподвижной точки для одного из операторов U, R.
-* Сформулировать закон, ''не более тривиальный'', чем законы дистрибутивности для темпоральных операторов, и доказать его.
-Один сдающий может выбрать только '''один''' закон (или пару законов дистрибутивности), '''не выбранный ранее''' другими сдавшими. <span style="background:#DDFFDD">+1 балл</span> каждому решившему.
-''Статистика:''
-* решены законы дистрибутивности 1+2, 3+4
-* один решивший: законы из разных пар, поэтому пары остаются незанятыми
-== Model checking для LTL ==
-Доказать (додоказать) утверждение, представленное в слайдах '''лекции 18'''.
-* Утверждение на слайде 18 (106): однозначное задание согласованных предположений атомарными высказываниями и Next-time-формулами. <span style="background:#DDFFDD">+2 балла</span> каждому решившему.
-* Обоснование табличного метода model checking, достаточность, индуктивный переход, Until-формула: предложить обоснование для этого случая. <span style="background:#DDFFDD">+3 балла</span> каждому решившему.
--->
-= Программа курса =
 == Классические логики ==
 <ol>
-<li> Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.
+<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.
 <li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.
-<li> Проблема выполнимости булевых формул: приложения, основные решающие алгоритмы (алгоритм локального поиска, алгоритм DPLL).
 <li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).
-<li> Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
+<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.
 <li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.
-<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теорема корректности табличного вывода, теорема полноты табличного вывода.
+<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.
-<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.
+<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.
+<li> Машины Тьюринга. Теорема Чёрча.
 <li> Равносильные формулы. Теорема о равносильной замене.
 </ol>
@@ Строка 396: / Строка 254: @@
 <li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.
 <li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.
-<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.
+<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.
 <li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.
 <li> Лемма о связке. Алгоритм унификации. Теорема об унификации.
-<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема корректности резолютивного вывода.
+<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.
 <li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.
-<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема полноты резолютивного вывода.
+<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.
 <li> Метод резолюций: общая схема, применение.
-<li> Стратегии резолютивного вывода. Семантическая резолюция. Теорема полноты семантического резолютивного вывода. Входной резолютивный вывод.
-<li> Резолютивный вывод как средство вычисления. Хорновские дизъюнкты.
 </ol>
-== Аксиоматические теории первого порядка ==
+== Логические исчисления ==
-<ol start="21">
+<ol start="19">
-<li> Аксиомы, теоремы и теории. Выполнимость, противоречивость и общезначимость формул в теории. Проблема общезначимости формул логики предикатов в теории.
+<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.
-<li> Адекватность теорий интерпретации. Элементарная теория.
+<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.
-<li> Формальная арифметика. Арифметика Пеано. Теорема Гёделя о неполноте.
+<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.
-<li> Явные определения и определяющие аксиомы. Теорема о расширении теории. Теорема о подстановке определения.
+<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).
-<li> Арифметика Пресбургера: непротиворечивость, разрешимость, полнота, выразительные возможности.
+</ol>
-<li> Логические исчисления. Исчисления предикатов. Доказуемость (выводимость) формул.
-<li> Исчисление Гильберта. Теорема Гёделя о полноте. Натуральное исчисление Генцена.
+== Аксиоматические теории ==
+<ol start="23">
+<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.
+<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.
+<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.
+<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).
+<li> Арифметика Пресбургера, её разрешимость и выразительность.
 </ol>
@@ Строка 421: / Строка 283: @@
 <ol start="28">
 <li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.
-<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
+<li> Интуиционистская логика.
-<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
+<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.
-<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача верификации (проверки моделей; model checking) для логики линейного времени.
+<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.
-<li> Табличный алгоритм верификации для логики линейного времени. Упрощение формул. Замыкание Фишера-Ладнера. Согласованные предположения. Система Хинтикки. Сведение задачи верификации к графовым задачам.
 </ol>
-<!--
-== Аксиоматические теории первого порядка ==
-<ol start="21">
-<li> Аксиомы. Аксиоматическая теория первого порядка: определение; выполнимость, общезначимость и противоречивость формул в теории. Проблемы общезначимости и выполнимости формул логики предикатов в теории.
-<li> Основные свойства теорий: непротиворечивость, разрешимость, категоричность, полнота. Изоморфизм и элементарная эквивалентность интерпретаций. Связь изоморфизма интерпретаций, элементарной эквивалентности интерпретаций и полноты теорий.
-<li> Теория частичных порядков. Теория равенства: непротиворечивость, разрешимость, некатегоричность.
-<li> Исчисление предикатов: схемы аксиом, правило modus ponens, правило обобщения, логический вывод. Теорема Гёделя о полноте. Аксиоматические теории и исчисления.
-<li> Формальная арифметика. Теорема Гёделя о неполноте. Нумерации Гёделя. Арифметизуемые отношения.
-<li> Арифметика Пресбургера: непротиворечивость, разрешимость, полнота.
-<li> Бескванторные теории первого порядка. Теории с равенством. Преимущества проблемы выполнимости формул в теории перед проблемой общезначимости.
-<li> Теория равенства с неинтерпретируемыми функциями, разрешимость теории: сведение проблемы выполнимости в теории к проблеме выполнимости булевых формул.
-<li> Линейная арифметика. Виды линейных арифметик. NP-полнота линейной целочисленной арифметики.
-<li> Комбинация решающих алгоритмов для проблем выполнимости формул в теориях и в логике высказываний. Остовная проверка выполнимости формул в теориях. Интеграция алгоритмов проверки выполнимости формул в теориях в алгоритм DPLL.
-</ol>
-== Аксиоматическая теория множеств ==
-<ol start="31">
-<li> Наивная теория множеств. Сравнение мощностей множеств. Кардинальные числа в наивной теории множеств.
-<li> Теорема Кантора. Теорема об объединении множества, неограниченного по мощности. Теорема Кантора-Бернштейна.
-<li> Примеры кардинальных чисел. Конечность множеств мощности меньше счётной. Континуум-гипотеза в наивной теории множеств.
-<li> Выразительные возможности наивной теории множеств: натуральные числа, кортежи, функции. Парадоксы теории множеств.
-<li> Аксиоматические теории множеств. Теория Цермело-Френкеля: аксиомы и схемы аксиом, доказательство существования основных множеств наивной теории, исключение основных парадоксов теории множеств. Вопросы непротиворечивости теории Цермело-Френкеля.
-<li> Определимость функций и отношений в теории. Применение определений для расширения теории.
-<li> Аксиома выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и её отрицанием.
-<li> Ординальные числа. Основные свойства ординальных чисел. Арифметика ординальных чисел.
-<li> Теорема Цермело. Кардинальные числа в теории Цермело-Френкеля с аксиомой выбора.
-<li> Континуум-гипотеза в теории Цермело-Френкеля с аксиомой выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и континуум-гипотезой, её отрицанием.
-</ol>
-== Неклассические прикладные логики ==
-<ol start="41">
-<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.
-<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара.
-<li> Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.
-<li> Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача проверки выполнимости формул логики линейного времени на размеченных системах переходов.
-<li> Позитивная форма формул логики линейного времени. Замыкание Фишера-Ладнера. Согласованные множества формул. Системы Хинтикки. Табличный метод проверки выполнимости формул логики линейного времени на размеченных системах переходов.
-</ol>
--->
 = Рекомендованная литература =