Алгебра высказываний - 2#
Нормальные формы#
Нормальные формы в алгебре логики - это формулы специального вида. Любую булеву функцию всегда можно записать в нормальной форме, что упрощает обработку формул. Так, ДНФ (дизъюнктивная нормальная форма) удобно упрощается и минимизируется, КНФ (конъюнктивная нормальная форма) удобна для автоматизированного решения проблемы выполнимости. А совершенные формы (СДНФ, СКНФ) всегда единственны, поэтому позволяют сравнивать разные булевы функции друг с другом.
Понятия нормальных форм#
Определение. Литера - это формула, состоящая из булевой переменной или ее отрицания.
Определение. Дизъюнкт (элементарная дизъюнкция) - это одна или более литер, соединенных операцией дизъюнкции \(\vee\).
Определение. Конъюнкт (элементарная конъюнкция) - это одна или более литер, соединенных операцией конъюнкции \(\&\).
Определение. Конъюнктивная нормальная форма (КНФ) - это один или более дизъюнктов, соединенных операцией конъюнкции.
Определение. Дизъюнктивная нормальная форма (ДНФ) - это один или более конъюнктов, соединенных операцией дизъюнкции.
В дизъюнктивной форме корневая операция - дизъюнкция. В конъюнктивной форме корневая операция - конъюнкция.
<литера> ::= <переменная> | ¬<переменная>
<дизъюнкт> ::= <литера> | <дизъюнкт> ∨ <литера>
<конъюнкт> ::= <литера> | <конъюнкт> & <литера>
<КНФ> ::= (<дизъюнкт>) | <КНФ> & (<дизъюнкт>)
<ДНФ> ::= <конъюнкт> | <ДНФ> ∨ <конъюнкт>
Приведение формулы к КНФ#
Представим алгоритм приведения любой формулы алгебры логики к КНФ.
Дано: формула \(A\).
Построить: формула \(A'\) в КНФ, такая, что \(A' \equiv A\).
Согласно определению формулы алгебры логики, формула \(A\) получена в результате применения одного из трех правил:
\(A\) - булева переменная
В этом случае формула уже в КНФ, \(A' = A\).
\(A = \neg B\), где \(B\) - формула алгебры логики.
В этом случае формулу \(B\) нужно привести к ДНФ - формуле \(B'\). А затем применить закон де Моргана к формуле \(\neg B'\) - получится формула \(A'\), находящаяся в КНФ, причем \(A' \equiv A\).
\(A = (A_1 \,\&\, A_2)\) или \(A = (A_1 \vee A_2)\) или \(A = (A_1 \to A_2)\).
а) Если \(A = (A_1 \,\&\, A_2)\), то достаточно привести формулу \(A_1\) к КНФ \(A_1'\) и формулу \(A_2\) к КНФ \(A_2'\) - получится формула \(A' = (A_1' \,\&\, A_2')\), находящаяся в КНФ и равносильная формуле \(A\).
б) Если \(A = (A_1 \vee A_2)\), то нужно привести формулу \(A_1\) к КНФ \(A_1'\), формулу \(A_2\) к КНФ \(A_2'\), а затем применить второй закон дистрибутивности, чтобы вывести КНФ формулы \(A' = A_1 \vee A_2\).
Например, \(A_1' = (x \vee y) \,\&\, z\), \(A_2' = (\neg x \vee z) \,\&\, (y \vee \neg z)\). Тогда \(A' = \left( (x \vee y) \,\&\, z \right) \vee \left( (\neg x \vee z) \,\&\, (y \vee \neg z) \right) = \)
\( = (x \vee y \vee \neg x \vee z) \,\&\, (x \vee y \vee y \vee \neg z) \,\&\, (z \vee \neg x \vee z) \,\&\, (z \vee y \vee \neg z). \)
в) Если \(A = (A_1 \to A_2)\), то формулу \(A_1\) нужно привести к ДНФ \(A_1'\), а формулу \(A_2\) к КНФ \(A_2'\), после чего применить закон дистрибутивности к формуле \((\neg A_1' \vee A_2')\) так же, как в случае б).
Описанный алгоритм выглядит громоздко для ручного использования, зато он поддаётся автоматизации, поскольку чётко опирается на рекурсивную структуру формул.
Пример. Приведем формулу к КНФ:
\( ((x \to y) \to (z \to \neg x)) \to (\neg y \to \neg z). \)
Сначала необходимо привести эту формулу к формуле с тесными отрицаниями (в которой отрицания относятся только к переменным).
Применяем формулу замены импликации: \( ((x \to y) \to (z \to \neg x)) \to (\neg y \to \neg z) = \)
\( = ((\neg x \vee y) \to (\neg z \vee \neg x)) \to (y \vee \neg z) = \)
\( = \neg(\neg (\neg x \vee y) \vee (\neg z \vee \neg x)) \vee (y \vee \neg z). \)
Применяем закон де Моргана:
\( \ldots = (\neg\neg (\neg x \vee y) \,\&\, \neg(\neg z \vee \neg x)) \vee (y \vee \neg z) = \)
\( = ( (\neg x \vee y) \,\&\, (z \,\&\, x)) \vee (y \vee \neg z). \)
Уберём лишние скобки:
\( \ldots = (\neg x \vee y) \,\&\,z \,\&\, x \vee y \vee \neg z. \)
Полученную формулу с тесными отрицаниями нужно привести к КНФ.
Имея в виду аналогию между логическими и арифметическими операциями, перепишем эту формулу в алгебраической форме:
\( (\neg x \cdot y + z + x) \cdot y \cdot \neg z. \)
Раскроем скобки:
\( (\neg x \cdot y + z + x) \cdot y \cdot \neg z = \)
\( = (\neg x \cdot y \cdot y \cdot \neg z) + (z \cdot y \cdot \neg z) + (x \cdot y \cdot \neg z). \)
Вернёмся к логической символике:
\( (\neg x \vee y \vee y \vee \neg z) \,\&\, (z \vee y \vee \neg z) \,\&\, (x \vee y \vee \neg z). \)
По закону идемпотентности \(y \vee y = y\).
По закону исключенного третьего \(z \vee \neg z = 1\), а по закону единицы \(y \vee 1 = 1\).
Получаем КНФ:
\( (\neg x \vee y \vee \neg z) \,\&\, (x \vee y \vee \neg z). \)
Приведение формулы к ДНФ#
На практике удобно пользоваться аналогией между логическими операциями \(\&\) и \(\vee\) с одной стороны и арифметическими операциями \(\cdot\) и \(+\) с другой, так как равносильность
\( A \,\&\, (B \vee C) = A \,\&\, B \vee A \,\&\, C \)
напоминает тождество
\( A \cdot (B + C) = A \cdot B + A \cdot C. \)
Пример. Приведем формулу из предыдущего примера к ДНФ.
Первый шаг такой же - привести формулу к формуле с тесными отрицаниями:
\( (\neg x \vee y) \,\&\,z \,\&\, x \vee y \vee \neg z \)
Остается раскрыть скобки по первому закону дистрибутивности.
\( (\neg x \vee y) \,\&\,z \,\&\, x \vee y \vee \neg z = \)
\( = \neg x \,\&\, z \,\&\, x \vee y \,\&\, z \,\&\, x \vee y \vee \neg z. \)
Первый конъюнкт равен \(0\) по закону противоречия \(x \,\&\, \neg x = 0\).
Получаем ДНФ:
\( y \,\&\, z \,\&\, x \vee y \vee \neg z. \)
Программная реализация#
Ознакомьтесь с реализацией алгоритма приведения к КНФ/ДНФ в электронном ресурсе.
Пример вывода программы:
Формула: (((x & z) → y) & (¬y ∨ z))
ДНФ: (¬x & ¬y) ∨ (¬x & z) ∨ (¬z & ¬y) ∨ (¬z & z) ∨ (y & ¬y) ∨ (y & z)
КНФ: (¬x ∨ ¬z ∨ y) & (¬y ∨ z)
Упражнение. Допишите программу для дополнительного упрощения нормальной формы по закону исключенного третьего и законам поглощения.
Совершенные нормальные формы#
Любая формула, находящаяся в ДНФ, с помощью равносильных преобразований приводится к СДНФ.
Любая формула, находящаяся в КНФ, с помощью равносильных преобразований приводится к СКНФ.
Кроме того, существуют алгоритмы построения СДНФ и СКНФ по таблице истинности.
Материалы для самостоятельного изучения
Упражнение. Вам дана программа для построения СДНФ по таблице истинности. Напишите аналогичную программу для построения СКНФ.
Выполнимость логических формул#
Определение. Множество формул \(\Gamma\) называется выполнимым, если существует такая оценка (набор значений переменных) \(v\), при которой все формулы из \(\Gamma\) принимают значение \(1\).
Оценку \(v\), на которой все формулы из \(\Gamma\) равны \(1\), называется выполняющей оценкой (выполняющим набором) для множества \(\Gamma\).
Буквой $v$ здесь обозначен "словарь", который каждой переменной ставит в соответствие значение $0$ или $1$. Это и есть оценка.Определение. Невыполнимые множества формул называют несовместными.
Определение. Формула \(A\) называется выполнимой, если выполнимо множество \(\{A\}\).
Пример. Множество формул \(\{\neg x, x \,\&\, y\}\) несовместно. Всякий раз, когда первая формула равна \(1\), вторая обращается в \(0\).
Пример. Множество формул \(\{x \vee y, \; \neg y \to z, \; z \leftrightarrow x\}\) выполнимо. Выполняющая оценка: \(x = 1, \, y = 1, \, z = 1\).
Критерий несовместности множества \(\Gamma = \{A_1, A_2, \ldots, A_n\}\):
\( \Gamma \text{ - несовместно} \;\;\Longleftrightarrow \;\; A_1 \,\&\, A_2\,\&\, \ldots \,\&\, A_n \equiv 0. \)
Пример. Множество \(\{x, \; x \to y, \; \neg y\}\) несовместно, так как
\( x \,\&\, (x \to y) \,\&\, \neg y = x \,\&\, (\neg x \vee y) \,\&\, \neg y = 0. \)
Упражнение. Докажите, что если множество формул \(\Gamma\) несовместно, то любое его расширение, т.е. множество формул \(\Delta\) такое, что \(\Gamma \subset \Delta\), также несовместно.
Логическое следствие#
Понятие логического следствия#
Пример. Даны два высказывания, выделяющие “истинные” ситуации \(x, y, z\), где \(x = \) “человек ошибается”, \(y = \) “человек работает”, \(z = \) “человек ест”:
Не ошибается только тот, кто ничего не делает: \(\neg x \to \neg y\).
Кто не работает, тот не ест: \(\neg y \to \neg z\).
Укажем с помощью таблицы истинности, в каких ситуациях оба высказывания истинны.
\(F_1\) |
\(F_2\) |
||||
|---|---|---|---|---|---|
\(x\) |
\(y\) |
\(z\) |
\(\neg x \to \neg y\) |
\(\neg y \to \neg z\) |
\(F_1 \,\&\, F_2\) |
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
Подумаем, какая формула описывает все “истинные” ситуации.
Во-первых, по таблице истинности \(F_1 \,\&\, F_2\) можно построить формулу - она в точности опишет все “истинные” ситуации.
Во-вторых, чтобы описать “истинные” ситуации с помощью простой формулы, мы можем порассуждать, каким общим свойством обладают все “истинные” ситуации. Иначе говоря, попробуем вывести логическое следствие из наших гипотез.
Итак, рассуждаем. Формула \(\neg x \to \neg y\) сообщает, что ложность \(x\) всегда гарантирует ложность \(y\) (то есть ситуация, когда \(x = 0\) и \(y = 1\), у нас исключается). Вторая формула \(\neg y \to \neg z\), с другой стороны, гарантирует, что при ложном \(y\) ложно и \(z\). Объединяя наши рассуждения, получим, что при ложном \(x\) ложно \(z\).
Следовательно, при истинных гипотезах \(\neg x \to \neg y\) и \(\neg y \to \neg z\) истинна формула \(\neg x \to \neg z\). По закону контрапозиции \(\neg x \to \neg z = z \to x\). Теперь мы можем сформулировать логическое следствие:
\( \neg x \to \neg y,\;\; \neg y \to \neg z \; \models \; z \to x \)
Путем рассуждений мы установили, что все ситуации, когда \(F_1 \,\&\, F_2 = 1\), должны удовлетворять формуле \(z \to x\).
Построим таблицу истинности, чтобы проверить выкладки.
\(x\) |
\(y\) |
\(z\) |
\(F_1 \,\&\, F_2\) |
\(z \to x\) |
|---|---|---|---|---|
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
\(1\) |
Мы подтвердили, что во всех ситуациях, когда истинны обе гипотезы \(F_1, F_2\), истинна и формула \(z \to x\). Но это не значит, что \(F_1 \,\&\, F_2 = z \to x\).
Логическое следствие \(F_1,\; F_2 \models z \to x\) означает тождественную истинность импликации \(F_1 \,\&\, F_2 \to (z \to x)\). Поговорим об этом подробнее в следующем разделе.
Логическое следствие мы привыкли понимать так. Говорят, что утверждение \(A\) вытекает (следует) из утверждений \(A_1, A_2, \ldots, A_n\), если утверждение \(A\) истинно всегда, когда истинны утверждения \(A_1, A_2, \ldots, A_n\).
В математической логике понятие логического следствия уточняется следующим образом.
Определение. Формула алгебры логики \(A\) логически следует из множества формул (гипотез) \(\Gamma = \{A_1, A_2, \ldots, A_n\}\), если \(v(A) = 1\) для любой оценки \(v\), при которой все формулы из \(\Gamma\) принимают значение \(1\).
Обозначение для логического следствия:
\(\Gamma \models A\) или \(A_1, A_2, \ldots, A_n \models A\)
Критерии логического следствия#
Табличный критерий#
Из определения логического следствия вытекает критерий на основе таблицы истинности:
Выделим все строчки таблицы истинности, в которых все гипотезы равны \(1\). Формула \(A\) следует из \(\Gamma\), если во всех выделенных строчках \(A = 1\).
Пример. Спортсмен посещает спорткомплекс (бассейн \(x\), групповые программы \(y\), тренажерный зал \(z\)). Всякий раз, когда он ходит в тренажерный зал, он ходит и в бассейн. Сегодня спортсмен был в тренажерном зале или на групповых программах. Следовательно, спортсмен точно был в бассейне или на групповых программах.
Проверим логическое следствие:
\( z \to x, \;\; z \vee y \; \models \; x \vee y. \)
\(x\) |
\(y\) |
\(z\) |
\(z \to x\) |
\(z \vee y\) |
\(x \vee y\) |
|---|---|---|---|---|---|
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(1\) |
\(0\) |
\(\mathbf{0}\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(1\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(\mathbf{1}\) |
\(1\) |
\(1\) |
\(1\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(1\) |
\(1\) |
\(1\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(1\) |
\(1\) |
\(1\) |
В таблице жирным выделены все оценки, при которых обе гипотезы равны \(1\).
Во всех выделенных строчках следствие \(x \vee y\) также равно \(1\). Логическое следствие доказано.
Пример. Спортсмен посещает спорткомплекс (бассейн \(x\), групповые программы \(y\), тренажерный зал \(z\)). Всякий раз, когда он ходит в тренажерный зал, он ходит и в бассейн. Сегодня спортсмен был в бассейне или на групповых программах. Можно ли сделать вывод, что спортсмен точно был в тренажерном зале или на групповых программах?
Проверим логическое следствие:
\( z \to x, \;\; x \vee y \; \models \; z \vee y. \)
\(x\) |
\(y\) |
\(z\) |
\(z \to x\) |
\(x \vee y\) |
\(z \vee y\) |
|---|---|---|---|---|---|
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(0\) |
\(0\) |
\(1\) |
\(0\) |
\(0\) |
\(1\) |
\(\mathbf{0}\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(1\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(0\) |
\(1\) |
\(1\) |
\(\color{Red}\mathbf{1}\) |
\(\color{Red}\mathbf{0}\) |
\(\color{Red}\mathbf{0}\) |
\(\color{Red} 1\) |
\(\color{Red} 1\) |
\(\color{Red} 0\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(\mathbf{1}\) |
\(1\) |
\(1\) |
\(1\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(\mathbf{0}\) |
\(1\) |
\(1\) |
\(1\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(\mathbf{1}\) |
\(1\) |
\(1\) |
\(1\) |
В таблице жирным выделены все оценки, при которых обе гипотезы равны \(1\).
Теперь в таблице виден контрпример: в красной строчке обе посылки равны \(1\), а следствие равно \(0\). Существование хотя бы одного контрпримера сразу опровергает логическое следствие. Значит, логического следствия нет:
\( z \to x, \;\; x \vee y \; \nvDash \; z \vee y. \)
Таким образом, в ситуации, когда спортсмен пошел только в бассейн (\(x=1,\,y=0,\,z=0\)), все гипотезы выполняются, а следствие не выполняется!
Первый критерий#
Помимо табличного критерия, имеется первый критерий логического следствия - тождественная истинность импликации.
Например, \( z \to x, \;\; z \vee y \; \models \; x \vee y \;\; \Longleftrightarrow \)
\( \Longleftrightarrow \;\; (z \to x) \,\&\, (z\vee y) \to (x \vee y). \)
Действительно, логическое следствие \(A_1, A_2, \ldots, A_n \models A\) означает, что для любой оценки, если истинны все гипотезы, то истинно и следствие \(A\):
\( A_1, A_2, \ldots, A_n \models A \;\; \Longleftrightarrow \;\; \left(A_1 \,\&\, A_2 \,\&\, \ldots \,\&\, A_n \to A\right) \equiv 1. \)
Любой контрпример сразу обнуляет выражение \(\left(A_1 \,\&\, A_2 \,\&\, \ldots \,\&\, A_n \to A\right)\).
Второй критерий#
Второй критерий логического следствия - проверка несовместности гипотез с отрицанием следствия.
Например, чтобы проверить логическое следствие
\( z \to x, \;\; x \vee y \; \models \; z \vee y, \)
напишем условие, которому подчиняются все контрпример - гипотезы истинны, следствие ложно:
\( (z \to x) \,\&\, (x \vee y) \,\&\, \neg (z \vee y). \)
Логическое следствие имеет место, если это выражение никогда не равно \(1\):
\( z \to x, \;\; x \vee y \; \models \; z \vee y \;\; \Longleftrightarrow \)
\( \Longleftrightarrow \;\; (z \to x) \,\&\, (x \vee y) \,\&\, \neg (z \vee y) \equiv 0. \)
Действительно, из формул \(A_1, A_2, \ldots, A_n\) логически следует формула \(A\) тогда и только тогда, когда множество формул \(\{A_1, A_2, \ldots, A_n, \neg A\}\) несовместно. Критерий несовместности - противоречивость конъюнкции:
\( A_1 \,\&\, A_2 \,\&\, \ldots \,\&\, A_n \,\&\, \neg A \equiv 0. \)
Слева от знака \(\equiv\) записано условие нарушения логического следствия. Противоречивость (\(\equiv 0\)) означает, что это условие никогда не выполняется: логическое следствие нарушить никак нельзя.
Упражнение. Пользуясь формулой для отрицания импликации, выведите второй критерий из первого.
Метод от противного#
Вернёмся к примерам со спортсменом.
Пример. Проверим логическое следствие:
\( z \to x, \;\; z \vee y \; \models \; x \vee y. \)
Все контрпримеры (значения \(x,y,z\), при которых гипотезы истинны, а следствие ложно) удовлетворяют системе логических уравнений:
\( \left\{\begin{aligned} z \to x &= 1,\\ z \vee y &= 1, \\ x \vee y &= 0. \end{aligned}\right. \)
Давайте найдём все контрпримеры (или докажем, что их нет).
Поскольку дизъюнкция равна \(0\), только когда оба операнда равны \(0\), то из третьего уравнения выводим \(x = 0, \, y = 0\).
Подставляя найденные значения в первые два уравнения, приходим к системе
\( \left\{\begin{aligned} z \to 0 &= 1,\\ z \vee 0 &= 1. \end{aligned}\right. \)
Отсюда, поскольку \(z \to 0 = \neg z\) и \(z \vee 0 = z\), получаем
\( \left\{\begin{aligned} \neg z &= 1,\\ z &= 1. \end{aligned}\right. \)
Система уравнений противоречива. Значит, решений системы нет. И контрпримеров к логическому следствию тоже нет.
Вывод: логическое следствие нельзя нарушить \(\Rightarrow\) логическое следствие выполнено.
Пример. Проверим логическое следствие:
\( z \to x, \;\; x \vee y \; \models \; z \vee y. \)
Точно так же составляем систему логических уравнений, приравнивая гипотезы к \(1\), а следствие к \(0\):
\( \left\{\begin{aligned} z \to x &= 1,\\ x \vee y &= 1, \\ z \vee y &= 0. \end{aligned}\right. \)
Из третьего уравнения \(z = 0\), \(y = 0\). Тогда все контрпримеры обязаны удовлетворять системе
\( \left\{\begin{aligned} 0 \to x &= 1,\\ x \vee 0 &= 1. \end{aligned}\right. \)
Первое уравнение выполнено при любом \(x\). А из второго уравнения находим \(x = 1\).
Итак, мы нашли контрпример: \(x=1,\,y=0,\,z=0\). Логическое следствие нарушается.
Программная реализация#
В электронном ресурсе доступна программа для проверки логического следствия \(A_1, A_2, \ldots, A_n \models A\).
Реализован парсер логических формул.
Программа читает из файла несколько формул - гипотезы и следствие.
Пример входного файла:
x -> ~y
y
~x
Пример вывода:
Гипотезы:
(x → ¬y)
y
Следствие:
¬x
Критерий логического следствия:
(((x → ¬y) & y) → ¬x)
Таблица истинности:
(0, 0) -> 1
(0, 1) -> 1
(1, 0) -> 1
(1, 1) -> 1
Упражнение. Реализуйте вывод подробной таблицы истинности (столбцы для всех гипотез \(A_1, A_2, \ldots, A_n\), следствия \(A\) и импликации \(A_1 \,\&\, A_2 \,\&\, \ldots \,\&\, A_n \to A\)) и списка всех контрпримеров к логическому следствию.
Метод резолюций#
Как быстро проверить логическое следствие, включающее много формул?
Как найти выполняющий набор для формулы алгебры логики или установить, что формула невыполнима?
Как решить эти вопросы для очень больших задач с помощью компьютера?
На помощь приходит метод резолюций.
Типичный пример применения метода резолюций: представьте, что у вас есть база знаний, записанная в форме дизъюнктов (логики высказываний или логики предикатов). Вы хотите узнать, будет ли заданная формула истинной, когда истинны все допущения базы знаний. Другими словами, вы делаете запрос к базе знаний и хотите выяснить истинность следствия.
Например, вы знаете, что:
если не сдать логику (\(\neg x)\), сессия не будет закрыта (\(\neg y)\);
если не закрыть сессию (\(\neg y\)), не будет стипендии (\(\neg z\)).
Вы почти уверены, но хотите уточнить: правда ли, что стипендия будет только в том случае, если сдашь логику (\(z \to x\))?
База знаний: \(\neg x \to \neg y,\; \neg y \to \neg z\).
Запрос: \(\;?\, z \to x\).
Решение:
Компьютер берёт отрицание вашего запроса и добавляет его в базу знаний, а затем проверяет, что полученное множество формул несовместно.
Чтобы быстро проверить несовместность формул, алгоритм пытается вывести противоречие (тождественный \(0\)) из множества дизъюнктов с помощью правила резолюции.
Если противоречие удается вывести - значит, множество формул несовместно.
Если противоречие никак не выводится - значит, множество формул выполнимо, и с помощью метода резолюций можно даже подобрать выполняющую оценку.
Правило резолюции#
Правило резолюции - это вот такое логическое следствие (здесь \(A\), \(B\), \(C\) - любые формулы):
\( \dfrac{A \vee B, \;\; \neg A \vee C}{B \vee C} \)
Пример. Придадим буквам смысл:
\(A = \) “прогулял пару”
\(B = \) “слушаю лекцию”
\(C = \) “сплю”
Формулы над чертой - это наши гипотезы, их мы считаем истинными.
То есть, с одной стороны, из формулы \(A \vee B\) не может быть, что я одновременно не прогулял пару и не слушаю лекцию. С другой стороны, из формулы \(A \vee C\) не может быть, что я одновременно прогулял пару и не сплю.
Согласно правилу резолюции, я делаю вывод: или я слушаю лекцию, или сплю (или и то, и другое одновременно).
Упражнение. Обоснуйте правило резолюции: а) с помощью компьютерной программы проверки логического следствия; б) методом от противного.
Проверка логического следствия#
Так как метод резолюций применяется к дизъюнктам, для проверки выполнимости булевой формулы следует привести формулу к КНФ.
Пример. Проверим логическое следствие:
\( z \to x, \;\; z \vee y \; \models \; x \vee y. \)
Согласно второму критерию логического следствия, нужно проверить несовместность множества формул
\( z \to x, \; z \vee y, \; \neg(x \vee y), \)
то есть тождественную ложность их конъюнкции:
\( (z \to x)\,\&\, (z \vee y)\,\&\, \neg(x \vee y) \equiv 0. \)
Приводим эту формулу к КНФ:
\( (z \to x)\,\&\, (z \vee y)\,\&\, \neg(x \vee y) = \)
\( = (\neg z \vee x)\,\&\, (z \vee y)\,\&\, \neg x \,\&\, \neg y. \)
Перечисляем все дизъюнкты:
\( \neg z \vee x, \;z \vee y,\; \neg x,\; \neg y. \)
Нам осталось вооружиться правилом резолюции, чтобы вывести \(0\).
Первые два дизъюнкта резольвируют. Это значит, что к ним можно применить правило резолюции. Контрарные (противоположные) литеры вычеркиваются, а остатки соединяются.
\( \dfrac{\neg z \vee x,\; z \vee y}{x \vee y} \)
Логическое следствие добавляется в базу знаний:
\( \neg z \vee x,\; z \vee y,\; \neg x,\; \neg y, \; x\vee y. \)
Снова ищем, какие дизъюнкты резольвируют. Теперь это два последних дизъюнкта. Дизъюнкт \(\neg y\) запишем в виде \(0 \vee \neg y\).
\( \dfrac{0 \vee \neg y, \; x \vee y}{0 \vee x} \)
Логическое следствие: \(x\).
Снова пополняем базу знаний:
\( \neg z \vee x,\; z \vee y,\; \neg x,\; \neg y, \; x\vee y, \; x. \)
Из дизъюнктов \(x\) и \(\neg x\) сразу выводим \(0\).
Итак, формула \((z \to x)\,\&\, (z \vee y)\,\&\, \neg(x \vee y)\) оказалась невыполнимой. А значит, логическое следствие нарушить нельзя. Логическое следствие выполняется.
Пример. Проверим логическое следствие:
\( z \to x, \;\; x \vee y \; \models \; z \vee y. \)
Второй критерий логического следствия:
\( (z \to x) \,\&\, (x \vee y) \,\&\, \neg (z \vee y) \equiv 0. \)
Приводим формулу к КНФ:
\( (\neg z \vee x) \,\&\, (x \vee y) \,\&\, \neg z \,\&\, \neg y. \)
Перечисляем все дизъюнкты:
\( \neg z \vee x, \; x \vee y, \; \neg z, \; \neg y. \)
Применяем правило резолюций:
Из второго и четвертого дизъюнктов выводим \(x\).
Больше ничего вывести не получается.
Чтобы наша КНФ равнялась \(1\), мы выяснили, что должны быть истинными формулы \(x,\, \neg y, \, \neg z\). Поэтому попутно найден контрпример: \(x = 1,\,y = 0, \, z = 0\), опровергающий логическое следствие.
Задачи на метод резолюций#
Задача. Три комнаты: 1, 2, 3. В каждой ровно один обитатель: принцесса, тигр, призрак (все разные, по одному).
Таблички:
Комната 1: «Призрак в комнате 3».
Комната 2: «Принцесса не в комнате 1».
Комната 3: «Тигр в комнате 2».
Правила правдивости:
Если в комнате принцесса, то надпись на её двери истинна.
Если в комнате тигр, то надпись на его двери ложна.
Если в комнате призрак, то надпись может быть любой (нет ограничений).
Цель: определить, кто в какой комнате, используя метод резолюций.
Схема решения. Введем булевы переменные \(P_{i, X}\), где \(i = 1, 2, 3\) - номер комнаты, \(X = P, T, G\) (принцесса, тигр, призрак). То есть всего 9 переменных. Например, \(P_{1, P}\) означает “в комнате 1 - принцесса”.
Запишем ограничения в виде формул алгебры логики.
Сначала скажем, что каждый обитатель находится в одной своей комнате.
\(P_{1,P} \vee P_{2,P} \vee P_{3,P}\)
Для любых \(i, j\), где \(i\neq j\) справедлива формула: \(P_{i, P} \to \neg P_{j, P}\) (если принцесса в \(i\)-й комнате, то в \(j\)-й комнате её нет), или, по формуле замены импликации, \(\neg P_{i, P} \vee \neg P_{j, P}\).
Итак,
\(\neg P_{1, P} \vee \neg P_{2, P}, \; \neg P_{1, P} \vee \neg P_{3, P}, \; \neg P_{2, P} \vee \neg P_{3, P}.\)
Аналогично для \(T\) и \(G\).
Итого мы записали 12 дизъюнктов.
Теперь скажем, что в каждой комнате находится ровно один обитатель.
В первой комнате кто-то есть:
\( P_{1, P} \vee P_{1, T} \vee P_{1, G} \)
Аналогично для второй и третьей комнат.
Также запишем условия, что если в комнате есть кто-то один, то кого-то другого там нет.
Для каждого \(i = 1, 2, 3\):
\( \neg P_{i, P} \vee \neg P_{i, T}, \; \neg P_{i, P} \vee \neg P_{i, G}, \; \neg P_{i, T} \vee \neg P_{i, G}. \)
Итого мы записали ещё 12 дизъюнктов.
Дальше запишем условия на табличках.
Комната 1: «Призрак в комнате 3» \(\Rightarrow \; S_1 = P_{3, G}\)
Комната 2: «Принцесса не в комнате 1» \(\Rightarrow \; S_2 = \neg P_{1, P}\)
Комната 3: «Тигр в комнате 2» \(\Rightarrow \; S_3 = P_{2, T}\)
Правила правдивости:
Если \(P_{i, P}\) (принцесса), то \(S_i\) истинно \(\Rightarrow \; P_{i, P} \to S_i\)
Если \(P_{i, T}\) (тигр), то \(S_i\) ложно \(\Rightarrow \; P_{i, T} \to \neg S_i\)
Итак, дизъюнкты:
(первое правило правдивости)
\(P_{1, P} \to P_{3, G} = \neg P_{1, P} \vee P_{3, G}\)
\(P_{2, P} \to \neg P_{1, P} = \neg P_{2, P} \vee \neg P_{1, P}\)
\(P_{3, P} \to P_{2, T} = \neg P_{3, P} \vee P_{2, T}\)
(второе правило правдивости)
\(P_{1, T} \to \neg P_{3, G} = \neg P_{1, T} \vee \neg P_{3, G}\)
\(P_{2, T} \to P_{1, P} = \neg P_{2, T} \vee P_{1, P}\)
\(P_{3, T} \to \neg P_{2, T} = \neg P_{3, T} \vee \neg P_{2, T}\)
Итого у нас ещё 6 дизъюнктов.
Итак, всего 9 переменных и 30 дизъюнктов.
Нашу КНФ теперь не так сложно ввести в компьютерную программу, которая найдет выполняющий набор значений переменных.
Задача. Классическая “задача Эйнштейна” тоже сводится к задаче выполнимости системы ограничений.
Есть 5 домов в ряд, пронумерованных 1-5 слева направо. В каждом живёт ровно один человек. У каждого человека есть ровно одна характеристика из каждой категории: национальность, цвет дома, напиток, автомобиль, питомец.
И есть набор условий, которые переводятся в логические формулы.
Надо определить, кто держит рыбок.
Для решения этой задачи по методу резолюций перебираем \(i\) от 1 до 5 и добавляем к базе знаний отрицание условия, что “\(i\)-й человек держит рыбок”, и пытаемся вывести противоречие. (То есть проверяем по очереди все возможные логические следствия.)
Задача. Зоологика: закодируйте пример с помощью логических формул и решите методом резолюций.
Упражнение. Вам дана программа, в которой реализован метод резолюций. Решите с помощью этой программы разобранные задачи.
Для быстрого нахождения всех выполняющих наборов можно использовать SAT-солвер pycosat. (Можно обратиться к нейросети, чтобы представить условие задачи в формате, который понимает SAT-солвер, например, DIMACS CNF. Не забывайте, что ответственность за правильность нейросетевого решения лежит на вас! Перепроверяйте!) Ещё вариант (медленнее) - построить таблицу истинности.
Литература#
Крупский, Плиско - Математическая логика и теория алгоритмов