Кафедра математической кибернетики - Вклад участника [ru]

Математическая логика и логическое программирование (3-й поток)

2026-04-27T15:32:53Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]
''Актуальность информации: осенний семестр 2025/2026 учебного года.''

Обязательный курс для студентов 3 потока 4 курса в 7 семестре.
Лектор: [[Подымов Владислав Васильевич|Подымов В.В.]]

= Материалы занятий =

== Лекции ==

[[Media: MLLP_VP_01.pdf|Блок 1]] (вступительный). Что такое логика. Несколько логических парадоксов. Чего ожидать в лекциях.

[[Media: MLLP_VP_02.pdf|Блок 2.]] Логика высказываний: синтаксис, семантика.

[[Media: MLLP_VP_03.pdf|Блок 3.]] Логика предикатов: синтаксис, семантика.

[[Media: MLLP_VP_04.pdf|Блок 4.]] Как формализовать предложение на языке логики предикатов (пример).

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

[[Media: MLLP_VP_06.pdf|Блок 6.]] Логика предикатов: выполнимые и общезначимые формулы, модели формул, логическое следствие, проблема общезначимости формул (постановка).

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

[[Media: MLLP_VP_08.pdf|Блок 8.]] Метод семантических таблиц: семантические таблицы.

[[Media: MLLP_VP_09.pdf|Блок 9.]] Подстановки (основные определения).

[[Media: MLLP_VP_10.pdf|Блок 10.]] Метод семантических таблиц: табличный вывод.

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

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

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

[[Media: MLLP_VP_14.pdf|Блок 14.]] Общая схема метода резолюций.

[[Media: MLLP_VP_15.pdf|Блок 15.]] Равносильность формул логики предикатов.

[[Media: MLLP_VP_16.pdf|Блок 16.]] Предварённая нормальная форма (ПНФ).

[[Media: MLLP_VP_17.pdf|Блок 17.]] Сколемовская стандартная форма (ССФ).

[[Media: MLLP_VP_18.pdf|Блок 18.]] Системы дизъюнктов.

[[Media: MLLP_VP_19.pdf|Блок 19.]] Композиция подстановок. Постановка задачи унификации.

[[Media: MLLP_VP_20.pdf|Блок 20.]] Алгоритм унификации атомарных формул.

[[Media: MLLP_VP_21.pdf|Блок 21.]] Монотонность и транзитивность логического следования.

[[Media: MLLP_VP_22.pdf|Блок 22.]] Резолютивный вывод. Корректность резолютивного вывода.

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

[[Media: MLLP_VP_24.pdf|Блок 24.]] Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: MLLP_VP_25.pdf|Блок 25.]] Теорема Эрбрана. Полнота резолютивного вывода.

[[Media: MLLP_VP_26.pdf|Блок 26.]] Стратегии резолютивного вывода.

[[Media: MLLP_VP_27.pdf|Блок 27.]] Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.

[[Media: MLLP_VP_28.pdf|Блок 28.]] Хорновские дизъюнкты.

[[Media: MLLP_VP_29.pdf|Блок 29.]] Вычислительные возможности метода резолюций.

[[Media: MLLP_VP_30.pdf|Блок 30.]] Хорновские логические программы: синтаксис, декларативная семантика, правильные ответы.

[[Media: MLLP_VP_31.pdf|Блок 31.]] Хорновские логические программы: списки.

[[Media: MLLP_VP_32.pdf|Блок 32.]] Хорновские логические программы: операционная семантика, SLD-резолютивные вычисления, SLD-вычислимые ответы.

[[Media: MLLP_VP_33.pdf|Блок 33.]] Хорновские логические программы: корректность операционной семантики.

[[Media: MLLP_VP_34.pdf|Блок 34.]] Хорновские логические программы: полнота операционной семантики.

[[Media: MLLP_VP_35.pdf|Блок 35.]] Хорновские логические программы: содержательное сравнение семантик.

[[Media: MLLP_VP_36.pdf|Блок 36.]] Хорновские логические программы: переключательная лемма, сильная полнота операционной семантики, стандартное правило выбора подцели.

[[Media: MLLP_VP_37.pdf|Блок 37.]] Хорновские логические программы: деревья SLD-резолютивных вычислений, стратегии вычисления и их полнота, стандартная стратегия вычисления.

[[Media: MLLP_VP_38.pdf|Блок 38.]] Машины Тьюринга.

[[Media: MLLP_VP_39.pdf|Блок 39.]] Моделирование машин Тьюринга хорновскими логическими программами.

[[Media: MLLP_VP_40.pdf|Блок 40.]] Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: MLLP_VP_41.pdf|Блок 41.]] Теорема Чёрча.

[[Media: MLLP_VP_42.pdf|Блок 42.]] Логические программы: встроенные предикаты и функции.

[[Media: MLLP_VP_43.pdf|Блок 43.]] Логические программы: стековые вычисления.

[[Media: MLLP_VP_44.pdf|Блок 44.]] Логические программы: управление вычислениями, оператор отсечения.

[[Media: MLLP_VP_45.pdf|Блок 45.]] Отрицание в логическом программировании. Допущение замкнутости мира.

[[Media: MLLP_VP_46.pdf|Блок 46.]] Логические программы: оператор отрицания, SLDNF-резолюция.

[[Media: MLLP_VP_47.pdf|Блок 47.]] Формальная верификация.

[[Media: MLLP_VP_48.pdf|Блок 48.]] Модельные императивные программы. Постановка задачи верификации программ.

[[Media: MLLP_VP_49.pdf|Блок 49.]] Логика Хоара. Автоматизация проверки правильности программ.

[[Media: MLLP_VP_50.pdf|Блок 50.]] Проверка правильности распределённых систем. Пара слов о методе проверки моделей.

[[Media: MLLP_VP_51.pdf|Блок 51.]] Модели Крипке.

[[Media: MLLP_VP_52.pdf|Блок 52.]] Темпоральные логики.

[[Media: MLLP_VP_53.pdf|Блок 53.]] Алгоритм проверки моделей для логики ветвящегося времени.

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

=== Прошлогодние ===

[[Media: MLLP_VP_r01.pdf|Вне программы 1]] Логические исчисления.

[[Media: MLLP_VP_r02.pdf|Вне программы 2.]] Натуральные исчисления.

[[Media: MLLP_VP_r03.pdf|Вне программы 3.]] Пара слов о лямбда-исчислении.

[[Media: MLLP_VP_r04.pdf|Вне программы 4.]] Изоморфизм Карри-Говарда.

[[Media: MLLP_VP_r05.pdf|Вне программы 5.]] Теорема Гёделя о полноте.

[[Media: MLLP_VP_r06.pdf|Вне программы 6.]] Формальная арифметика. Теорема Гёделя о неполноте.

[[Media: MLLP_VP_all.pdf|Все слайды лекций к экзамену в одном файле.]]

== Семинары ==

[[Media: MatLog_tasks.pdf| Задачи, обсуждающиеся на семинарах.]]

[[Медиа: MatLog_exer.pdf| Расширенный сборник задач для самостоятельного решения.]]

= Экзамен и контрольные работы =

На контрольных работах и на экзамене будут задачи следующих видов со следующими техническими баллами за полное правильное решение (в случае ошибок решению даётся меньший балл в зависимости от количества и качества ошибок):
* Типовые задачи (''4 балла''):
*# Формализовать в логике предикатов предложение, записанное на естественном языке (семинар 1).
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц (семинар 2). Правила табличного вывода будут выданы вместе с задачей.
*# Обосновать общезначимость формулы логики предикатов методом резолюций (семинары 3 и 4).
*# Построить дерево SLD-резолютивных вычислений заданной логической программы (семинары 5-7).
* Логическая программа (''8 баллов''). Написанию таких программ посвящены семинары 5-7.
* Задачи с формулировками (''3 балла''). Такая задача состоит из трёх частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
*# Аргументировать (обосновать) ответ на вопрос.
* Задача на понимание (''4 балла''). В этой задаче содержится один или несколько (не более трёх) близких (смежных, взаимосвязанных, схожих и т.п.) вопросов на углублённое понимание материалов курса (в том числе доказательств), на каждый из которых требуется ответить с обоснованием.

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

На лекциях будет проведено три контрольных работы, каждая - письменно на одну пару за вычетом 15 минут от начала пары на раскладку вариантов, рассадку студентов и отмашку о начале работы.

В первой контрольной работе содержатся типовые задачи 1 и 2, одна задача с формулировкой и две задачи на понимание.
Во второй контрольной работе содержатся типовая задача 3, две задачи с формулировкой и две задачи на понимание.
В третьей контрольной работе содержатся типовая задача 4, логическая программа, одна задача с формулировкой и одна задача на понимание.

== Экзамен ==

Экзамен проводится письменно, длительность - 150 минут.
В варианте экзамена содержатся три группы задач, в каждой группе - столько же и такого же вида, как на соответствующей [[#Контрольные работы|контрольной работе]].

По итогам экзамена определяются 4 технических оценки:
# Если на экзамене предпринята попытка решить задачи первой группы, то берётся сумма баллов за это решение, а иначе - сумма баллов за решение задач первой контрольной работы.
# То же относительно второй группы и второй контрольной работы.
# То же относительно третьей группы и третьей контрольной работы.
# Баллы за особые заслуги. Эти баллы оговариваются индивидуально с желающими их заслужить. К особым заслугам относится, в частности, решение задач, записанных в слайдах лекций оранжевым цветом в чёрной рамке.

Полученные 4 технических оценки складываются, и в зависимости от этой суммы определяется оценка за экзамен:

{| class="wikitable" style="margin:auto"
|-
! Сумма
! Оценка
|-
| Хотя бы 45
| Отлично
|-
| 34-44
| Хорошо
|-
| 23-33
| Удовлетворительно
|-
| 22 или меньше
| Неудовлетворительно
|}

Максимальные баллы за контрольные работы и за экзамен (без учёта особых заслуг):
* Первая контрольная: 19 баллов.
* Вторая контрольная: 18 баллов.
* Третья контрольная: 19 баллов.
* Экзамен (три контрольные вместе): 56 баллов.

= Программа =

''Программа может уточняться по мере проведения занятий.''

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

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

== Основы логического программирования ==
<ol start="22">
<li> Синтаксис хорновских логических программ: факты, правила, утверждения, программы, подцели, запросы.
<li> Декларативная семантика хорновских логических программ, правильный ответ на запрос.
<li> SLD-резолюция. SLD-резолютивное вычисление хорновской логической программы. Успешные, тупиковые и бесконечные вычисления программ. Операционная семантика программ, вычислимый ответ на запрос.
<li> Корректность и полнота операционной семантики хорновских логических программ относительно декларативной.
<li> Правило выбора подцели. Переключательная лемма, теорема о сильной полноте SLD-резолюции.
<li> Дерево SLD-резолютивных вычислений. Стратегия вычисления хорновских логических программ, примеры полных и неполных стратегий. Стандартная стратегия вычисления.
<li> Встроенные функции и предикаты в логических программах, их операционная семантика.
<li> Управление вычислениями логических программ. Оператор отсечения, его операционная семантика.
<li> Отрицание в логических программах. Гипотеза замкнутости мира. Оператор отрицания, его операционная семантика.
<li> Машины Тьюринга, моделирование их логическими программами. Теорема Чёрча.
</ol>

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

= Литература =

== Основная ==
# Клини С. Математическая логика. М.:Мир, 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 с.

= Материалы для подготовки к государственному экзамену =

''Материалы составлены для выпуска 2025. 2026 - без изменений.''

[[Media: MLLP_VP_gos3.pdf|Вопрос 3.]] Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций.

[[Media: MLLP_VP_gos4.pdf|Вопрос 4.]] Логическое программирование. Декаларативная семантика и операционная семантика, соотношение между ними. Стандартная стратегия выполнения логических программ.

Распределённые алгоритмы

2026-04-27T09:07:47Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

= Слайды =

[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.

[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.

[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.

[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.

[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.

[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.

[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.

[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.

[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.

[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.

[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.

[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.

[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.

[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.

[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.

[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.

[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DA_VP_S03.pdf| Семинар 3.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.

[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда - Уоршелла.

[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга

[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди - Мисры.

[[Media: DA_VP_S04.pdf| Семинар 4.]] Алгоритмы маршрутизации.

[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.

[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.

[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.

[[Media: DA_VP_S05.pdf| Семинар 5.]] Сложность по времени.

[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DA_VP_25.pdf| Блок 25.]] Кольцевой волновой алгоритм.

[[Media: DA_VP_26.pdf| Блок 26.]] Древесный волновой алгоритм.

[[Media: DA_VP_27.pdf| Блок 27.]] Алгоритм эха.

[[Media: DA_VP_S06.pdf| Семинар 6.]] Приложения волновых алгоритмов.

[[Media: DA_VP_28.pdf| Блок 28.]] Распределённые алгоритмы обхода.

[[Media: DA_VP_29.pdf| Блок 29.]] Алгоритм Тарри.

[[Media: DA_VP_30.pdf| Блок 30.]] Классический обход в глубину.

[[Media: DA_VP_31.pdf| Блок 31.]] Алгоритм Авербаха.

Семинар 7 (без слайдов). Распределённые алгоритмы обхода.

[[Media: DA_VP_32.pdf| Блок 32.]] Задача избрания лидера: основные определения и допущения, избрание лидера INF-алгоритмом.

[[Media: DA_VP_33.pdf| Блок 33.]] Задача избрания лидера: эффект угасания.

[[Media: DA_VP_34.pdf| Блок 34.]] Избрание лидера в дереве.

[[Media: DA_VP_35.pdf| Блок 35.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя - Робертса.

[[Media: DA_VP_36.pdf| Блок 36.]] Задача избрания лидера: нижние оценки.

Семинар 8 (без слайдов). Задача избрания лидера, простейшие алгоритмы и свойства.

[[Media: DA_VP_37.pdf| Блок 37.]] Избрание лидера и построение остовного дерева: алгоритм Галлагера - Хамблета - Спиры (GHS).

Семинар 9 (без слайдов). Алгоритм Галлагера - Хамблета - Спиры.

[[Media: DA_VP_38.pdf| Блок 38.]] Задача сохранения снимка сети.

[[Media: DA_VP_39.pdf| Блок 39.]] Алгоритм Чанди - Лэмпорта.

[[Media: DA_VP_40.pdf| Блок 40.]] Алгоритм Лаи - Янга.

Семинар 10 (без слайдов). Сохранение снимка сети.

[[Media: DA_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи приниятия решения.

[[Media: DA_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DA_VP_43.pdf| Блок 43.]] Паксос.

Семинар 11 (без слайдов). Задача консенсуса, Паксос.

[[Media: DA_VP_44.pdf| Блок 44.]] Задача выявления конца вычислений.

[[Media: DA_VP_45.pdf| Блок 45.]] Выявление конца вычислений: алгоритм Дейкстры - Шолтена.

[[Media: DA_VP_46.pdf| Блок 46.]] Выявление конца вычислений: алгоритм Шави - Франчеза.

[[Media: DA_VP_47.pdf| Блок 47.]] Выявление конца вычислений: алгоритм возвращения кредита.

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

= Экзамен =

Экзамен проводится письменно, длительность - 100 минут.
Вариант экзамена содержит 5 задач такого же характера, как задачи домашних заданий в семестре.

Каждая задача оценивается по шкале от 0 до 100 баллов.
В оценке задачи учитываются следующие характеристики решения:
* Полнота - учтены все детали, разобраны все случаи и т.п.
* Корректность - все утверждения в решении правильны.
* Строгость - решение написано грамотно, в том числе математически грамотно.
Средний балл по всем задачам преобразуется в оценку так: 80-100 - отлично, 60-79 - хорошо, 40-59 - удовлетворительно, менее 40 - неудовлетворительно.

Можно пользоваться лекциями, книгами, конспектами.
Нельзя пользоваться никакими иными неодобренными источниками.
Имейте в виду, что времени на решение задач даётся не очень много, поэтому использование материалов на экзамене не заменяет подготовку к нему.

= Домашние задания =

Желающие облегчить экзамен (в том числе избежать его - получить автомат) могут выполнять домашние задания во время семестра.

Каждому семинару отвечает своё домашнее задание.
Оно оценивается по шкале от 0 до 100 баллов.
В домашнем задании может быть несколько задач, баллы распределяются пропорционально трудности задач.
В оценке каждой задачи учитываются те же характеристики, что и в оценке задач экзамена.
Кроме того, выдаётся штраф за слишком долгое решение:
* Решение сдано до конца воскресенья, следующего за семинаром - штрафа нет.
* Каждая дополнительная неделя даёт штраф -6 баллов.
* После окончания семестра домашние задания не принимаются, за исключением явно оговорённых случаев.

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

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Файл:Mathlog VP 37.pdf

2026-04-07T06:46:06Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 37.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 37

Математическая логика (318, 319/2, 241, 242)

2026-04-01T15:11:41Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

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

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

[[Media: Mathlog_VP_02.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.

[[Media: Mathlog_VP_03.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.

[[Media: Mathlog_VP_04.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).

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

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

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

[[Media: Mathlog_VP_08.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.

[[Media: Mathlog_VP_09.pdf|Блок 9]]. Подстановки (основные определения).

[[Media: Mathlog_VP_10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.

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

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

[[Media: Mathlog_VP_13.pdf|Блок 13]]. Теорема компактности Мальцева. Автоматизация доказательства теорем.

[[Media: Mathlog_VP_14.pdf|Блок 14]]. Общая схема метода резолюций.

[[Media: Mathlog_VP_15.pdf|Блок 15]]. Равносильность формул.

[[Media: Mathlog_VP_16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).

[[Media: Mathlog_VP_17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).

[[Media: Mathlog_VP_18.pdf|Блок 18]]. Системы дизъюнктов.

[[Media: Mathlog_VP_19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.

[[Media: Mathlog_VP_20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.

[[Media: Mathlog_VP_21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.

[[Media: Mathlog_VP_22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.

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

[[Media: Mathlog_VP_24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: Mathlog_VP_25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.

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

[[Media: Mathlog_VP_27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.

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

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

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

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

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

[[Media: Mathlog_VP_33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.

[[Media: Mathlog_VP_34.pdf|Блок 34]]. Даша, Саша, Паша, пиво и натуральное исчисление предикатов.

[[Media: Mathlog_VP_35.pdf|Блок 35]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: Mathlog_VP_36.pdf|Блок 36]]. Машины Тьюринга (МТ).

[[Media: Mathlog_VP_37.pdf|Блок 37]]. Теорема Чёрча.

[[Media: Mathlog_VP_38.pdf|Блок 38]]. Модальные логики.

[[Media: Mathlog_VP_39.pdf|Блок 39]]. Эпистемические логики.

[[Media: Mathlog_VP_40.pdf|Блок 40]]. Темпоральные логики.

[[Media: Mathlog_VP_41.pdf|Блок 41]]. Интуиционистская логика.

[[Media: Mathlog_VP_42.pdf|Блок 42]]. Формальная верификация.

[[Media: Mathlog_VP_43.pdf|Блок 43]]. Модельные императивные программы. Постановка задачи верификации программ.

[[Media: Mathlog_VP_44.pdf|Блок 44]]. Логика Хоара. Автоматизация проверки правильности программ.

[[Media: Mathlog_VP_45.pdf|Блок 45]]. Проверка правильности распределённых систем. Пара слов о методе проверки моделей.

[[Media: Mathlog_VP_46.pdf|Блок 46]]. Размеченные системы переходов.

[[Media: Mathlog_VP_47.pdf|Блок 47]]. Спецификация систем при помощи темпоральных логик.

[[Media: Mathlog_VP_48.pdf|Блок 48]]. Алгоритм проверки моделей для логики ветвящегося времени.

'''Вне программы.'''

[[Media: Mathlog_VP_X01.pdf|Блок В01.]] Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

[[Media: Mathlog_VP_X02.pdf|Блок В02.]] Основные свойства аксиоматических теорий.

[[Media: Mathlog_VP_X03.pdf|Блок В03.]] Арифметические интерпретации и теории.

[[Media: Mathlog_VP_X04.pdf|Блок В04.]] Определения и выразимость.

[[Media: Mathlog_VP_X05.pdf|Блок В05.]] Формальная арифметика. Теорема Гёделя о неполноте.

[[Media: Mathlog_VP_X06.pdf|Блок В06.]] Арифметика Пресбургера.

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

= Семинары =

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

Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]

[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]

= Контрольные работы, зачёт и экзамен =

На контрольных работах, зачёте и экзамене будут задачи следующих видов со следующими техническими баллами за полное правильное решение (в случае ошибок решению даётся меньший балл в зависимости от количества и качества ошибок):
* Типовые задачи (''4 балла''):
*# Формализовать в логике предикатов предложение, записанное на естественном языке (семинар 1).
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц (семинар 2). Правила табличного вывода будут выданы вместе с задачей.
*# Обосновать общезначимость формулы логики предикатов методом резолюций (семинары 3 и 4).
*# Доказать формулу в натуральном исчислении предикатов (семинары 5 и 6).
* Задачи с формулировками (''3 балла''). Такая задача состоит из трёх частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
*# Аргументировать (обосновать) ответ на вопрос.
* Задачи на понимание (''4 балла''). В этой задаче содержится один или несколько (не более трёх) близких (смежных, взаимосвязанных, схожих и т.п.) вопросов на углублённое понимание материалов курса (в том числе доказательств), на каждый из которых требуется ответить с обоснованием.

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

На лекциях будет проведено три контрольных работы, каждая - письменно, 80 минут (остальное время занятия резервируется для раскладки вариантов, рассадки студентов, отмашки о начале работы, сбора работ и прочего).
Использование любых источников, кроме своей головы, запрещено.

В первой контрольной работе содержатся типовые задачи 1 и 2, одна задача с формулировкой и две задачи на понимание.
Во второй контрольной работе содержатся типовая задача 3, две задачи с формулировкой и две задачи на понимание.
В третьей контрольной работе содержатся типовая задача 4, две задачи с формулировкой и две задачи на понимание.

Максимальная оценка за первую контрольную работу - 19 баллов, за вторую и третью - по 18 баллов, суммарная максимальная оценка за все контрольные работы - 55 баллов.

== Зачёт ==

Чтобы получить зачёт, требуется получить два результата:
# Набрать хотя бы 11 баллов за типовые задачи.
# Набрать хотя бы 24 балла за всё, что есть в курсе.

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

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

== Экзамен ==

Экзамен проводится письменно, длится 150 минут и состоит в переписывании любого количества контрольных работ.
До экзамена каждый сдающий может изъявить желание сохранить оценки тех или иных контрольных работ.
На самом экзамене обнуляются и пишутся заново все контрольные работы, по которым такое желание не было изъявлено.

Суммарный балл за все контрольные работы преобразуется в оценку следующим образом:

{| class="wikitable" style="margin:auto"
|-
! Сумма
! Оценка
|-
| Хотя бы 44
| Отлично
|-
| 33-43
| Хорошо
|-
| 22-32
| Удовлетворительно
|-
| 21 или меньше
| Неудовлетворительно
|}

= Бонусные баллы =

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

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

Премиальные задачи объявляются по мере проведения занятий.
Для каждой задачи определяются премия и номер контрольной работы.

Премии распределяются в каждой группе независимо от других.
Например, "первый" означает "первый в 318, первый в 319/2, первый в 241 и первый в 242".

Премия добавляется к баллам за соответствующую контрольную работу, но не более максимальной оценки за контрольную работу.
Сверх максимальной оценки премия обменивается на баллы по курсу 4:1 - каждые 4 объявленных премиальных балла преобразуются в 1 фактически полученный.
Задачи, не соответствующие ни одной контрольной работе, всегда принимаются по полному курсу (1:1).

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

== Особые заслуги ==

Особые заслуги обсуждаются индивидуально - это дела, полезные для курса и демонстрирующие освоение материалов курса.

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

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

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

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

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

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

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

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

== Основная литература ==
# Клини С. Математическая логика. М.:Мир, 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 с.

Математическая логика (318, 319/2, 241, 242)

2026-03-31T17:38:45Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

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

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

[[Media: Mathlog_VP_02.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.

[[Media: Mathlog_VP_03.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.

[[Media: Mathlog_VP_04.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).

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

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

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

[[Media: Mathlog_VP_08.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.

[[Media: Mathlog_VP_09.pdf|Блок 9]]. Подстановки (основные определения).

[[Media: Mathlog_VP_10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.

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

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

[[Media: Mathlog_VP_13.pdf|Блок 13]]. Теорема компактности Мальцева. Автоматизация доказательства теорем.

[[Media: Mathlog_VP_14.pdf|Блок 14]]. Общая схема метода резолюций.

[[Media: Mathlog_VP_15.pdf|Блок 15]]. Равносильность формул.

[[Media: Mathlog_VP_16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).

[[Media: Mathlog_VP_17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).

[[Media: Mathlog_VP_18.pdf|Блок 18]]. Системы дизъюнктов.

[[Media: Mathlog_VP_19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.

[[Media: Mathlog_VP_20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.

[[Media: Mathlog_VP_21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.

[[Media: Mathlog_VP_22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.

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

[[Media: Mathlog_VP_24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: Mathlog_VP_25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.

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

[[Media: Mathlog_VP_27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.

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

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

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

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

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

[[Media: Mathlog_VP_33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.

[[Media: Mathlog_VP_34.pdf|Блок 34]]. Даша, Саша, Паша, пиво и натуральное исчисление предикатов.

[[Media: Mathlog_VP_35.pdf|Блок 35]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: Mathlog_VP_36.pdf|Блок 36]]. Машины Тьюринга (МТ).

[[Media: Mathlog_VP_37.pdf|Блок 37]]. Теорема Чёрча.

[[Media: Mathlog_VP_38.pdf|Блок 38]]. Модальные логики.

[[Media: Mathlog_VP_39.pdf|Блок 39]]. Эпистемические логики.

[[Media: Mathlog_VP_40.pdf|Блок 40]]. Темпоральные логики.

[[Media: Mathlog_VP_41.pdf|Блок 41]]. Интуиционистская логика.

[[Media: Mathlog_VP_42.pdf|Блок 42]]. Формальная верификация.

[[Media: Mathlog_VP_43.pdf|Блок 43]]. Модельные императивные программы. Постановка задачи верификации программ.

[[Media: Mathlog_VP_44.pdf|Блок 44]]. Логика Хоара. Автоматизация проверки правильности программ.

[[Media: Mathlog_VP_45.pdf|Блок 45]]. Проверка правильности распределённых систем. Пара слов о методе проверки моделей.

[[Media: Mathlog_VP_46.pdf|Блок 46]]. Размеченные системы переходов.

[[Media: Mathlog_VP_47.pdf|Блок 47]]. Спецификация систем при помощи темпоральных логик.

[[Media: Mathlog_VP_48.pdf|Блок 48]]. Алгоритм проверки моделей для логики ветвящегося времени.

'''Вне программы.'''

[[Media: Mathlog_VP_X01.pdf|Блок В01.]] Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.

[[Media: Mathlog_VP_X02.pdf|Блок В02.]] Основные свойства аксиоматических теорий.

[[Media: Mathlog_VP_X03.pdf|Блок В03.]] Арифметические интерпретации и теории.

[[Media: Mathlog_VP_X04.pdf|Блок В04.]] Определения и выразимость.

[[Media: Mathlog_VP_X05.pdf|Блок В05.]] Формальная арифметика. Теорема Гёделя о неполноте.

[[Media: Mathlog_VP_X06.pdf|Блок В06.]] Арифметика Пресбургера.

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

= Семинары =

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

Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]

[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]

= Контрольные работы, зачёт и экзамен =

На контрольных работах, зачёте и экзамене будут задачи следующих видов со следующими техническими баллами за полное правильное решение (в случае ошибок решению даётся меньший балл в зависимости от количества и качества ошибок):
* Типовые задачи (''4 балла''):
*# Формализовать в логике предикатов предложение, записанное на естественном языке (семинар 1).
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц (семинар 2). Правила табличного вывода будут выданы вместе с задачей.
*# Обосновать общезначимость формулы логики предикатов методом резолюций (семинары 3 и 4).
*# Доказать формулу в натуральном исчислении предикатов (семинары 5 и 6).
* Задачи с формулировками (''3 балла''). Такая задача состоит из трёх частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
*# Аргументировать (обосновать) ответ на вопрос.
* Задачи на понимание (''4 балла''). В этой задаче содержится один или несколько (не более трёх) близких (смежных, взаимосвязанных, схожих и т.п.) вопросов на углублённое понимание материалов курса (в том числе доказательств), на каждый из которых требуется ответить с обоснованием.

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

На лекциях будет проведено три контрольных работы, каждая - письменно, 80 минут (остальное время занятия резервируется для раскладки вариантов, рассадки студентов, отмашки о начале работы, сбора работ и прочего).
Использование любых источников, кроме своей головы, запрещено.

В первой контрольной работе содержатся типовые задачи 1 и 2, одна задача с формулировкой и две задачи на понимание.
Во второй контрольной работе содержатся типовая задача 3, две задачи с формулировкой и две задачи на понимание.
В третьей контрольной работе содержатся типовая задача 4, две задачи с формулировкой и две задачи на понимание.

Максимальная оценка за первую контрольную работу - 19 баллов, за вторую и третью - по 18 баллов, суммарная максимальная оценка за все контрольные работы - 55 баллов.

== Зачёт ==

Чтобы получить зачёт, требуется получить два результата:
# Набрать хотя бы 11 баллов за типовые задачи.
# Набрать хотя бы 24 балла за всё, что есть в курсе.

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

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

== Экзамен ==

Экзамен проводится письменно, длится 150 минут и состоит в переписывании любого количества контрольных работ.
До экзамена каждый сдающий может изъявить желание сохранить оценки тех или иных контрольных работ.
На самом экзамене обнуляются и пишутся заново все контрольные работы, по которым такое желание не было изъявлено.

Суммарный балл за все контрольные работы преобразуется в оценку следующим образом:

{| class="wikitable" style="margin:auto"
|-
! Сумма
! Оценка
|-
| Хотя бы 44
| Отлично
|-
| 33-43
| Хорошо
|-
| 22-32
| Удовлетворительно
|-
| 21 или меньше
| Неудовлетворительно
|}

= Бонусные баллы =

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

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

Премиальные задачи объявляются по мере проведения занятий.
Для каждой задачи определяются премия и номер контрольной работы.

Премии распределяются в каждой группе независимо от других.
Например, "первый" означает "первый в 318, первый в 319/2, первый в 241 и первый в 242".

Премия добавляется к баллам за соответствующую контрольную работу, но не более максимальной оценки за контрольную работу.
Сверх максимальной оценки премия обменивается на баллы по курсу 4:1 - каждые 4 объявленных премиальных балла преобразуются в 1 фактически полученный.

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

== Особые заслуги ==

Особые заслуги обсуждаются индивидуально - это дела, полезные для курса и демонстрирующие освоение материалов курса.

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

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

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

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

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

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

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

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

== Основная литература ==
# Клини С. Математическая логика. М.:Мир, 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 с.

Файл:Mathlog VP X06.pdf

2026-03-31T17:35:11Z

PodymovVV: матлог 318 319 241 242 вне программы 6

матлог 318 319 241 242 вне программы 6

Файл:Mathlog VP X05.pdf

2026-03-31T17:34:53Z

PodymovVV: матлог 318 319 241 242 вне программы 5

матлог 318 319 241 242 вне программы 5

Файл:Mathlog VP X04.pdf

2026-03-31T17:34:31Z

PodymovVV: матлог 318 319 241 242 вне программы 4

матлог 318 319 241 242 вне программы 4

Файл:Mathlog VP X03.pdf

2026-03-31T17:34:11Z

PodymovVV: матлогика 318 319 241 242 вне программы 3

матлогика 318 319 241 242 вне программы 3

Файл:Mathlog VP X02.pdf

2026-03-31T17:33:50Z

PodymovVV: матлогика 318 319 241 242 вне программы 2

матлогика 318 319 241 242 вне программы 2

Файл:Mathlog VP X01.pdf

2026-03-31T17:33:26Z

PodymovVV: матлогика 318-319-241-242, вне программы

матлогика 318-319-241-242, вне программы

Математическая логика (318, 319/2, 241, 242)

2026-03-25T20:59:03Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

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

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

[[Media: Mathlog_VP_02.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.

[[Media: Mathlog_VP_03.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.

[[Media: Mathlog_VP_04.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).

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

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

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

[[Media: Mathlog_VP_08.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.

[[Media: Mathlog_VP_09.pdf|Блок 9]]. Подстановки (основные определения).

[[Media: Mathlog_VP_10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.

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

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

[[Media: Mathlog_VP_13.pdf|Блок 13]]. Теорема компактности Мальцева. Автоматизация доказательства теорем.

[[Media: Mathlog_VP_14.pdf|Блок 14]]. Общая схема метода резолюций.

[[Media: Mathlog_VP_15.pdf|Блок 15]]. Равносильность формул.

[[Media: Mathlog_VP_16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).

[[Media: Mathlog_VP_17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).

[[Media: Mathlog_VP_18.pdf|Блок 18]]. Системы дизъюнктов.

[[Media: Mathlog_VP_19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.

[[Media: Mathlog_VP_20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.

[[Media: Mathlog_VP_21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.

[[Media: Mathlog_VP_22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.

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

[[Media: Mathlog_VP_24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.

[[Media: Mathlog_VP_25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.

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

[[Media: Mathlog_VP_27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.

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

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

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

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

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

[[Media: Mathlog_VP_33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.

[[Media: Mathlog_VP_34.pdf|Блок 34]]. Даша, Саша, Паша, пиво и натуральное исчисление предикатов.

[[Media: Mathlog_VP_35.pdf|Блок 35]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.

[[Media: Mathlog_VP_36.pdf|Блок 36]]. Машины Тьюринга (МТ).

[[Media: Mathlog_VP_37.pdf|Блок 37]]. Теорема Чёрча.

[[Media: Mathlog_VP_38.pdf|Блок 38]]. Модальные логики.

[[Media: Mathlog_VP_39.pdf|Блок 39]]. Эпистемические логики.

[[Media: Mathlog_VP_40.pdf|Блок 40]]. Темпоральные логики.

[[Media: Mathlog_VP_41.pdf|Блок 41]]. Интуиционистская логика.

[[Media: Mathlog_VP_42.pdf|Блок 42]]. Формальная верификация.

[[Media: Mathlog_VP_43.pdf|Блок 43]]. Модельные императивные программы. Постановка задачи верификации программ.

[[Media: Mathlog_VP_44.pdf|Блок 44]]. Логика Хоара. Автоматизация проверки правильности программ.

[[Media: Mathlog_VP_45.pdf|Блок 45]]. Проверка правильности распределённых систем. Пара слов о методе проверки моделей.

[[Media: Mathlog_VP_46.pdf|Блок 46]]. Размеченные системы переходов.

[[Media: Mathlog_VP_47.pdf|Блок 47]]. Спецификация систем при помощи темпоральных логик.

[[Media: Mathlog_VP_48.pdf|Блок 48]]. Алгоритм проверки моделей для логики ветвящегося времени.

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

= Семинары =

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

Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]

Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]

[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]

= Контрольные работы, зачёт и экзамен =

На контрольных работах, зачёте и экзамене будут задачи следующих видов со следующими техническими баллами за полное правильное решение (в случае ошибок решению даётся меньший балл в зависимости от количества и качества ошибок):
* Типовые задачи (''4 балла''):
*# Формализовать в логике предикатов предложение, записанное на естественном языке (семинар 1).
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц (семинар 2). Правила табличного вывода будут выданы вместе с задачей.
*# Обосновать общезначимость формулы логики предикатов методом резолюций (семинары 3 и 4).
*# Доказать формулу в натуральном исчислении предикатов (семинары 5 и 6).
* Задачи с формулировками (''3 балла''). Такая задача состоит из трёх частей:
*# Сформулировать утверждение, определение и т.п.
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.
*# Аргументировать (обосновать) ответ на вопрос.
* Задачи на понимание (''4 балла''). В этой задаче содержится один или несколько (не более трёх) близких (смежных, взаимосвязанных, схожих и т.п.) вопросов на углублённое понимание материалов курса (в том числе доказательств), на каждый из которых требуется ответить с обоснованием.

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

На лекциях будет проведено три контрольных работы, каждая - письменно, 80 минут (остальное время занятия резервируется для раскладки вариантов, рассадки студентов, отмашки о начале работы, сбора работ и прочего).
Использование любых источников, кроме своей головы, запрещено.

В первой контрольной работе содержатся типовые задачи 1 и 2, одна задача с формулировкой и две задачи на понимание.
Во второй контрольной работе содержатся типовая задача 3, две задачи с формулировкой и две задачи на понимание.
В третьей контрольной работе содержатся типовая задача 4, две задачи с формулировкой и две задачи на понимание.

Максимальная оценка за первую контрольную работу - 19 баллов, за вторую и третью - по 18 баллов, суммарная максимальная оценка за все контрольные работы - 55 баллов.

== Зачёт ==

Чтобы получить зачёт, требуется получить два результата:
# Набрать хотя бы 11 баллов за типовые задачи.
# Набрать хотя бы 24 балла за всё, что есть в курсе.

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

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

== Экзамен ==

Экзамен проводится письменно, длится 150 минут и состоит в переписывании любого количества контрольных работ.
До экзамена каждый сдающий может изъявить желание сохранить оценки тех или иных контрольных работ.
На самом экзамене обнуляются и пишутся заново все контрольные работы, по которым такое желание не было изъявлено.

Суммарный балл за все контрольные работы преобразуется в оценку следующим образом:

{| class="wikitable" style="margin:auto"
|-
! Сумма
! Оценка
|-
| Хотя бы 44
| Отлично
|-
| 33-43
| Хорошо
|-
| 22-32
| Удовлетворительно
|-
| 21 или меньше
| Неудовлетворительно
|}

= Бонусные баллы =

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

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

Премиальные задачи объявляются по мере проведения занятий.
Для каждой задачи определяются премия и номер контрольной работы.

Премии распределяются в каждой группе независимо от других.
Например, "первый" означает "первый в 318, первый в 319/2, первый в 241 и первый в 242".

Премия добавляется к баллам за соответствующую контрольную работу, но не более максимальной оценки за контрольную работу.
Сверх максимальной оценки премия обменивается на баллы по курсу 4:1 - каждые 4 объявленных премиальных балла преобразуются в 1 фактически полученный.

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

== Особые заслуги ==

Особые заслуги обсуждаются индивидуально - это дела, полезные для курса и демонстрирующие освоение материалов курса.

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

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

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

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

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

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

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

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

== Основная литература ==
# Клини С. Математическая логика. М.:Мир, 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 с.

Файл:Mathlog VP 48.pdf

2026-03-25T20:57:27Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 48.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 48

Файл:Mathlog VP 47.pdf

2026-03-25T20:57:07Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 47.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 47

Файл:Mathlog VP 46.pdf

2026-03-25T20:56:45Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 46.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 46

Файл:Mathlog VP 45.pdf

2026-03-25T20:56:27Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 45.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 45

Файл:Mathlog VP 44.pdf

2026-03-25T20:56:05Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 44.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 44

Файл:Mathlog VP 43.pdf

2026-03-25T20:55:35Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 43.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 43

Файл:Mathlog VP 42.pdf

2026-03-25T20:55:15Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 42.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 42

Файл:Mathlog VP 41.pdf

2026-03-25T20:54:32Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 41.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 41

Файл:Mathlog VP 40.pdf

2026-03-25T20:54:13Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 40.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 40

Файл:Mathlog VP 39.pdf

2026-03-25T20:53:44Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 39.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 39

Файл:Mathlog VP 38.pdf

2026-03-25T20:53:21Z

PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog VP 38.pdf»

Матлогика 318+319/2+241+242. Лекции, блок 38

Распределённые алгоритмы

2026-03-24T12:13:16Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

= Слайды =

[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.

[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.

[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.

[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.

[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.

[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.

[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.

[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.

[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.

[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.

[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.

[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.

[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.

[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.

[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.

[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.

[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DA_VP_S03.pdf| Семинар 3.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.

[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда - Уоршелла.

[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга

[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди - Мисры.

[[Media: DA_VP_S04.pdf| Семинар 4.]] Алгоритмы маршрутизации.

[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.

[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.

[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.

[[Media: DA_VP_S05.pdf| Семинар 5.]] Сложность по времени.

[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DA_VP_25.pdf| Блок 25.]] Кольцевой волновой алгоритм.

[[Media: DA_VP_26.pdf| Блок 26.]] Древесный волновой алгоритм.

[[Media: DA_VP_27.pdf| Блок 27.]] Алгоритм эха.

[[Media: DA_VP_S06.pdf| Семинар 6.]] Приложения волновых алгоритмов.

[[Media: DA_VP_28.pdf| Блок 28.]] Распределённые алгоритмы обхода.

[[Media: DA_VP_29.pdf| Блок 29.]] Алгоритм Тарри.

[[Media: DA_VP_30.pdf| Блок 30.]] Классический обход в глубину.

[[Media: DA_VP_31.pdf| Блок 31.]] Алгоритм Авербаха.

Семинар 7 (без слайдов). Распределённые алгоритмы обхода.

[[Media: DA_VP_32.pdf| Блок 32.]] Задача избрания лидера: основные определения и допущения, избрание лидера INF-алгоритмом.

[[Media: DA_VP_33.pdf| Блок 33.]] Задача избрания лидера: эффект угасания.

[[Media: DA_VP_34.pdf| Блок 34.]] Избрание лидера в дереве.

[[Media: DA_VP_35.pdf| Блок 35.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.

[[Media: DA_VP_36.pdf| Блок 36.]] Задача избрания лидера: нижние оценки.

Семинар 8 (без слайдов). Задача избрания лидера, простейшие алгоритмы и свойства.

[[Media: DA_VP_37.pdf| Блок 37.]] Избрание лидера и построение остовного дерева: алгоритм Галлагера - Хамблета - Спиры (GHS).

Семинар 9 (без слайдов). Алгоритм Галлагера - Хамблета - Спиры.

[[Media: DA_VP_38.pdf| Блок 38.]] Задача сохранения снимка сети.

[[Media: DA_VP_39.pdf| Блок 39.]] Алгоритм Чанди - Лэмпорта.

[[Media: DA_VP_40.pdf| Блок 40.]] Алгоритм Лаи - Янга.

Семинар 10 (без слайдов). Сохранение снимка сети.

[[Media: DA_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи приниятия решения.

[[Media: DA_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DA_VP_43.pdf| Блок 43.]] Паксос.

Семинар 11 (без слайдов). Задача консенсуса, Паксос.

[[Media: DA_VP_44.pdf| Блок 44.]] Задача выявления конца вычислений.

[[Media: DA_VP_45.pdf| Блок 45.]] Выявление конца вычислений: алгоритм Дейкстры - Шолтена.

[[Media: DA_VP_46.pdf| Блок 46.]] Выявление конца вычислений: алгоритм Шави - Франчеза.

[[Media: DA_VP_47.pdf| Блок 47.]] Выявление конца вычислений: алгоритм возвращения кредита.

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

= Экзамен =

Экзамен проводится письменно, длительность - 100 минут.
Вариант экзамена содержит 5 задач такого же характера, как задачи домашних заданий в семестре.

Каждая задача оценивается по шкале от 0 до 100 баллов.
В оценке задачи учитываются следующие характеристики решения:
* Полнота - учтены все детали, разобраны все случаи и т.п.
* Корректность - все утверждения в решении правильны.
* Строгость - решение написано грамотно, в том числе математически грамотно.
Средний балл по всем задачам преобразуется в оценку так: 80-100 - отлично, 60-79 - хорошо, 40-59 - удовлетворительно, менее 40 - неудовлетворительно.

Можно пользоваться лекциями, книгами, конспектами.
Нельзя пользоваться никакими иными неодобренными источниками.
Имейте в виду, что времени на решение задач даётся не очень много, поэтому использование материалов на экзамене не заменяет подготовку к нему.

= Домашние задания =

Желающие облегчить экзамен (в том числе избежать его - получить автомат) могут выполнять домашние задания во время семестра.

Каждому семинару отвечает своё домашнее задание.
Оно оценивается по шкале от 0 до 100 баллов.
В домашнем задании может быть несколько задач, баллы распределяются пропорционально трудности задач.
В оценке каждой задачи учитываются те же характеристики, что и в оценке задач экзамена.
Кроме того, выдаётся штраф за слишком долгое решение:
* Решение сдано до конца воскресенья, следующего за семинаром - штрафа нет.
* Каждая дополнительная неделя даёт штраф -6 баллов.
* После окончания семестра домашние задания не принимаются, за исключением явно оговорённых случаев.

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

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Файл:DA VP 47.pdf

2026-03-24T12:12:45Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 47.pdf»

Распределённые алгоритмы.
2024-2025, блок 47

Файл:DA VP 46.pdf

2026-03-24T12:12:39Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 46.pdf»

Распределённые алгоритмы.
2024-2025, блок 46

Файл:DA VP 45.pdf

2026-03-24T12:12:32Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 45.pdf»

Распределённые алгоритмы.
2024-2025, блок 45

Файл:DA VP 44.pdf

2026-03-24T12:12:23Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 44.pdf»

Распределённые алгоритмы.
2024-2025, блок 44

Распределённые алгоритмы

2026-03-24T12:02:52Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

= Слайды =

[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.

[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.

[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.

[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.

[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.

[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.

[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.

[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.

[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.

[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.

[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.

[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.

[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.

[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.

[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.

[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.

[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DA_VP_S03.pdf| Семинар 3.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.

[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда - Уоршелла.

[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга

[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди - Мисры.

[[Media: DA_VP_S04.pdf| Семинар 4.]] Алгоритмы маршрутизации.

[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.

[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.

[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.

[[Media: DA_VP_S05.pdf| Семинар 5.]] Сложность по времени.

[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DA_VP_25.pdf| Блок 25.]] Кольцевой волновой алгоритм.

[[Media: DA_VP_26.pdf| Блок 26.]] Древесный волновой алгоритм.

[[Media: DA_VP_27.pdf| Блок 27.]] Алгоритм эха.

[[Media: DA_VP_S06.pdf| Семинар 6.]] Приложения волновых алгоритмов.

[[Media: DA_VP_28.pdf| Блок 28.]] Распределённые алгоритмы обхода.

[[Media: DA_VP_29.pdf| Блок 29.]] Алгоритм Тарри.

[[Media: DA_VP_30.pdf| Блок 30.]] Классический обход в глубину.

[[Media: DA_VP_31.pdf| Блок 31.]] Алгоритм Авербаха.

Семинар 7 (без слайдов). Распределённые алгоритмы обхода.

[[Media: DA_VP_32.pdf| Блок 32.]] Задача избрания лидера: основные определения и допущения, избрание лидера INF-алгоритмом.

[[Media: DA_VP_33.pdf| Блок 33.]] Задача избрания лидера: эффект угасания.

[[Media: DA_VP_34.pdf| Блок 34.]] Избрание лидера в дереве.

[[Media: DA_VP_35.pdf| Блок 35.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.

[[Media: DA_VP_36.pdf| Блок 36.]] Задача избрания лидера: нижние оценки.

Семинар 8 (без слайдов). Задача избрания лидера, простейшие алгоритмы и свойства.

[[Media: DA_VP_37.pdf| Блок 37.]] Избрание лидера и построение остовного дерева: алгоритм Галлагера - Хамблета - Спиры (GHS).

Семинар 9 (без слайдов). Алгоритм Галлагера - Хамблета - Спиры.

[[Media: DA_VP_38.pdf| Блок 38.]] Задача сохранения снимка сети.

[[Media: DA_VP_39.pdf| Блок 39.]] Алгоритм Чанди - Лэмпорта.

[[Media: DA_VP_40.pdf| Блок 40.]] Алгоритм Лаи - Янга.

Семинар 10 (без слайдов). Сохранение снимка сети.

[[Media: DA_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи приниятия решения.

[[Media: DA_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DA_VP_43.pdf| Блок 43.]] Паксос.

Семинар 11 (без слайдов). Задача консенсуса, Паксос.

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

=== Прошлогодние ===

[[Media: DA_VP_44.pdf| Блок 44.]] Задача выявления конца вычислений.

[[Media: DA_VP_45.pdf| Блок 45.]] Выявление конца вычислений: алгоритм Дейкстры-Шолтена.

[[Media: DA_VP_46.pdf| Блок 46.]] Выявление конца вычислений: алгоритм Шави-Франчеза.

[[Media: DA_VP_47.pdf| Блок 47.]] Выявление конца вычислений: алгоритм возвращения кредита.

= Экзамен =

Экзамен проводится письменно, длительность - 100 минут.
Вариант экзамена содержит 5 задач такого же характера, как задачи домашних заданий в семестре.

Каждая задача оценивается по шкале от 0 до 100 баллов.
В оценке задачи учитываются следующие характеристики решения:
* Полнота - учтены все детали, разобраны все случаи и т.п.
* Корректность - все утверждения в решении правильны.
* Строгость - решение написано грамотно, в том числе математически грамотно.
Средний балл по всем задачам преобразуется в оценку так: 80-100 - отлично, 60-79 - хорошо, 40-59 - удовлетворительно, менее 40 - неудовлетворительно.

Можно пользоваться лекциями, книгами, конспектами.
Нельзя пользоваться никакими иными неодобренными источниками.
Имейте в виду, что времени на решение задач даётся не очень много, поэтому использование материалов на экзамене не заменяет подготовку к нему.

= Домашние задания =

Желающие облегчить экзамен (в том числе избежать его - получить автомат) могут выполнять домашние задания во время семестра.

Каждому семинару отвечает своё домашнее задание.
Оно оценивается по шкале от 0 до 100 баллов.
В домашнем задании может быть несколько задач, баллы распределяются пропорционально трудности задач.
В оценке каждой задачи учитываются те же характеристики, что и в оценке задач экзамена.
Кроме того, выдаётся штраф за слишком долгое решение:
* Решение сдано до конца воскресенья, следующего за семинаром - штрафа нет.
* Каждая дополнительная неделя даёт штраф -6 баллов.
* После окончания семестра домашние задания не принимаются, за исключением явно оговорённых случаев.

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

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Файл:DA VP 43.pdf

2026-03-24T11:59:53Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 43.pdf»

распределенные алгоритмы 2023-2024, блок 43

Файл:DA VP 42.pdf

2026-03-24T11:59:48Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 42.pdf»

распределенные алгоритмы 2023-2024, блок 42

Файл:DA VP 41.pdf

2026-03-24T11:59:42Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 41.pdf»

распределенные алгоритмы 2023-2024, блок 41

Файл:DA VP 40.pdf

2026-03-24T11:59:34Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 40.pdf»

распределённые алгоритмы, весна 2023-2024, блок 40

Файл:DA VP 39.pdf

2026-03-24T11:59:28Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 39.pdf»

распределённые алгоритмы, весна 2023-2024, блок 39

Файл:DA VP 38.pdf

2026-03-24T11:59:21Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 38.pdf»

распределённые алгоритмы, весна 2023-2024, блок 38

Файл:DA VP 37.pdf

2026-03-24T11:59:16Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 37.pdf»

распределённые алгоритмы, весна 2023-2024, блок 37

Файл:DA VP 36.pdf

2026-03-24T11:59:10Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 36.pdf»

распределённые алгоритмы, весна 2023-2024, блок 36

Файл:DA VP 35.pdf

2026-03-24T11:59:05Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 35.pdf»

распределённые алгоритмы, весна 2023-2024, блок 35

Файл:DA VP 34.pdf

2026-03-24T11:58:57Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 34.pdf»

распределённые алгоритмы, весна 2023-2024, блок 34

Файл:DA VP 33.pdf

2026-03-24T11:58:51Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 33.pdf»

распределённые алгоритмы, весна 2023-2024, блок 33

Файл:DA VP 32.pdf

2026-03-24T11:58:45Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 32.pdf»

распределённые алгоритмы, весна 2023-2024, блок 32

Файл:DA VP 20.pdf

2026-03-24T11:13:55Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 20.pdf»

распределённые алгоритмы, весна 2023-2024, блок 20

Файл:DA VP 18.pdf

2026-03-24T11:13:42Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 18.pdf»

распределённые алгоритмы, весна 2023-2024, блок 18

Распределённые алгоритмы

2026-03-24T10:52:57Z

PodymovVV:

[[Категория:Лекционные курсы кафедры МК]]

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

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

= Слайды =

[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.

[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.

[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.

[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.

[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.

[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.

[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.

[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.

[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.

[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.

[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.

[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.

[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.

[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.

[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.

[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.

[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.

[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.

[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.

[[Media: DA_VP_S03.pdf| Семинар 3.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.

[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда-Уоршелла.

[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга

[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди-Мисры.

[[Media: DA_VP_S04.pdf| Семинар 4.]] Алгоритмы маршрутизации.

[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.

[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.

[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.

[[Media: DA_VP_S05.pdf| Семинар 5.]] Сложность по времени.

[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.

[[Media: DA_VP_25.pdf| Блок 25.]] Кольцевой волновой алгоритм.

[[Media: DA_VP_26.pdf| Блок 26.]] Древесный волновой алгоритм.

[[Media: DA_VP_27.pdf| Блок 27.]] Алгоритм эха.

[[Media: DA_VP_S06.pdf| Семинар 6.]] Приложения волновых алгоритмов.

[[Media: DA_VP_28.pdf| Блок 28.]] Распределённые алгоритмы обхода.

[[Media: DA_VP_29.pdf| Блок 29.]] Алгоритм Тарри.

[[Media: DA_VP_30.pdf| Блок 30.]] Классический обход в глубину.

[[Media: DA_VP_31.pdf| Блок 31.]] Алгоритм Авербаха.

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

=== Прошлогодние ===

[[Media: DA_VP_32.pdf| Блок 32.]] Задача избрания лидера: основные определения и допущения, избрание лидера INF-алгоритмом.

[[Media: DA_VP_33.pdf| Блок 33.]] Задача избрания лидера: эффект угасания.

[[Media: DA_VP_34.pdf| Блок 34.]] Избрание лидера в дереве.

[[Media: DA_VP_35.pdf| Блок 35.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.

[[Media: DA_VP_36.pdf| Блок 36.]] Задача избрания лидера: нижние оценки.

[[Media: DA_VP_37.pdf| Блок 37.]] Избрание лидера и построение остовного дерева: алгоритм Галлагера-Хамблета-Спиры (GHS).

[[Media: DA_VP_38.pdf| Блок 38.]] Задача сохранения снимка сети.

[[Media: DA_VP_39.pdf| Блок 39.]] Алгоритм Чанди-Лэмпорта.

[[Media: DA_VP_40.pdf| Блок 40.]] Алгоритм Лаи-Янга.

[[Media: DA_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи приниятия решения.

[[Media: DA_VP_42.pdf| Блок 42.]] Задача консенсуса.

[[Media: DA_VP_43.pdf| Блок 43.]] Паксос.

[[Media: DA_VP_44.pdf| Блок 44.]] Задача выявления конца вычислений.

[[Media: DA_VP_45.pdf| Блок 45.]] Выявление конца вычислений: алгоритм Дейкстры-Шолтена.

[[Media: DA_VP_46.pdf| Блок 46.]] Выявление конца вычислений: алгоритм Шави-Франчеза.

[[Media: DA_VP_47.pdf| Блок 47.]] Выявление конца вычислений: алгоритм возвращения кредита.

= Экзамен =

Экзамен проводится письменно, длительность - 100 минут.
Вариант экзамена содержит 5 задач такого же характера, как задачи домашних заданий в семестре.

Каждая задача оценивается по шкале от 0 до 100 баллов.
В оценке задачи учитываются следующие характеристики решения:
* Полнота - учтены все детали, разобраны все случаи и т.п.
* Корректность - все утверждения в решении правильны.
* Строгость - решение написано грамотно, в том числе математически грамотно.
Средний балл по всем задачам преобразуется в оценку так: 80-100 - отлично, 60-79 - хорошо, 40-59 - удовлетворительно, менее 40 - неудовлетворительно.

Можно пользоваться лекциями, книгами, конспектами.
Нельзя пользоваться никакими иными неодобренными источниками.
Имейте в виду, что времени на решение задач даётся не очень много, поэтому использование материалов на экзамене не заменяет подготовку к нему.

= Домашние задания =

Желающие облегчить экзамен (в том числе избежать его - получить автомат) могут выполнять домашние задания во время семестра.

Каждому семинару отвечает своё домашнее задание.
Оно оценивается по шкале от 0 до 100 баллов.
В домашнем задании может быть несколько задач, баллы распределяются пропорционально трудности задач.
В оценке каждой задачи учитываются те же характеристики, что и в оценке задач экзамена.
Кроме того, выдаётся штраф за слишком долгое решение:
* Решение сдано до конца воскресенья, следующего за семинаром - штрафа нет.
* Каждая дополнительная неделя даёт штраф -6 баллов.
* После окончания семестра домашние задания не принимаются, за исключением явно оговорённых случаев.

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

= Литература =

#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.

Файл:DA VP 31.pdf

2026-03-24T10:51:43Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 31.pdf»

распределённые алгоритмы, весна 2023-2024, блок 31

Файл:DA VP 30.pdf

2026-03-24T10:51:35Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 30.pdf»

распределённые алгоритмы, 2023-2024, блок 30

Файл:DA VP 29.pdf

2026-03-24T10:51:22Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 29.pdf»

распределённые алгоритмы, 2023-2024, блок 29

Файл:DA VP 28.pdf

2026-03-24T10:51:15Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 28.pdf»

распределённые алгоритмы, 2023-2024, блок 28

Файл:DA VP 27.pdf

2026-03-24T10:50:45Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 27.pdf»

распределённые алгоритмы, весна 2023-2024, блок 27

Файл:DA VP 26.pdf

2026-03-24T10:50:36Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 26.pdf»

распределённые алгоритмы, весна 2023-2024, блок 26

Файл:DA VP 25.pdf

2026-03-24T10:50:29Z

PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 25.pdf»

распределённые алгоритмы, весна 2023-2024, блок 25