https://mk.cs.msu.ru/api.php?action=feedcontributions&user=PodymovVV&feedformat=atomКафедра математической кибернетики - Вклад участника [ru]2024-03-29T09:53:59ZВклад участникаMediaWiki 1.22.5//mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_(318,_319/2,_241,_242)Математическая логика (318, 319/2, 241, 242)2024-03-26T12:16:58Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
= Слайды лекций =<br />
<br />
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.<br />
<br />
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).<br />
<br />
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.<br />
<br />
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).<br />
<br />
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?<br />
<br />
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.<br />
<br />
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).<br />
<br />
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.<br />
<br />
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.<br />
<br />
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.<br />
<br />
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.<br />
<br />
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.<br />
<br />
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.<br />
<br />
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).<br />
<br />
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).<br />
<br />
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.<br />
<br />
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.<br />
<br />
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.<br />
<br />
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.<br />
<br />
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).<br />
<br />
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.<br />
<br />
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.<br />
<br />
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.<br />
<br />
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.<br />
<br />
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.<br />
<br />
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.<br />
<br />
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.<br />
<br />
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.<br />
<br />
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.<br />
<br />
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).<br />
<br />
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.<br />
<br />
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.<br />
<br />
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.<br />
<br />
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.<br />
<br />
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.<br />
<br />
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.<br />
<br />
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.<br />
<br />
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.<br />
<br />
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.<br />
<br />
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.<br />
<br />
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.<br />
<br />
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.<br />
<br />
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.<br />
<br />
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.<br />
<br />
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.<br />
<br />
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.<br />
<br />
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.<br />
<br />
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.<br />
<br />
= Семинары =<br />
<br />
''Материалы семинаров будут обновляться по мере проведения занятий''<br />
<br />
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]<br />
<br />
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]<br />
<br />
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]<br />
<br />
= Контрольные работы =<br />
<br />
Контрольные работы проводятся письменно, длительность каждой - 90 минут.<br />
<br />
В контрольных работах встретятся 4 типовые задачи со следующими темами:<br />
# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
# Доказать формулу в натуральном исчислении предикатов.<br />
<br />
Оценка решений типовых задач:<br />
* Максимальная оценка - 4 балла.<br />
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.<br />
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.<br />
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.<br />
<br />
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.<br />
Правильно решённый теоретический вопрос оценивается в 1 балл.<br />
<br />
'''Первая контрольная работа''' будет содержать<br />
* 3 типовые задачи по темам 1-3 и<br />
* 9 теоретических вопросов по прочитанным лекциям.<br />
<br />
'''Вторая контрольная работа''' будет содержать<br />
* 4 типовые задачи по всем темам и<br />
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.<br />
<br />
'''Остальные контрольные работы''' будут содержать<br />
* 4 типовые задачи по всем темам и<br />
* 14 теоретических вопросов по всем лекциям.<br />
<br />
= Зачёт =<br />
<br />
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.<br />
При проставлении зачёта учитывается 6 технических оценок:<br />
* Четыре оценки за типовые задачи, по одной за каждую задачу.<br />
* Оценка за знание теории. Максимум - 14 баллов.<br />
* Оценка за решение премиальных задач.<br />
<br />
Для получения зачёта требуется получить два результата:<br />
# Набрать хотя бы 11 баллов за типовые задачи.<br />
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).<br />
<br />
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].<br />
<br />
Для решения каждой типовой задачи будет предложено несколько попыток.<br />
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.<br />
<br />
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных<br />
* суммарно за первые две контрольные работы и<br />
* за каждую из следующих контрольных работ.<br />
<br />
= Экзамен =<br />
<br />
Формат проведения и длительность экзамена: письменно, 120 минут.<br />
<br />
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.<br />
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].<br />
Согласно набранной сумме технических баллов выставляется оценка:<br />
* хотя бы 30: '''отлично''';<br />
* хотя бы 23, но менее 30: '''хорошо''';<br />
* хотя бы 16, но менее 23: '''удовлетворительно''';<br />
* менее 16: '''неудовлетворительно'''.<br />
<br />
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:<br />
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:<br />
*# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
*# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
*# Доказать формулу в натуральном исчислении предикатов.<br />
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:<br />
*# Сформулировать утверждение, определение и т.п.<br />
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.<br />
*# Аргументировать (обосновать) ответ на вопрос.<br />
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:<br />
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.<br />
** Невыбранные ответы обосновывать не нужно.<br />
<br />
== Контрольная работа ==<br />
<br />
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].<br />
Максимальная техническая оценка за эту работу - 21 балл.<br />
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:<br />
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;<br />
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;<br />
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;<br />
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;<br />
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;<br />
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;<br />
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.<br />
<br />
= Премиальные задачи =<br />
<br />
Общие условия сдачи решений премиальных задач:<br />
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение. <br />
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.<br />
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.<br />
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.<br />
<br />
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.<br />
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".<br />
<br />
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.<br />
<br />
= Программа курса =<br />
<br />
''Программа будет обновляться согласно фактически прочитанному материалу''<br />
<br />
== Классические логики ==<br />
<ol><br />
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.<br />
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.<br />
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).<br />
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.<br />
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.<br />
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.<br />
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.<br />
<li> Машины Тьюринга. Теорема Чёрча.<br />
<li> Равносильные формулы. Теорема о равносильной замене.<br />
</ol><br />
<br />
== Метод резолюций в логике предикатов ==<br />
<ol start="10"><br />
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.<br />
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.<br />
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.<br />
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.<br />
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.<br />
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.<br />
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.<br />
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.<br />
<li> Метод резолюций: общая схема, применение.<br />
</ol><br />
<br />
== Логические исчисления ==<br />
<ol start="19"><br />
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.<br />
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.<br />
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.<br />
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).<br />
</ol><br />
<br />
== Аксиоматические теории ==<br />
<ol start="23"><br />
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.<br />
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.<br />
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.<br />
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).<br />
<li> Арифметика Пресбургера, её разрешимость и выразительность.<br />
</ol><br />
<br />
== Неклассические прикладные логики ==<br />
<ol start="28"><br />
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.<br />
<li> Интуиционистская логика.<br />
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.<br />
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.<br />
</ol><br />
<br />
= Рекомендованная литература =<br />
<br />
== Основная литература ==<br />
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.<br />
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.<br />
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.<br />
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.<br />
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.<br />
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.<br />
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.<br />
<br />
== Дополнительная литература ==<br />
<br />
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.<br />
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.<br />
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.<br />
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.<br />
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.<br />
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.<br />
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.<br />
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.<br />
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.<br />
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.<br />
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.<br />
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.<br />
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b32.pdfФайл:Mathlog 318 b32.pdf2024-03-26T12:16:05Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b32.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 32. Натуральное исчисление предикатов (полнота)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b31.pdfФайл:Mathlog 318 b31.pdf2024-03-26T12:15:43Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b31.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 31. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b29.pdfФайл:Mathlog 318 b29.pdf2024-03-25T11:51:19Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b29.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 29. Натуральное исчисление высказываний (полнота)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b28.pdfФайл:Mathlog 318 b28.pdf2024-03-25T11:51:11Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b28.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 28. Натуральное исчисление высказываний (корректность)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b27.pdfФайл:Mathlog 318 b27.pdf2024-03-25T11:51:03Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b27.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 27. Натуральное исчисление высказываний (основные определения)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b26.pdfФайл:Mathlog 318 b26.pdf2024-03-25T11:50:55Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b26.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 26. Устройство доказательств, логические исчисления</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b24.pdfФайл:Mathlog 318 b24.pdf2024-03-25T11:50:45Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b24.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 24. Полнота резолютивного вывода и теорема Эрбрана</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A0%D0%B0%D1%81%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D1%8B%D0%B5_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D1%8BРаспределённые алгоритмы2024-03-25T08:20:52Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
= Слайды =<br />
<br />
== Лекции ==<br />
<br />
[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.<br />
<br />
[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.<br />
<br />
[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.<br />
<br />
[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.<br />
<br />
[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.<br />
<br />
[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.<br />
<br />
[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.<br />
<br />
[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.<br />
<br />
[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.<br />
<br />
[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга<br />
<br />
[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди-Мисры.<br />
<br />
[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.<br />
<br />
[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.<br />
<br />
[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.<br />
<br />
[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DA_VP_25.pdf| Блок 25.]] Кольцевой волновой алгоритм.<br />
<br />
[[Media: DA_VP_26.pdf| Блок 26.]] Древесный волновой алгоритм.<br />
<br />
[[Media: DA_VP_27.pdf| Блок 27.]] Алгоритм эха.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Семинары ==<br />
<br />
[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.<br />
<br />
[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.<br />
<br />
[[Media: DA_VP_S04.pdf| Семинар 4.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_S05.pdf| Семинар 5.]] Алгоритмы маршрутизации.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.<br />
<br />
[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.<br />
<br />
[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов<br />
<br />
[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.<br />
<br />
[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.<br />
<br />
[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.<br />
<br />
[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.<br />
<br />
[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.<br />
<br />
[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.<br />
<br />
[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.<br />
<br />
[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.<br />
<br />
[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.<br />
<br />
[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.<br />
<br />
[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.<br />
<br />
[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.<br />
<br />
[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.<br />
<br />
[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.<br />
<br />
[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.<br />
<br />
[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.<br />
<br />
[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.<br />
<br />
[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.<br />
<br />
[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.<br />
<br />
[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.<br />
<br />
[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.<br />
<br />
[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галлагера-Хамблета-Спиры (GHS).<br />
<br />
[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.<br />
<br />
[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.<br />
<br />
[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.<br />
<br />
[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.<br />
<br />
[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.<br />
<br />
[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.<br />
<br />
[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.<br />
<br />
[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.<br />
<br />
[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.<br />
<br />
[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.<br />
<br />
= Литература =<br />
<br />
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)<br />
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)<br />
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_27.pdfФайл:DA VP 27.pdf2024-03-25T08:19:57Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 27</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 27</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_26.pdfФайл:DA VP 26.pdf2024-03-25T08:19:43Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 26</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 26</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_25.pdfФайл:DA VP 25.pdf2024-03-25T08:19:27Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 25</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 25</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_(318,_319/2,_241,_242)Математическая логика (318, 319/2, 241, 242)2024-03-24T19:05:34Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
= Слайды лекций =<br />
<br />
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.<br />
<br />
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).<br />
<br />
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.<br />
<br />
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).<br />
<br />
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?<br />
<br />
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.<br />
<br />
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).<br />
<br />
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.<br />
<br />
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.<br />
<br />
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.<br />
<br />
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.<br />
<br />
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.<br />
<br />
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.<br />
<br />
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).<br />
<br />
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).<br />
<br />
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.<br />
<br />
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.<br />
<br />
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.<br />
<br />
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.<br />
<br />
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).<br />
<br />
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.<br />
<br />
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.<br />
<br />
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.<br />
<br />
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.<br />
<br />
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.<br />
<br />
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.<br />
<br />
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).<br />
<br />
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.<br />
<br />
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.<br />
<br />
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).<br />
<br />
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.<br />
<br />
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.<br />
<br />
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.<br />
<br />
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.<br />
<br />
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.<br />
<br />
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.<br />
<br />
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.<br />
<br />
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.<br />
<br />
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.<br />
<br />
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.<br />
<br />
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.<br />
<br />
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.<br />
<br />
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.<br />
<br />
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.<br />
<br />
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.<br />
<br />
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.<br />
<br />
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.<br />
<br />
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.<br />
<br />
= Семинары =<br />
<br />
''Материалы семинаров будут обновляться по мере проведения занятий''<br />
<br />
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]<br />
<br />
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]<br />
<br />
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]<br />
<br />
= Контрольные работы =<br />
<br />
Контрольные работы проводятся письменно, длительность каждой - 90 минут.<br />
<br />
В контрольных работах встретятся 4 типовые задачи со следующими темами:<br />
# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
# Доказать формулу в натуральном исчислении предикатов.<br />
<br />
Оценка решений типовых задач:<br />
* Максимальная оценка - 4 балла.<br />
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.<br />
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.<br />
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.<br />
<br />
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.<br />
Правильно решённый теоретический вопрос оценивается в 1 балл.<br />
<br />
'''Первая контрольная работа''' будет содержать<br />
* 3 типовые задачи по темам 1-3 и<br />
* 9 теоретических вопросов по прочитанным лекциям.<br />
<br />
'''Вторая контрольная работа''' будет содержать<br />
* 4 типовые задачи по всем темам и<br />
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.<br />
<br />
'''Остальные контрольные работы''' будут содержать<br />
* 4 типовые задачи по всем темам и<br />
* 14 теоретических вопросов по всем лекциям.<br />
<br />
= Зачёт =<br />
<br />
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.<br />
При проставлении зачёта учитывается 6 технических оценок:<br />
* Четыре оценки за типовые задачи, по одной за каждую задачу.<br />
* Оценка за знание теории. Максимум - 14 баллов.<br />
* Оценка за решение премиальных задач.<br />
<br />
Для получения зачёта требуется получить два результата:<br />
# Набрать хотя бы 11 баллов за типовые задачи.<br />
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).<br />
<br />
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].<br />
<br />
Для решения каждой типовой задачи будет предложено несколько попыток.<br />
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.<br />
<br />
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных<br />
* суммарно за первые две контрольные работы и<br />
* за каждую из следующих контрольных работ.<br />
<br />
= Экзамен =<br />
<br />
Формат проведения и длительность экзамена: письменно, 120 минут.<br />
<br />
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.<br />
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].<br />
Согласно набранной сумме технических баллов выставляется оценка:<br />
* хотя бы 30: '''отлично''';<br />
* хотя бы 23, но менее 30: '''хорошо''';<br />
* хотя бы 16, но менее 23: '''удовлетворительно''';<br />
* менее 16: '''неудовлетворительно'''.<br />
<br />
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:<br />
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:<br />
*# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
*# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
*# Доказать формулу в натуральном исчислении предикатов.<br />
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:<br />
*# Сформулировать утверждение, определение и т.п.<br />
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.<br />
*# Аргументировать (обосновать) ответ на вопрос.<br />
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:<br />
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.<br />
** Невыбранные ответы обосновывать не нужно.<br />
<br />
== Контрольная работа ==<br />
<br />
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].<br />
Максимальная техническая оценка за эту работу - 21 балл.<br />
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:<br />
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;<br />
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;<br />
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;<br />
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;<br />
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;<br />
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;<br />
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.<br />
<br />
= Премиальные задачи =<br />
<br />
Общие условия сдачи решений премиальных задач:<br />
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение. <br />
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.<br />
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.<br />
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.<br />
<br />
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.<br />
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".<br />
<br />
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.<br />
<br />
= Программа курса =<br />
<br />
''Программа будет обновляться согласно фактически прочитанному материалу''<br />
<br />
== Классические логики ==<br />
<ol><br />
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.<br />
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.<br />
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).<br />
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.<br />
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.<br />
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.<br />
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.<br />
<li> Машины Тьюринга. Теорема Чёрча.<br />
<li> Равносильные формулы. Теорема о равносильной замене.<br />
</ol><br />
<br />
== Метод резолюций в логике предикатов ==<br />
<ol start="10"><br />
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.<br />
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.<br />
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.<br />
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.<br />
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.<br />
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.<br />
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.<br />
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.<br />
<li> Метод резолюций: общая схема, применение.<br />
</ol><br />
<br />
== Логические исчисления ==<br />
<ol start="19"><br />
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.<br />
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.<br />
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.<br />
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).<br />
</ol><br />
<br />
== Аксиоматические теории ==<br />
<ol start="23"><br />
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.<br />
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.<br />
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.<br />
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).<br />
<li> Арифметика Пресбургера, её разрешимость и выразительность.<br />
</ol><br />
<br />
== Неклассические прикладные логики ==<br />
<ol start="28"><br />
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.<br />
<li> Интуиционистская логика.<br />
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.<br />
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.<br />
</ol><br />
<br />
= Рекомендованная литература =<br />
<br />
== Основная литература ==<br />
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.<br />
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.<br />
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.<br />
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.<br />
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.<br />
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.<br />
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.<br />
<br />
== Дополнительная литература ==<br />
<br />
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.<br />
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.<br />
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.<br />
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.<br />
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.<br />
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.<br />
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.<br />
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.<br />
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.<br />
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.<br />
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.<br />
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.<br />
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b30.pdfФайл:Mathlog 318 b30.pdf2024-03-24T19:05:12Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b30.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 30. Натуральное исчисление предикатов (основные определения, корректность)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b29.pdfФайл:Mathlog 318 b29.pdf2024-03-24T19:05:05Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b29.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 29. Натуральное исчисление высказываний (полнота)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b28.pdfФайл:Mathlog 318 b28.pdf2024-03-24T19:04:58Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b28.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 28. Натуральное исчисление высказываний (корректность)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b27.pdfФайл:Mathlog 318 b27.pdf2024-03-24T19:04:49Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b27.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 27. Натуральное исчисление высказываний (основные определения)</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_24.pdfФайл:DA VP 24.pdf2024-03-24T11:10:29Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 24.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 24</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_(318,_319/2,_241,_242)Математическая логика (318, 319/2, 241, 242)2024-03-19T09:49:19Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
= Слайды лекций =<br />
<br />
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.<br />
<br />
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).<br />
<br />
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.<br />
<br />
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).<br />
<br />
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?<br />
<br />
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.<br />
<br />
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).<br />
<br />
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.<br />
<br />
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.<br />
<br />
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.<br />
<br />
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.<br />
<br />
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.<br />
<br />
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.<br />
<br />
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).<br />
<br />
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).<br />
<br />
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.<br />
<br />
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.<br />
<br />
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.<br />
<br />
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.<br />
<br />
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).<br />
<br />
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.<br />
<br />
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.<br />
<br />
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.<br />
<br />
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.<br />
<br />
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.<br />
<br />
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.<br />
<br />
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).<br />
<br />
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.<br />
<br />
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.<br />
<br />
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).<br />
<br />
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.<br />
<br />
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.<br />
<br />
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.<br />
<br />
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.<br />
<br />
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.<br />
<br />
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.<br />
<br />
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.<br />
<br />
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.<br />
<br />
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.<br />
<br />
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.<br />
<br />
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.<br />
<br />
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.<br />
<br />
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.<br />
<br />
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.<br />
<br />
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.<br />
<br />
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.<br />
<br />
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.<br />
<br />
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.<br />
<br />
= Семинары =<br />
<br />
''Материалы семинаров будут обновляться по мере проведения занятий''<br />
<br />
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]<br />
<br />
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]<br />
<br />
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]<br />
<br />
= Контрольные работы =<br />
<br />
Контрольные работы проводятся письменно, длительность каждой - 90 минут.<br />
<br />
В контрольных работах встретятся 4 типовые задачи со следующими темами:<br />
# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
# Доказать формулу в натуральном исчислении предикатов.<br />
<br />
Оценка решений типовых задач:<br />
* Максимальная оценка - 4 балла.<br />
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.<br />
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.<br />
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.<br />
<br />
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.<br />
Правильно решённый теоретический вопрос оценивается в 1 балл.<br />
<br />
'''Первая контрольная работа''' будет содержать<br />
* 3 типовые задачи по темам 1-3 и<br />
* 9 теоретических вопросов по прочитанным лекциям.<br />
<br />
'''Вторая контрольная работа''' будет содержать<br />
* 4 типовые задачи по всем темам и<br />
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.<br />
<br />
'''Остальные контрольные работы''' будут содержать<br />
* 4 типовые задачи по всем темам и<br />
* 14 теоретических вопросов по всем лекциям.<br />
<br />
= Зачёт =<br />
<br />
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.<br />
При проставлении зачёта учитывается 6 технических оценок:<br />
* Четыре оценки за типовые задачи, по одной за каждую задачу.<br />
* Оценка за знание теории. Максимум - 14 баллов.<br />
* Оценка за решение премиальных задач.<br />
<br />
Для получения зачёта требуется получить два результата:<br />
# Набрать хотя бы 11 баллов за типовые задачи.<br />
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).<br />
<br />
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].<br />
<br />
Для решения каждой типовой задачи будет предложено несколько попыток.<br />
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.<br />
<br />
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных<br />
* суммарно за первые две контрольные работы и<br />
* за каждую из следующих контрольных работ.<br />
<br />
= Экзамен =<br />
<br />
Формат проведения и длительность экзамена: письменно, 120 минут.<br />
<br />
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.<br />
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].<br />
Согласно набранной сумме технических баллов выставляется оценка:<br />
* хотя бы 30: '''отлично''';<br />
* хотя бы 23, но менее 30: '''хорошо''';<br />
* хотя бы 16, но менее 23: '''удовлетворительно''';<br />
* менее 16: '''неудовлетворительно'''.<br />
<br />
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:<br />
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:<br />
*# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
*# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
*# Доказать формулу в натуральном исчислении предикатов.<br />
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:<br />
*# Сформулировать утверждение, определение и т.п.<br />
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.<br />
*# Аргументировать (обосновать) ответ на вопрос.<br />
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:<br />
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.<br />
** Невыбранные ответы обосновывать не нужно.<br />
<br />
== Контрольная работа ==<br />
<br />
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].<br />
Максимальная техническая оценка за эту работу - 21 балл.<br />
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:<br />
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;<br />
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;<br />
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;<br />
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;<br />
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;<br />
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;<br />
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.<br />
<br />
= Премиальные задачи =<br />
<br />
Общие условия сдачи решений премиальных задач:<br />
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение. <br />
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.<br />
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.<br />
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.<br />
<br />
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.<br />
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".<br />
<br />
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.<br />
<br />
= Программа курса =<br />
<br />
''Программа будет обновляться согласно фактически прочитанному материалу''<br />
<br />
== Классические логики ==<br />
<ol><br />
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.<br />
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.<br />
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).<br />
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.<br />
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.<br />
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.<br />
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.<br />
<li> Машины Тьюринга. Теорема Чёрча.<br />
<li> Равносильные формулы. Теорема о равносильной замене.<br />
</ol><br />
<br />
== Метод резолюций в логике предикатов ==<br />
<ol start="10"><br />
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.<br />
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.<br />
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.<br />
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.<br />
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.<br />
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.<br />
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.<br />
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.<br />
<li> Метод резолюций: общая схема, применение.<br />
</ol><br />
<br />
== Логические исчисления ==<br />
<ol start="19"><br />
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.<br />
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.<br />
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.<br />
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).<br />
</ol><br />
<br />
== Аксиоматические теории ==<br />
<ol start="23"><br />
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.<br />
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.<br />
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.<br />
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).<br />
<li> Арифметика Пресбургера, её разрешимость и выразительность.<br />
</ol><br />
<br />
== Неклассические прикладные логики ==<br />
<ol start="28"><br />
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.<br />
<li> Интуиционистская логика.<br />
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.<br />
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.<br />
</ol><br />
<br />
= Рекомендованная литература =<br />
<br />
== Основная литература ==<br />
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.<br />
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.<br />
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.<br />
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.<br />
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.<br />
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.<br />
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.<br />
<br />
== Дополнительная литература ==<br />
<br />
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.<br />
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.<br />
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.<br />
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.<br />
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.<br />
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.<br />
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.<br />
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.<br />
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.<br />
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.<br />
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.<br />
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.<br />
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b26.pdfФайл:Mathlog 318 b26.pdf2024-03-19T09:48:53Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b26.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 26. Устройство доказательств, логические исчисления</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b25.pdfФайл:Mathlog 318 b25.pdf2024-03-19T09:48:45Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b25.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 25. Метод резолюций - заключительный пример</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_24.pdfФайл:DA VP 24.pdf2024-03-19T07:44:55Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 24.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 24</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_21.pdfФайл:DA VP 21.pdf2024-03-19T07:44:44Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 21.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 21</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A0%D0%B0%D1%81%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D1%8B%D0%B5_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D1%8BРаспределённые алгоритмы2024-03-18T11:34:45Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
= Слайды =<br />
<br />
== Лекции ==<br />
<br />
[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.<br />
<br />
[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.<br />
<br />
[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.<br />
<br />
[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.<br />
<br />
[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.<br />
<br />
[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.<br />
<br />
[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.<br />
<br />
[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.<br />
<br />
[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.<br />
<br />
[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга<br />
<br />
[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди-Мисры.<br />
<br />
[[Media: DA_VP_21.pdf| Блок 21.]] Диаграммы событий. Причинно-следственный порядок событий.<br />
<br />
[[Media: DA_VP_22.pdf| Блок 22.]] Логические часы.<br />
<br />
[[Media: DA_VP_23.pdf| Блок 23.]] Сложность распределённого алгоритма по времени.<br />
<br />
[[Media: DA_VP_24.pdf| Блок 24.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Семинары ==<br />
<br />
[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.<br />
<br />
[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.<br />
<br />
[[Media: DA_VP_S04.pdf| Семинар 4.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_S05.pdf| Семинар 5.]] Алгоритмы маршрутизации.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.<br />
<br />
[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.<br />
<br />
[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов<br />
<br />
[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.<br />
<br />
[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.<br />
<br />
[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.<br />
<br />
[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.<br />
<br />
[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.<br />
<br />
[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.<br />
<br />
[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.<br />
<br />
[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.<br />
<br />
[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.<br />
<br />
[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.<br />
<br />
[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.<br />
<br />
[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.<br />
<br />
[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.<br />
<br />
[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.<br />
<br />
[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.<br />
<br />
[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.<br />
<br />
[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.<br />
<br />
[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.<br />
<br />
[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.<br />
<br />
[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.<br />
<br />
[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.<br />
<br />
[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галлагера-Хамблета-Спиры (GHS).<br />
<br />
[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.<br />
<br />
[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.<br />
<br />
[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.<br />
<br />
[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.<br />
<br />
[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.<br />
<br />
[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.<br />
<br />
[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.<br />
<br />
[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.<br />
<br />
[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.<br />
<br />
[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.<br />
<br />
= Литература =<br />
<br />
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)<br />
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)<br />
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_24.pdfФайл:DA VP 24.pdf2024-03-18T11:33:05Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 24</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 24</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_23.pdfФайл:DA VP 23.pdf2024-03-18T11:32:51Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 23</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 23</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_22.pdfФайл:DA VP 22.pdf2024-03-18T11:32:38Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 22</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 22</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_21.pdfФайл:DA VP 21.pdf2024-03-18T11:32:17Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 21</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 21</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A0%D0%B0%D1%81%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D1%8B%D0%B5_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D1%8BРаспределённые алгоритмы2024-03-17T10:44:39Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
= Слайды =<br />
<br />
== Лекции ==<br />
<br />
[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.<br />
<br />
[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.<br />
<br />
[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.<br />
<br />
[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.<br />
<br />
[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.<br />
<br />
[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.<br />
<br />
[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.<br />
<br />
[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.<br />
<br />
[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.<br />
<br />
[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга<br />
<br />
[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди-Мисры.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Семинары ==<br />
<br />
[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.<br />
<br />
[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.<br />
<br />
[[Media: DA_VP_S04.pdf| Семинар 4.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_S05.pdf| Семинар 5.]] Алгоритмы маршрутизации.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.<br />
<br />
[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.<br />
<br />
[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов<br />
<br />
[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.<br />
<br />
[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.<br />
<br />
[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.<br />
<br />
[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.<br />
<br />
[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.<br />
<br />
[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.<br />
<br />
[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.<br />
<br />
[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.<br />
<br />
[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.<br />
<br />
[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.<br />
<br />
[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.<br />
<br />
[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.<br />
<br />
[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.<br />
<br />
[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.<br />
<br />
[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.<br />
<br />
[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.<br />
<br />
[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.<br />
<br />
[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.<br />
<br />
[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.<br />
<br />
[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.<br />
<br />
[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.<br />
<br />
[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галлагера-Хамблета-Спиры (GHS).<br />
<br />
[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.<br />
<br />
[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.<br />
<br />
[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.<br />
<br />
[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.<br />
<br />
[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.<br />
<br />
[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.<br />
<br />
[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.<br />
<br />
[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.<br />
<br />
[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.<br />
<br />
[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.<br />
<br />
= Литература =<br />
<br />
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)<br />
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)<br />
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_S05.pdfФайл:DA VP S05.pdf2024-03-17T10:44:05Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, семинар 5</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, семинар 5</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A1%D0%BF%D0%B5%D1%86%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80%D1%8BСпецсеминары2024-03-16T15:55:22Z<p>PodymovVV: </p>
<hr />
<div>''Если хотите связаться с преподавателем, но не можете, то напишите [[Подымов Владислав Васильевич|ему]].''<br />
<br />
=2023-2024, весенний семестр=<br />
<br />
<br />
{| class="wikitable"<br />
!Название!!Руководители!!Время!!Место!!Целевая аудитория<br />
|-<br />
|[[Дискретные функции и сложность алгоритмов]]<br />
|[[Алексеев Валерий Борисович|Алекссев В.Б.]], [[Марченков Сергей Серафимович|Марченков С.С.]], [[Вороненко Андрей Анатольевич|Вороненко А.А.]]<br />
|<br />
|<br />
|rowspan="4"|студенты бакалавриата и магистратуры<br />
|-<br />
|[[Теория управляющих систем и математические модели СБИС]]<br />
|[[Ложкин Сергей Андреевич|Ложкин С.А.]], [[Романов Дмитрий Сергеевич|Романов Д.С.]], [[Шуплецов Михаил Сергеевич|Шуплецов М.С.]], [[Данилов Борис Радиславович|Данилов Б.Р.]]<br />
|четверг, 16:20-17:55<br />
|ауд. 506<br />
|-<br />
|[[Теоретические проблемы программирования]]<br />
|[[Подымов Владислав Васильевич|Подымов В.В.]], [[Владимирова Юлия Сергеевна|Владимирова Ю.С.]]<br />
|пятница, 16:20-17:55 или 18:00-19:35 (по объявлениям)<br />
|ауд. 508<br />
|-<br />
|[[Сложность решения дискретных задач]]<br />
|[[Селезнева Светлана Николаевна|Селезнева С.Н.]], [[Бухман Антон Владимирович|Бухман А.В.]]<br />
| <br />
| <br />
|-<br />
|}<br />
<br />
<br />
=2023-2024, осенний семестр=<br />
<br />
<br />
{| class="wikitable"<br />
!Название!!Руководители!!Время!!Место!!Целевая аудитория<br />
|-<br />
|[[Дискретные функции и сложность алгоритмов]]<br />
|[[Алексеев Валерий Борисович|Алекссев В.Б.]], [[Марченков Сергей Серафимович|Марченков С.С.]], [[Вороненко Андрей Анатольевич|Вороненко А.А.]]<br />
|<br />
|<br />
|rowspan="4"|студенты бакалавриата и магистратуры<br />
|-<br />
|[[Теория управляющих систем и математические модели СБИС]]<br />
|[[Ложкин Сергей Андреевич|Ложкин С.А.]], [[Романов Дмитрий Сергеевич|Романов Д.С.]], [[Шуплецов Михаил Сергеевич|Шуплецов М.С.]], [[Данилов Борис Радиславович|Данилов Б.Р.]]<br />
|среда, 14:45-16:15<br />
|ауд. 507<br />
|-<br />
|[[Теоретические проблемы программирования]]<br />
|[[Подымов Владислав Васильевич|Подымов В.В.]], [[Владимирова Юлия Сергеевна|Владимирова Ю.С.]]<br />
|вторник, 18:00-19:35<br />
|ауд. 503<br />
|-<br />
|[[Сложность решения дискретных задач]]<br />
|[[Селезнева Светлана Николаевна|Селезнева С.Н.]], [[Бухман Антон Владимирович|Бухман А.В.]]<br />
| <br />
| <br />
|-<br />
|}<br />
<br />
=2022-2023, весенний семестр=<br />
<br />
{| class="wikitable"<br />
!Название!!Руководители!!Время!!Место!!Целевая аудитория<br />
|-<br />
|[[Дискретные функции и сложность алгоритмов]]||[[Алексеев Валерий Борисович|Алекссев В.Б.]], [[Марченков Сергей Серафимович|Марченков С.С.]], [[Вороненко Андрей Анатольевич|Вороненко А.А.]]<br />
||||<br />
|rowspan="4"|студенты бакалавриата и магистратуры<br />
|-<br />
|[[Теория управляющих систем и математические модели СБИС]]||[[Ложкин Сергей Андреевич|Ложкин С.А.]], [[Романов Дмитрий Сергеевич|Романов Д.С.]], [[Шуплецов Михаил Сергеевич|Шуплецов М.С.]], [[Данилов Борис Радиславович|Данилов Б.Р.]]<br />
||вторник, 18:00-19:35||ауд. 508<br />
|-<br />
|[[Теоретические проблемы программирования]]||[[Подымов Владислав Васильевич|Подымов В.В.]], [[Владимирова Юлия Сергеевна|Владимирова Ю.С.]]<br />
||среда, 10:30-12:05||ауд. 507<br />
|-<br />
|[[Сложность решения дискретных задач]]||[[Селезнева Светлана Николаевна|Селезнева С.Н.]], [[Бухман Антон Владимирович|Бухман А.В.]]<br />
||||<br />
|-<br />
|}</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%9F%D1%80%D0%BE%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%D0%B4%D0%BB%D1%8F_2-%D0%B3%D0%BE_%D0%BA%D1%83%D1%80%D1%81%D0%B0Просеминар для 2-го курса2024-03-12T16:09:11Z<p>PodymovVV: </p>
<hr />
<div>{{DISPLAYTITLE:Просеминар для 2-го курса "Избранные вопросы дискретной математики и математической кибернетики"}}<br />
<br />
'''Информация о просеминаре 2023-2024 учебного года.'''<br />
<br />
= Общая информация =<br />
<br />
Просеминар предназначен для знакомства студентов 2 курса с основными направлениями и наиболее интересными результатами проводимых на кафедре и в лаборатории исследований в области дискретной математики, теории графов, сложности алгоритмов, теории синтеза, надёжности и контроля дискретных управляющих систем, а также с применением этих результатов при решении некоторых задач проектирования СБИС и программирования.<br />
<br />
Просеминар проводится в форме независимых лекций-семинаров, на которые приглашаются все заинтересованные студенты 1 и 2 курсов.<br />
Предварительных знаний не требуется.<br />
Занятия проходят '''по пятницам с 16:20 до 17:55 в ауд. 579'''.<br />
Первое занятие - 16.02.2024.<br />
<!-- <span style="background:#FFDDDD">28</span> --><br />
<br />
[[Информация для 2 курса|Общая информация о кафедре для студентов 2 курса бакалавриата.]]<br />
<br />
= Программа просеминара =<br />
<br />
'''Оптимальная структурная реализация булевых функций и графов в некоторых моделях'''<br />
<br />
* Докладчик: [[Ложкин Сергей Андреевич|С.А. Ложкин]]<br />
* Дата: 16.02.2024 и 01.03.2024.<br />
<br />
<span style="background:#FFDDDD"><br />
'''Временные автоматы и их эквивалентность'''<br />
</span><br />
<br />
* <span style="background:#FFDDDD">Докладчик:</span> [[Подымов Владислав Васильевич |В.В. Подымов]]<br />
* Дата: 15.03.2024.<br />
* Доклад посвящён разновидности автоматов, выполняющихся в условиях "непрерывно текущего" реального времени и предназначенных для моделирования и анализа вычислительных систем, компоненты которых имеют директивные сроки выполнения своих подзадач. Для этих автоматов будут обсуждаться некоторые результаты, касающиеся проверки их эквивалентности (схожести поведения) - относительно давние и относительно свежие, полученные докладчиком и не только.<br />
<br />
= Материалы докладов прошлых лет =<br />
<br />
== 2023 ==<br />
<br />
'''Сложность проверки свойств функций алгебры логики, заданных полиномами Жегалкина.'''<br />
<br />
* Докладчик: [[Селезнева Светлана Николаевна |Селезнева С.Н.]]<br />
* Дата: 04.04.2023.<br />
* Аннотация: При решении прикладных задач часто возникает необходимость в проверке свойств функций алгебры логики. При этом функции заданы определенным образом, в частности, нормальными формами. Одним из таких представлений являются полиномы Жегалкина. В докладе будут рассмотрены свойства монотонности, четности, периодичности, уравновешенности функции алгебры логики и показано, с какой сложностью можно проверить эти свойства функции по ее полиному Жегалкина.<br />
<br />
'''Прикладные задачи автоматизации проектирования интегральных схем.'''<br />
<br />
* Докладчик: [[Шуплецов Михаил Сергеевич |Шуплецов М.С.]]<br />
* Дата: 28.03.2023.<br />
* Аннотация: При решении задача проектирования интегральных схем возникает спектр прикладных математических задач из области дискретной математики и математической кибернетики. В докладе будут рассмотрены некоторые задачи, которые возникают на этапе логического проектирования интегральной схемы, а также некоторые задачи, связанные с верификацией схем.<br />
<br />
'''Проблемы сложности, надежности и контроля на примере реализации линейной и некоторых других булевых функций в модели контактных схем и BDD.'''<br />
<br />
* Докладчик: [[Ложкин Сергей Андреевич|Ложкин С.А.]]<br />
* Дата: 21.03.2023.<br />
* Аннотация: Решение основных проблем и задач теории дискретных управляющих систем, указанных в теме семинара, будет рассмотрено на примере счетчика четности, то есть суммы по модулю 2 заданного числа булевых переменных, при его реализации в классах контактных схем, являющихся моделью транзисторного уровня современных сверхбольших интегральных схем, и BDD. Для счетчика четности будут построены: минимальная контактная схема и близкий к минимальному тест, диагностирующий обрыв одного из ее контактов; минимальная схема, корректирующая обрыв одного контакта.<br />
<br />
'''Сложность алгоритмов на графах.'''<br />
<br />
* Докладчик: [[Алексеев Валерий Борисович|Алексеев В.Б.]]<br />
* Дата: 14.03.2023.<br />
* Аннотация: быстрый алгоритм транзитивного замыкания графа, быстрый приближенный алгоритм для поиска минимального вершинного покрытия, эйлеровы и гамильтоновы циклы, задача коммивояжера.<br />
<br />
'''Оптимальная реализация некоторых монотонных симметрических функций формулами на основе двоичных кодов.'''<br />
<br />
* Докладчик: [[Ложкин Сергей Андреевич|Ложкин С.А.]]<br />
* Дата: 07.03.2023.<br />
* [[Media: Proseminar 2023.03.07 annotation.pdf|Аннотация]].<br />
<br />
'''Сложность алгебраических вычислений - примеры быстрых алгоритмов и нерешенные задачи.'''<br />
<br />
* Докладчик: [[Алексеев Валерий Борисович|Алексеев В.Б.]]<br />
* Дата: 28.02.2023.<br />
* Аннотация: Будет рассказано про нерешенную до конца («зависшую») проблему быстрого умножения матриц, про неожиданный алгоритм Штрассена для этой задачи и его обобщения, про следствия для быстрых алгоритмов на графах и в целом про сложность алгебраических вычислений.<br />
<br />
== 2016 ==<br />
<br />
[[Media:2016_Proseminar_FPGA.pdf|Программируемые логические интегральные схемы.]] (2016, [[Шуплецов Михаил Сергеевич|Шуплецов М.С.]])<br />
<br />
[[Media:Proseminar_2016_Marchenko.pdf| Математические методы проектирования топологии СБИС.]] (2016, бывш. сотр. Марченко А.М.)<br />
<br />
[[Media:Prosem_2016_Podymov_Zakharov.pdf| Дискретные модели и задачи управления компьютерными сетями.]] (2016, [[Захаров Владимир Анатольевич|Захаров В.А.]] и [[Подымов Владислав Васильевич|Подымов В.В.]])</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_(318,_319/2,_241,_242)Математическая логика (318, 319/2, 241, 242)2024-03-12T11:21:44Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
= Слайды лекций =<br />
<br />
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.<br />
<br />
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).<br />
<br />
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.<br />
<br />
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).<br />
<br />
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?<br />
<br />
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.<br />
<br />
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).<br />
<br />
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.<br />
<br />
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.<br />
<br />
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.<br />
<br />
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.<br />
<br />
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.<br />
<br />
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.<br />
<br />
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).<br />
<br />
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).<br />
<br />
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.<br />
<br />
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.<br />
<br />
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.<br />
<br />
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.<br />
<br />
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).<br />
<br />
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.<br />
<br />
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.<br />
<br />
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.<br />
<br />
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.<br />
<br />
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.<br />
<br />
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.<br />
<br />
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).<br />
<br />
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.<br />
<br />
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.<br />
<br />
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).<br />
<br />
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.<br />
<br />
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.<br />
<br />
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.<br />
<br />
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.<br />
<br />
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.<br />
<br />
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.<br />
<br />
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.<br />
<br />
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.<br />
<br />
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.<br />
<br />
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.<br />
<br />
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.<br />
<br />
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.<br />
<br />
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.<br />
<br />
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.<br />
<br />
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.<br />
<br />
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.<br />
<br />
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.<br />
<br />
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.<br />
<br />
= Семинары =<br />
<br />
''Материалы семинаров будут обновляться по мере проведения занятий''<br />
<br />
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]<br />
<br />
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]<br />
<br />
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]<br />
<br />
= Контрольные работы =<br />
<br />
Контрольные работы проводятся письменно, длительность каждой - 90 минут.<br />
<br />
В контрольных работах встретятся 4 типовые задачи со следующими темами:<br />
# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
# Доказать формулу в натуральном исчислении предикатов.<br />
<br />
Оценка решений типовых задач:<br />
* Максимальная оценка - 4 балла.<br />
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.<br />
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.<br />
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.<br />
<br />
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.<br />
Правильно решённый теоретический вопрос оценивается в 1 балл.<br />
<br />
'''Первая контрольная работа''' будет содержать<br />
* 3 типовые задачи по темам 1-3 и<br />
* 9 теоретических вопросов по прочитанным лекциям.<br />
<br />
'''Вторая контрольная работа''' будет содержать<br />
* 4 типовые задачи по всем темам и<br />
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.<br />
<br />
'''Остальные контрольные работы''' будут содержать<br />
* 4 типовые задачи по всем темам и<br />
* 14 теоретических вопросов по всем лекциям.<br />
<br />
= Зачёт =<br />
<br />
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.<br />
При проставлении зачёта учитывается 6 технических оценок:<br />
* Четыре оценки за типовые задачи, по одной за каждую задачу.<br />
* Оценка за знание теории. Максимум - 14 баллов.<br />
* Оценка за решение премиальных задач.<br />
<br />
Для получения зачёта требуется получить два результата:<br />
# Набрать хотя бы 11 баллов за типовые задачи.<br />
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).<br />
<br />
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].<br />
<br />
Для решения каждой типовой задачи будет предложено несколько попыток.<br />
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.<br />
<br />
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных<br />
* суммарно за первые две контрольные работы и<br />
* за каждую из следующих контрольных работ.<br />
<br />
= Экзамен =<br />
<br />
Формат проведения и длительность экзамена: письменно, 120 минут.<br />
<br />
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.<br />
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].<br />
Согласно набранной сумме технических баллов выставляется оценка:<br />
* хотя бы 30: '''отлично''';<br />
* хотя бы 23, но менее 30: '''хорошо''';<br />
* хотя бы 16, но менее 23: '''удовлетворительно''';<br />
* менее 16: '''неудовлетворительно'''.<br />
<br />
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:<br />
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:<br />
*# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
*# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
*# Доказать формулу в натуральном исчислении предикатов.<br />
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:<br />
*# Сформулировать утверждение, определение и т.п.<br />
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.<br />
*# Аргументировать (обосновать) ответ на вопрос.<br />
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:<br />
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.<br />
** Невыбранные ответы обосновывать не нужно.<br />
<br />
== Контрольная работа ==<br />
<br />
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].<br />
Максимальная техническая оценка за эту работу - 21 балл.<br />
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:<br />
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;<br />
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;<br />
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;<br />
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;<br />
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;<br />
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;<br />
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.<br />
<br />
= Премиальные задачи =<br />
<br />
Общие условия сдачи решений премиальных задач:<br />
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение. <br />
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.<br />
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.<br />
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.<br />
<br />
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.<br />
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".<br />
<br />
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.<br />
<br />
= Программа курса =<br />
<br />
''Программа будет обновляться согласно фактически прочитанному материалу''<br />
<br />
== Классические логики ==<br />
<ol><br />
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.<br />
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.<br />
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).<br />
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.<br />
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.<br />
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.<br />
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.<br />
<li> Машины Тьюринга. Теорема Чёрча.<br />
<li> Равносильные формулы. Теорема о равносильной замене.<br />
</ol><br />
<br />
== Метод резолюций в логике предикатов ==<br />
<ol start="10"><br />
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.<br />
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.<br />
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.<br />
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.<br />
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.<br />
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.<br />
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.<br />
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.<br />
<li> Метод резолюций: общая схема, применение.<br />
</ol><br />
<br />
== Логические исчисления ==<br />
<ol start="19"><br />
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.<br />
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.<br />
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.<br />
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).<br />
</ol><br />
<br />
== Аксиоматические теории ==<br />
<ol start="23"><br />
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.<br />
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.<br />
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.<br />
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).<br />
<li> Арифметика Пресбургера, её разрешимость и выразительность.<br />
</ol><br />
<br />
== Неклассические прикладные логики ==<br />
<ol start="28"><br />
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.<br />
<li> Интуиционистская логика.<br />
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.<br />
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.<br />
</ol><br />
<br />
= Рекомендованная литература =<br />
<br />
== Основная литература ==<br />
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.<br />
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.<br />
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.<br />
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.<br />
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.<br />
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.<br />
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.<br />
<br />
== Дополнительная литература ==<br />
<br />
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.<br />
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.<br />
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.<br />
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.<br />
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.<br />
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.<br />
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.<br />
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.<br />
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.<br />
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.<br />
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.<br />
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.<br />
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b24.pdfФайл:Mathlog 318 b24.pdf2024-03-12T11:21:19Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b24.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 24. Полнота резолютивного вывода и теорема Эрбрана</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b23.pdfФайл:Mathlog 318 b23.pdf2024-03-12T11:21:12Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b23.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 23. Эрбрановские интерпретации</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b22.pdfФайл:Mathlog 318 b22.pdf2024-03-12T11:21:04Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b22.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 19. Пример обоснования общезначимости формулы методом резолюций</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_20.pdfФайл:DA VP 20.pdf2024-03-11T15:46:16Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 20.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 20</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_19.pdfФайл:DA VP 19.pdf2024-03-11T15:46:03Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 19.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 19</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_18.pdfФайл:DA VP 18.pdf2024-03-11T15:45:48Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 18.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 18</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A0%D0%B0%D1%81%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D1%8B%D0%B5_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D1%8BРаспределённые алгоритмы2024-03-11T13:08:58Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
= Слайды =<br />
<br />
== Лекции ==<br />
<br />
[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.<br />
<br />
[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.<br />
<br />
[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.<br />
<br />
[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.<br />
<br />
[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.<br />
<br />
[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.<br />
<br />
[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.<br />
<br />
[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.<br />
<br />
[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.<br />
<br />
[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DA_VP_18.pdf| Блок 18.]] Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DA_VP_19.pdf| Блок 19.]] Алгоритм Туэга<br />
<br />
[[Media: DA_VP_20.pdf| Блок 20.]] Алгоритм Чанди-Мисры.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Семинары ==<br />
<br />
[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.<br />
<br />
[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.<br />
<br />
[[Media: DA_VP_S04.pdf| Семинар 4.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.<br />
<br />
[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.<br />
<br />
[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов<br />
<br />
[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.<br />
<br />
[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.<br />
<br />
[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.<br />
<br />
[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.<br />
<br />
[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.<br />
<br />
[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.<br />
<br />
[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.<br />
<br />
[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.<br />
<br />
[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.<br />
<br />
[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.<br />
<br />
[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.<br />
<br />
[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.<br />
<br />
[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.<br />
<br />
[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.<br />
<br />
[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.<br />
<br />
[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.<br />
<br />
[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.<br />
<br />
[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.<br />
<br />
[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.<br />
<br />
[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.<br />
<br />
[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.<br />
<br />
[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галлагера-Хамблета-Спиры (GHS).<br />
<br />
[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.<br />
<br />
[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.<br />
<br />
[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.<br />
<br />
[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.<br />
<br />
[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.<br />
<br />
[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.<br />
<br />
[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.<br />
<br />
[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.<br />
<br />
[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.<br />
<br />
[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.<br />
<br />
= Литература =<br />
<br />
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)<br />
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)<br />
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_20.pdfФайл:DA VP 20.pdf2024-03-11T13:07:16Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 20</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 20</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_19.pdfФайл:DA VP 19.pdf2024-03-11T13:07:03Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 19</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 19</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_18.pdfФайл:DA VP 18.pdf2024-03-11T13:06:39Z<p>PodymovVV: распределённые алгоритмы, весна 2023-2024, блок 18</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 18</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_17.pdfФайл:DA VP 17.pdf2024-03-10T20:11:59Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 17.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 17</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A0%D0%B0%D1%81%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D1%8B%D0%B5_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D1%8BРаспределённые алгоритмы2024-03-10T16:23:22Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Обязательный курс для студентов группы 521. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
= Слайды =<br />
<br />
== Лекции ==<br />
<br />
[[Media: DA_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DA_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DA_VP_03.pdf| Блок 3.]] Иллюстрация трудности разработки распределённых алгоритмов: начало.<br />
<br />
[[Media: DA_VP_04.pdf| Блок 4.]] Системы переходов.<br />
<br />
[[Media: DA_VP_05.pdf| Блок 5.]] Справедливые вычисления систем.<br />
<br />
[[Media: DA_VP_06.pdf| Блок 6.]] Основные соглашения о псевдокоде.<br />
<br />
[[Media: DA_VP_07.pdf| Блок 7.]] Адресованные сообщения.<br />
<br />
[[Media: DA_VP_08.pdf| Блок 8.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DA_VP_09.pdf| Блок 9.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости. Свойства корректности симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_10.pdf| Блок 10.]] Безопасность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_11.pdf| Блок 11.]] Живость симметричного протокола раздвижного окна.<br />
<br />
[[Media: DA_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна. Протокол альтернирующих битов.<br />
<br />
[[Media: DA_VP_13.pdf| Блок 13.]] Напоминание о графах.<br />
<br />
[[Media: DA_VP_14.pdf| Блок 14.]] Типовые допущения и ограничения.<br />
<br />
[[Media: DA_VP_15.pdf| Блок 15.]] Коммуникационная и битовая сложности.<br />
<br />
[[Media: DA_VP_16.pdf| Блок 16.]] Задача маршрутизации.<br />
<br />
[[Media: DA_VP_17.pdf| Блок 17.]] Основные допущения в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Семинары ==<br />
<br />
[[Media: DA_VP_S01.pdf| Семинар 1.]] Псевдокод, системы переходов и справедливость на примере передачи данных с обеспечением надёжности.<br />
<br />
[[Media: DA_VP_S02.pdf| Семинар 2.]] Свойства безопасности и живости.<br />
<br />
[[Media: DA_VP_S04.pdf| Семинар 4.]] Вычисление таблиц маршрутизации. Коммуникационная и битовая сложности.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: DAS_VP_01.pdf| Блок 1.]] О чём этот курс. Литература.<br />
<br />
[[Media: DAS_VP_02.pdf| Блок 2.]] Вступление: несколько слов о распределённых системах, проблемы организации их вычислений, особенности распределённых алгоритмов.<br />
<br />
[[Media: DAS_VP_03.pdf| Блок 3.]] Модель распределённой системы: система переходов системы, система переходов узла, распределённый алгоритм, асинхронный и синхронный обмен сообщениями.<br />
<br />
[[Media: DAS_VP_04.pdf| Блок 4.]] Справедливые вычисления.<br />
<br />
[[Media: DAS_VP_05.pdf| Блок 5.]] Иллюстрация трудности разработки распределённых алгоритмов<br />
<br />
[[Media: DAS_VP_06.pdf| Блок 6.]] Причинно-следственный порядок событий.<br />
<br />
[[Media: DAS_VP_07.pdf| Блок 7.]] Логические часы.<br />
<br />
[[Media: DAS_VP_08.pdf| Блок 8.]] Дополнительные допущения. Сложность.<br />
<br />
[[Media: DAS_VP_09.pdf| Блок 9.]] Симметричный протокол раздвижного окна.<br />
<br />
[[Media: DAS_VP_10.pdf| Блок 10.]] Как обосновывать корректность распределённых алгоритмов. Свойства безопасности и живости.<br />
<br />
[[Media: DAS_VP_11.pdf| Блок 11.]] Корректность симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_12.pdf| Блок 12.]] Особенности реализации симметричного протокола раздвижного окна.<br />
<br />
[[Media: DAS_VP_13.pdf| Блок 13.]] Коммуникационный протокол с таймерами.<br />
<br />
[[Media: DAS_VP_14.pdf| Блок 14.]] Корректность протокола с таймерами.<br />
<br />
[[Media: DAS_VP_15.pdf| Блок 15.]] Задача маршрутизации.<br />
<br />
[[Media: DAS_VP_16.pdf| Блок 16.]] Основные допущения о весах в задаче маршрутизации. Маршрутизация и свойства графов.<br />
<br />
[[Media: DAS_VP_17.pdf| Блок 17.]] Построение оптимальных путей для всех пар вершин. Алгоритм Флойда-Уоршелла.<br />
<br />
[[Media: DAS_VP_18.pdf| Блок 18.]] Алгоритм маршрутизации Туэга.<br />
<br />
[[Media: DAS_VP_19.pdf| Блок 19.]] Алгоритм маршрутизации Мерлина-Сигалла.<br />
<br />
[[Media: DAS_VP_20.pdf| Блок 20.]] Алгоритм маршрутизации Чанди-Мисры.<br />
<br />
[[Media: DAS_VP_21.pdf| Блок 21.]] Волновые алгоритмы: основные определения и свойства.<br />
<br />
[[Media: DAS_VP_22.pdf| Блок 22.]] Применение волновых алгоритмов: PIF, SYN, INF.<br />
<br />
[[Media: DAS_VP_23.pdf| Блок 23.]] Примеры волновых алгоритмов: кольцевой алгоритм, древесный алгоритм, алгоритм эха.<br />
<br />
[[Media: DAS_VP_24.pdf| Блок 24.]] Примеры волновых алгоритмов: фазовый алгоритм.<br />
<br />
[[Media: DAS_VP_25.pdf| Блок 25.]] Примеры волновых алгоритмов: алгоритм Финна.<br />
<br />
[[Media: DAS_VP_26.pdf| Блок 26.]] Распределённые алгоритмы обхода. Алгоритм Тарри. Классический распределённый обход в глубину.<br />
<br />
[[Media: DAS_VP_27.pdf| Блок 27.]] Распределённый обход в глубину: алгоритм Авербаха.<br />
<br />
[[Media: DAS_VP_28.pdf| Блок 28.]] Алгоритмы избрания лидера: основные определения и допущения, волновое избрание лидера.<br />
<br />
[[Media: DAS_VP_29.pdf| Блок 29.]] Избрание лидера в дереве.<br />
<br />
[[Media: DAS_VP_30.pdf| Блок 30.]] Избрание лидера в кольце: алгоритм Ле-Ланна, алгоритм Ченя-Робертса.<br />
<br />
[[Media: DAS_VP_31.pdf| Блок 31.]] Избрание лидера: эффект угасания.<br />
<br />
[[Media: DAS_VP_32.pdf| Блок 32.]] Избрание лидера: нижние оценки.<br />
<br />
[[Media: DAS_VP_33.pdf| Блок 33.]] Избрание лидера: алгоритм Галлагера-Хамблета-Спиры (GHS).<br />
<br />
[[Media: DAS_VP_34.pdf| Блок 34.]] Задача сохранения снимка сети.<br />
<br />
[[Media: DAS_VP_35.pdf| Блок 35.]] Сохранение снимка сети: алгоритм Чанди-Лэмпорта.<br />
<br />
[[Media: DAS_VP_36.pdf| Блок 36.]] Сохранение снимка сети: алгоритм Лаи-Янга.<br />
<br />
[[Media: DAS_VP_37.pdf| Блок 37.]] Задача обнаружения завершения вычислений.<br />
<br />
[[Media: DAS_VP_38.pdf| Блок 38.]] Обнаружение завершения вычислений: алгоритм Дейкстры-Шолтена.<br />
<br />
[[Media: DAS_VP_39.pdf| Блок 39.]] Обнаружение завершения вычислений: алгоритм Шави-Франчеза.<br />
<br />
[[Media: DAS_VP_40.pdf| Блок 40.]] Обнаружение завершения вычислений: алгоритм возвращения кредита.<br />
<br />
[[Media: DAS_VP_41.pdf| Блок 41.]] Отказоустойчивые алгоритмы. Модели неисправностей. Задачи принятия решения.<br />
<br />
[[Media: DAS_VP_42.pdf| Блок 42.]] Задача консенсуса.<br />
<br />
[[Media: DAS_VP_43.pdf| Блок 43.]] Консенсус: Паксос.<br />
<br />
= Литература =<br />
<br />
#G. Tel. Introduction to Distributed Algorithms. Cambridge University Press. 2000. (русск. пер. Ж. Тель. Введение в распределенные алгоритмы, изд-во МЦНМО, 2009 г., 616 с.)<br />
#W. Fokkink. Distributed Algorithms: Intuitive Approach. The MIT Press. 2013. (русск. пер. У. Фоккинк. Распределенные алгоритмв: интуитивный подход., изд-во Питер, 2017 г., 231 с.)<br />
#N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996, 906 pp.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_S04.pdfФайл:DA VP S04.pdf2024-03-10T16:22:03Z<p>PodymovVV: распределённые алгоритмы, семинар 4</p>
<hr />
<div>распределённые алгоритмы, семинар 4</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:DA_VP_17.pdfФайл:DA VP 17.pdf2024-03-10T13:07:20Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:DA VP 17.pdf»</p>
<hr />
<div>распределённые алгоритмы, весна 2023-2024, блок 17</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%BB%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_(318,_319/2,_241,_242)Математическая логика (318, 319/2, 241, 242)2024-03-10T12:26:27Z<p>PodymovVV: </p>
<hr />
<div>[[Категория:Лекционные курсы кафедры МК]]<br />
<br />
Актуальность информации: весенний семестр 2023/2024 учебного года.<br />
<br />
Обязательный курс для студентов групп 318 и 319/2, ''а также 241 и 242 (Математическая логика и теория алгоритмов)''. Курс читает [[Подымов Владислав Васильевич|В. В. Подымов]].<br />
<br />
= Слайды лекций =<br />
<br />
[[Media: Mathlog_318_b1.pdf|Блок 1]] (вводный). Что такое логика. Несколько логических парадоксов. Чего ожидать в курсе.<br />
<br />
[[Media: Mathlog_318_b2.pdf|Блок 2]]. Логика высказываний: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b3.pdf|Блок 3]]. Логика предикатов: синтаксис, семантика.<br />
<br />
[[Media: Mathlog_318_b4.pdf|Блок 4]]. Как формализовать предложение на языке логики предикатов (пример).<br />
<br />
[[Media: Mathlog_318_b5.pdf|Блок 5]]. Логика высказываний: выполнимые и общезначимые формулы.<br />
<br />
[[Media: Mathlog_318_b6.pdf|Блок 6]]. Логика предикатов: выполнимые и общезначимые формулы; модели формул; логическое следствие; проблема общезначимости формул (постановка).<br />
<br />
[[Media: Mathlog_318_b7.pdf|Блок 7]]. Логика предикатов: можно ли проверить общезначимость формулы "в лоб"?<br />
<br />
[[Media: Mathlog_318_b8.pdf|Блок 8]]. Метод семантических таблиц: семантические таблицы.<br />
<br />
[[Media: Mathlog_318_b9.pdf|Блок 9]]. Подстановки (основные определения).<br />
<br />
[[Media: Mathlog_318_b10.pdf|Блок 10]]. Метод семантических таблиц: табличный вывод.<br />
<br />
[[Media: Mathlog_318_b11.pdf|Блок 11]]. Метод семантических таблиц: корректность табличного вывода.<br />
<br />
[[Media: Mathlog_318_b12.pdf|Блок 12]]. Метод семантических таблиц: полнота табличного вывода.<br />
<br />
[[Media: Mathlog_318_b13.pdf|Блок 13]]. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Автоматизация доказательства теорем.<br />
<br />
[[Media: Mathlog_318_b14.pdf|Блок 14]]. Общая схема метода резолюций.<br />
<br />
[[Media: Mathlog_318_b15.pdf|Блок 15]]. Равносильность формул.<br />
<br />
[[Media: Mathlog_318_b16.pdf|Блок 16]]. Предварённая нормальная форма (ПНФ).<br />
<br />
[[Media: Mathlog_318_b17.pdf|Блок 17]]. Сколемовская стандартная форма (ССФ).<br />
<br />
[[Media: Mathlog_318_b18.pdf|Блок 18]]. Системы дизъюнктов.<br />
<br />
[[Media: Mathlog_318_b19.pdf|Блок 19]]. Композиция подстановок. Постановка задачи унификации.<br />
<br />
[[Media: Mathlog_318_b20.pdf|Блок 20]]. Алгоритм унификации атомарных формул.<br />
<br />
[[Media: Mathlog_318_b21.pdf|Блок 21]]. Монотонность и транзитивность отношения логического следования.<br />
<br />
''Слайды будут появляться по мере чтения лекций.''<br />
<br />
== Прошлогодние слайды ==<br />
<br />
[[Media: Mathlog_318_b22.pdf|Блок 22]]. Резолютивный вывод. Корректность резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b23.pdf|Блок 23]]. Обоснование общезначимости формулы методом резолюций (пример).<br />
<br />
[[Media: Mathlog_318_b24.pdf|Блок 24]]. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях.<br />
<br />
[[Media: Mathlog_318_b25.pdf|Блок 25]]. Теорема Эрбрана. Полнота резолютивного вывода.<br />
<br />
[[Media: Mathlog_318_b26.pdf|Блок 26]]. Даша, Саша, Паша, пиво и метод семантических таблиц с методом резолюций.<br />
<br />
[[Media: Mathlog_318_b27.pdf|Блок 27]]. Как устроены математические доказательства. Логические исчисления.<br />
<br />
[[Media: Mathlog_318_b28.pdf|Блок 28]]. Натуральное исчисление высказываний: основные определения.<br />
<br />
[[Media: Mathlog_318_b29.pdf|Блок 29]]. Натуральное исчисление высказываний: правило монотонности, закон исключённого третьего, корректность.<br />
<br />
[[Media: Mathlog_318_b30.pdf|Блок 30]]. Натуральное исчисление высказываний: правило сечения, правило полного перебора, правило приведения к абсурду, полнота.<br />
<br />
[[Media: Mathlog_318_b31.pdf|Блок 31]]. Натуральное исчисление предикатов: основные определения, корректность.<br />
<br />
[[Media: Mathlog_318_b32.pdf|Блок 32]]. Гильбертовское исчисление предикатов. Теорема Гёделя о полноте (формулировка).<br />
<br />
[[Media: Mathlog_318_b33.pdf|Блок 33]]. Натуральное исчисление предикатов: полнота.<br />
<br />
[[Media: Mathlog_318_b34.pdf|Блок 34]]. Задачи и проблемы. Алгоритмы. Разрешимость. M-сводимость.<br />
<br />
[[Media: Mathlog_318_b35.pdf|Блок 35]]. Машины Тьюринга (МТ).<br />
<br />
[[Media: Mathlog_318_b36.pdf|Блок 36]]. Теорема Чёрча.<br />
<br />
[[Media: Mathlog_318_b37.pdf|Блок 37]]. Аксиоматические теории первого порядка. Проблема общезначимости формул в теории.<br />
<br />
[[Media: Mathlog_318_b38.pdf|Блок 38]]. Основные свойства аксиоматических теорий.<br />
<br />
[[Media: Mathlog_318_b39.pdf|Блок 39]]. Арифметические интерпретации и теории.<br />
<br />
[[Media: Mathlog_318_b40.pdf|Блок 40]]. Определения и выразимость.<br />
<br />
[[Media: Mathlog_318_b41.pdf|Блок 41]]. Формальная арифметика. Теорема Гёделя о неполноте.<br />
<br />
[[Media: Mathlog_318_b42.pdf|Блок 42]]. Арифметика Пресбургера.<br />
<br />
[[Media: Mathlog_318_b43.pdf|Блок 43]]. Модальные логики.<br />
<br />
[[Media: Mathlog_318_b44.pdf|Блок 44]]. Эпистемические логики.<br />
<br />
[[Media: Mathlog_318_b45.pdf|Блок 45]]. Темпоральные логики.<br />
<br />
[[Media: Mathlog_318_b46.pdf|Блок 46]]. Интуиционистская логика.<br />
<br />
[[Media: Mathlog_318_b47.pdf|Блок 47]]. Формальная верификация.<br />
<br />
[[Media: Mathlog_318_b48.pdf|Блок 48]]. Модельные императивные программы. Постановка задачи верификации программ.<br />
<br />
[[Media: Mathlog_318_b49.pdf|Блок 49]]. Логика Хоара. Автоматизация проверки правильности программ.<br />
<br />
[[Media: Mathlog_318_b50.pdf|Блок 50]]. Проверка правильности распределённых систем. Пара слов о методе model checking.<br />
<br />
[[Media: Mathlog_318_b51.pdf|Блок 51]]. Размеченные системы переходов.<br />
<br />
[[Media: Mathlog_318_b52.pdf|Блок 52]]. Спецификация систем при помощи темпоральных логик.<br />
<br />
[[Media: Mathlog_318_b53.pdf|Блок 53]]. Алгоритм model checking для CTL.<br />
<br />
= Семинары =<br />
<br />
''Материалы семинаров будут обновляться по мере проведения занятий''<br />
<br />
Семинары 1-4 проводятся по [[Media:MatLog_tasks.pdf| этому сборнику задач.]]<br />
<br />
Желающие более глубоко проработать материал первых четырёх семинаров могут обратиться к [[Media:MatLog_exer.pdf| расширенному сборнику задач]]<br />
<br />
[[Media:Mathlog_318_seminar_natural_inference.pdf| Материалы семинара 5-6 (натуральное исчисление).]]<br />
<br />
= Контрольные работы =<br />
<br />
Контрольные работы проводятся письменно, длительность каждой - 90 минут.<br />
<br />
В контрольных работах встретятся 4 типовые задачи со следующими темами:<br />
# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
# Доказать формулу в натуральном исчислении предикатов.<br />
<br />
Оценка решений типовых задач:<br />
* Максимальная оценка - 4 балла.<br />
* Если решение в целом верно, но содержит редкие ошибки серьёзнее опечаток, то оно оценивается в 3 балла.<br />
* Если решение содержит серьёзные ошибки, но имеет структуру, в целом разумно соотносящуюся с правильной, то задача оценивается в 2 балла.<br />
* Если в решении обнаружены правильные элементы, в заметном, но всё же малом количестве, то задача оценивается в 1 балл.<br />
<br />
Теоретические вопросы даются в форме теста с множественным выбором: из предложенных вариантов ответа требуется выбрать правильные (один, несколько или ни одного), обоснование не требуется.<br />
Правильно решённый теоретический вопрос оценивается в 1 балл.<br />
<br />
'''Первая контрольная работа''' будет содержать<br />
* 3 типовые задачи по темам 1-3 и<br />
* 9 теоретических вопросов по прочитанным лекциям.<br />
<br />
'''Вторая контрольная работа''' будет содержать<br />
* 4 типовые задачи по всем темам и<br />
* 5 теоретических вопросов по лекциям, не попавшим в первую контрольную работу.<br />
<br />
'''Остальные контрольные работы''' будут содержать<br />
* 4 типовые задачи по всем темам и<br />
* 14 теоретических вопросов по всем лекциям.<br />
<br />
= Зачёт =<br />
<br />
На зачёте оцениваются результаты, относящиеся к решению типовых задач, знанию теории и работе в семестре.<br />
При проставлении зачёта учитывается 6 технических оценок:<br />
* Четыре оценки за типовые задачи, по одной за каждую задачу.<br />
* Оценка за знание теории. Максимум - 14 баллов.<br />
* Оценка за решение премиальных задач.<br />
<br />
Для получения зачёта требуется получить два результата:<br />
# Набрать хотя бы 11 баллов за типовые задачи.<br />
# Набрать хотя бы 20 баллов суммарно за всё (типовые задачи, теория, премиальные задачи).<br />
<br />
Баллы за типовые задачи и за теорию набираются на [[#Контрольные работы|контрольных работах]].<br />
<br />
Для решения каждой типовой задачи будет предложено несколько попыток.<br />
При проставлении зачёта учитывается '''максимальная''' оценка за задачу среди всех попыток её решить.<br />
<br />
При проставлении зачёта учитывается '''максимальная''' оценка за теорию среди полученных<br />
* суммарно за первые две контрольные работы и<br />
* за каждую из следующих контрольных работ.<br />
<br />
= Экзамен =<br />
<br />
Формат проведения и длительность экзамена: письменно, 120 минут.<br />
<br />
Экзаменационная работа содержит 10 задач и оценивается по шкале от 0 до 37 технических баллов.<br />
К этим техническим баллам прибавляются баллы за выполнение премиальных задач и поощрение/штраф за [[#Контрольная работа|контрольную работу]].<br />
Согласно набранной сумме технических баллов выставляется оценка:<br />
* хотя бы 30: '''отлично''';<br />
* хотя бы 23, но менее 30: '''хорошо''';<br />
* хотя бы 16, но менее 23: '''удовлетворительно''';<br />
* менее 16: '''неудовлетворительно'''.<br />
<br />
Баллы за экзаменационную работу складываются из баллов за каждую задачу, предложенную в работе:<br />
* Каждая из задач 1-4 оценивается в 4 балла. Темы задач:<br />
*# Формализовать в логике предикатов предложение, записанное на естественном языке.<br />
*# Обосновать общезначимость формулы логики предикатов методом семантических таблиц.<br />
*# Обосновать общезначимость формулы логики предикатов методом резолюций.<br />
*# Доказать формулу в натуральном исчислении предикатов.<br />
* Каждая из задач 5-7 оценивается в 3 балла и состоит из трёх частей:<br />
*# Сформулировать утверждение, определение и т.п.<br />
*# Ответить на вопрос "на понимание", так или иначе связанный с формулировкой.<br />
*# Аргументировать (обосновать) ответ на вопрос.<br />
* Каждая из задач 8-10 оценивается в 4 балла и устроена так:<br />
** Из нескольких предложенных вариантов ответа выбрать правильные (один, несколько или ни одного) и '''обосновать''' выбранные ответы.<br />
** Невыбранные ответы обосновывать не нужно.<br />
<br />
== Контрольная работа ==<br />
<br />
На оценку за экзамен влияет первая [[#Контрольные работы|контрольная работа]].<br />
Максимальная техническая оценка за эту работу - 21 балл.<br />
В зависимости от технических баллов, набранных за первую контрольную работу, определяется поощрение или штраф к техническим баллам за экзамен:<br />
* Набрано хотя бы 19 баллов: бонус <span style="background:#DDFFDD">+3 балла</span>;<br />
* Набрано хотя бы 16, но менее 19 баллов: бонус <span style="background:#DDFFDD">+2 балла</span>;<br />
* Набрано хотя бы 13, но менее 16 баллов: бонус <span style="background:#DDFFDD">+1 балл</span>;<br />
* Набрано хотя бы 10, но менее 13 баллов: <span style="background:#CCCCCC">0 баллов</span>;<br />
* Набрано хотя бы 7, но менее 10 баллов: штраф <span style="background:#FFDDDD">-1 балл</span>;<br />
* Набрано хотя бы 4, но менее 7 баллов: штраф <span style="background:#FFDDDD">-2 балла</span>;<br />
* Набрано менее 4 баллов: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка без уважительной причины: штраф <span style="background:#FFDDDD">-3 балла</span>;<br />
* Неявка по уважительной причине: <span style="background:#CCCCCC">0 баллов</span>.<br />
<br />
= Премиальные задачи =<br />
<br />
Общие условия сдачи решений премиальных задач:<br />
* Можно как прислать письменное решение, так и обсудить решение устно. Если прислано письменное решение и к нему есть вопросы, то для ответов на эти вопросы может потребоваться дополнительное устное обсуждение. <br />
* При подготовке решения и во время его сдачи можно пользоваться любыми материалами.<br />
* При сдаче может быть проверено понимание '''каждой''' детали предложенного решения - следует быть к этому готовым.<br />
* Решение принимается, когда по нему не остаётся неотвеченных вопросов.<br />
<br />
'''Бонусы за решение задач формулируются для одной учебной группы''' и распределяются внутри одной группы независимо от другой.<br />
Например, "''первый''" трактуется как "''первый в группе 318, а также первый в группе 319/2, а также ...''".<br />
<br />
Условия задач и статистика принятых решений будут обновляться и доводиться до слушателей по мере чтения курса.<br />
<br />
= Программа курса =<br />
<br />
''Программа будет обновляться согласно фактически прочитанному материалу''<br />
<br />
== Классические логики ==<br />
<ol><br />
<li> Логика высказываний: синтаксис, семантика; выполнимость и общезначимость формул. Проблема общезначимости формул логики высказываний.<br />
<li> Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.<br />
<li> Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).<br />
<li> Выполнимость и общезначимость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.<br />
<li> Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.<br />
<li> Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теоремы о корректности и полноте табличного вывода.<br />
<li> Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева.<br />
<li> Машины Тьюринга. Теорема Чёрча.<br />
<li> Равносильные формулы. Теорема о равносильной замене.<br />
</ol><br />
<br />
== Метод резолюций в логике предикатов ==<br />
<ol start="10"><br />
<li> Предварённая нормальная форма. Теорема о предварённой нормальной форме.<br />
<li> Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.<br />
<li> Дизъюнкты. Сведение проблемы общезначимости формул к проблеме невыполнимости систем дизъюнктов.<br />
<li> Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.<br />
<li> Лемма о связке. Алгоритм унификации. Теорема об унификации.<br />
<li> Правило резолюции. Правило склейки. Резолютивный вывод. Теорема о корректности резолютивного вывода.<br />
<li> Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.<br />
<li> Лемма об основных дизъюнктах. Лемма о подъёме. Теорема о полноте резолютивного вывода.<br />
<li> Метод резолюций: общая схема, применение.<br />
</ol><br />
<br />
== Логические исчисления ==<br />
<ol start="19"><br />
<li> Логические исчисления. Исчисления высказываний и исчисления предикатов. Выводимость и доказуемость формул.<br />
<li> Натуральное исчисление высказываний. Правило монотонности. Закон исключённого третьего. Правило сечения. Правило полного перебора. Правило приведения к абсурду. Корректность и полнота исчисления.<br />
<li> Натуральное исчисление предикатов. Корректность и полнота исчисления.<br />
<li> Исчисление предикатов гильбертовского типа. Теорема Гёделя о полноте (формулировка).<br />
</ol><br />
<br />
== Аксиоматические теории ==<br />
<ol start="23"><br />
<li> Аксиоматические теории первого порядка: основные определения, проблема общезначимости формул в теории.<br />
<li> Основные свойства аксиоматических теорий: непротиворечивость, элементарность, полнота, разрешимость.<br />
<li> Определения и выразимость в интерпретациях. Теорема о подстановке определения.<br />
<li> Формальная арифметика. Теорема Гёделя о неполноте (формулировка и схема доказательства).<br />
<li> Арифметика Пресбургера, её разрешимость и выразительность.<br />
</ol><br />
<br />
== Неклассические прикладные логики ==<br />
<ol start="28"><br />
<li> Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики. Логика линейного времени. Логика деревьев вычислений.<br />
<li> Интуиционистская логика.<br />
<li> Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Полная и частичная корректность программ. Тройки Хоара. Логика Хоара. Корректность вывода в логике Хоара. Слабейшее предусловие. Инвариант цикла.<br />
<li> Размеченные системы переходов. Моделирование программ системами переходов. Логика деревьев вычислений (CTL): синтаксис, семантика, основные равносильности, применение для спецификации поведения распределённых систем. Задача проверки моделей (model checking) относительно CTL: формулировка, решающий алгоритм.<br />
</ol><br />
<br />
= Рекомендованная литература =<br />
<br />
== Основная литература ==<br />
# Клини С. Математическая логика. М.:Мир, 1973, 480 с.<br />
# Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.<br />
# Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.<br />
# Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.<br />
# Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.<br />
# Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.<br />
# Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.<br />
<br />
== Дополнительная литература ==<br />
<br />
# Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.<br />
# Верещагин Н.К., Шень А. Языки и исчисления. 2004.<br />
# Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.<br />
# Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.<br />
# Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.<br />
# Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.<br />
# Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.<br />
# Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.<br />
# Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.<br />
# Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.<br />
# Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.<br />
# Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.<br />
# Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b21.pdfФайл:Mathlog 318 b21.pdf2024-03-10T12:26:01Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b21.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 21. Резолютивный вывод и его корректность</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b20.pdfФайл:Mathlog 318 b20.pdf2024-03-10T12:25:52Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b20.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 19. Алгоритм унификации атомарных формул</div>PodymovVV//mk.cs.msu.ru/index.php/%D0%A4%D0%B0%D0%B9%D0%BB:Mathlog_318_b18.pdfФайл:Mathlog 318 b18.pdf2024-03-10T11:47:36Z<p>PodymovVV: PodymovVV загружена новая версия «Файл:Mathlog 318 b18.pdf»</p>
<hr />
<div>Математическая логика для 318, блок 18. Системы дизъюнктов</div>PodymovVV