你将学到什么
формализовывать инженерные проблемы
получать корректные следствия из установленных фактов
формально представлять и преобразовывать информацию об окружающем мире
проверять эквивалентность высказываний
课程概况
Современная математическая логика – обширная, сложная и разнообразная область знаний. Мы рассмотрим в курсе самую простую ее часть – логику высказываний. Методы, приемы решения задач логики высказываний составляют базис всей математической логики. На примере этой логики мы познакомим вас с основными задачами математической логики: проверка истинности высказывания при конкретных значениях переменных, эквивалентность двух высказываний, проверка на логическое следствие. Для твердого математического фундамента в курсе изучается математическая модель логики высказываний – двоичные функции, операции с ними, канонические формы, минимизация двоичных функций, их эффективное представление при программировании. Также в курсе затрагиваются вопросы формализации высказываний на естественном языке.
Применение логики высказываний продемонстрируем на задаче программирования в логических ограничениях. К широко известным примерам таких задач относится задача Эйнштейна: “В пяти домах живет пять человек разной национальности…” Эти задачи, например, входят в состав алгоритмов работы интеллектуальных агентов.
Наш курс отражает инженерный, политехнический подход. Это означает, что курс насыщен различными примерами из жизни, прикладными задачами, практическими случаями использования математической логики. Если вы хотите повысить свою квалификацию как программиста, инженера, политехника, наш курс – для вас.
课程大纲
Введение
Цель этого модуля - ознакомительная. Мы определяем здесь предмет курса - математическую логику, а также разбираем его структуру. Кроме того, в модуле разбираются задачи, которые вы сможете решать при помощи знаний, полученных в ходе обучения.
Булевы функции
Основная задача этого модуля - заложить математический фундамент для изучения математической логики. Для этого мы познакомимся с основной математической моделью, на которой строится логика высказываний - двоичной функцией. В данном курсе термины булева функция, двоичная функция, логическая функция используются как эквивалентные. В этом разделе рассматриваются две формы представления двоичных функций - в виде таблицы истинности и в виде формулы. А также решается задача построения алгоритма для перехода из одной формы в другую и обратно.
Нормальные формы представления булевых функций
Нормальная форма представления функции - это форма представления, фиксированная некоторым образом. Среди нормальных форм выделяются канонические формы. Представление функции в канонических формах единственно с точностью до порядка переменных, т. е. если зафиксировать порядок переменных, то представление будет единственным. Канонические формы позволяют эффективно решать задачу сравнения функций: не нужно сравнить функции по значениям, достаточно сравнить их представление. В модуле рассматриваются следующие нормальные формы представления двоичных функций: таблица истинности, дизъюнктивная нормальная форма (ДНФ), совершенная дизъюнктивная (СДНФ), конъюнктивная нормальная форма (КНФ), совершенная конъюнктивная (СКНФ), полином Жегалкина. Также решается задача перехода между разными формами представления. Во второй части модуля рассматривается задача, которая была особо актуальна при разработке аппаратных схем, - задача минимизации двоичных функций. Мы рассматриваем решение этой задачи с помощью карт Карно. В последней части рассматриваются несколько примеров реализации двоичных функций при решении практических задач.
Бинарные решающие диаграммы
В этом модуле рассмотрим еще одну каноническую форму представления двоичных функций - бинарные решающие диаграммы (BDD). Эту форму отличает компактное представление для многих практических задач, т. е. для них размер BDD полиномиален от числа переменных. Компактность этой формы позволяет решать многие практические задачи, определяемые через двоичные функции.
Основные понятия логики высказываний
Логика высказываний очень проста. Она выбирает в этом мире только высказывания, на которые можно ответить да или нет, и умеет их соединять самыми простыми связками. Получаемые высказывания снова отвечают на вопрос да или нет. Высказывание "Меня зовут Ирина?" является высказыванием этой логики, оно истинно или ложно, в зависимости от того, кто задает этот вопрос. А вот высказывание "Ирина" не относится к логике высказываний (оно не ставит вопроса с ответом да или нет). В этом модуле мы рассмотрим основные понятия логики высказываний: синтаксис языка этой логики, т.е. правила, определяющие, какие формулы относятся к формулам логики высказываний, семантику языка, т.е. математическую модель, на которой оценивается истинность формулы высказываний (это будут двоичные функции). Много внимания мы уделим тому, как перейти от высказывания на естественном языке к формуле логики высказываний и обратно - навык чрезвычайно полезный не только в профессии, но и в быту. Рассмотрим классические задачи логики: проверку выполнимости формулы на заданном наборе значений переменных, проверку эквивалентности двух формул. В конце этого модуля мы обратимся к наиболее простым приемам эквивалентного переформулирования утверждений математических теорем для упрощения структуры доказательства.
Логическое следствие и логический вывод в логике высказываний
Понятие логического следствия - особое понятие математической логики. Во-первых, оно отражает хорошо известную человечеству причинно-следственную зависимость между высказываниями. А потому прикладное значение этого понятия огромно. Удивительно, еще в начале прошлого века велись дискуссии о разнице понимания причины и следствия в математике и в быту. В модуле мы затронем эту проблему. Сейчас все выглядит решенным: современное понимание причинно-следственной связи ближе к математическому понятию. Во-вторых, задача определения, является ли высказывание логическим следствием множества высказываний - классическая задача математики. В-третьих, только в математической логике этой задаче посвящается столько усилий, только математическая логика столько "знает" об этой задаче - остальная часть математики и человечества пользуется её результатами. Чтобы продемонстрировать теоретические результаты, в модуле будут рассмотрены занимательные задачи и инженерные примеры.
Методы проверки выполнимости логических формул
Задачи математической логики - проверку эквивалентности высказываний, проверку логического следствия - можно свести к задаче проверки выполнимости логических формул. В модуле мы рассмотрим два метода соответствующих метода: метод резолюции, который очень близок к естественному выводу, который мы используем при обосновании своей позиции, и метод DPLL. В конце обсудим ограничения применения логики при решении практических задач.
