Как найти формулу в алгебре логики

Алгебра высказываний

Формулы алгебры высказываний

Формулы алгебры высказываний состоят из высказываний, соединенных связками.
Каждое высказывание – это повествовательное предложение, о котором в данной ситуации можно сказать,
что оно истинно или ложно, но не то и другое одновременно. В качестве связок используют
операции над высказываниями: конъюнкция, дизъюнкция, отрицание, импликация, эквиваленция.

Синтаксически формула алгебры высказываний – это логическое выражение. Семантически оно задает
булеву функцию $n$ переменных, где $n$ – число простых высказываний, входящих в формулу.
Каждая переменная в формуле может принимать одно из двух значений: истина (1) и ложь (0).
Выражаемая функция на всяком наборе значений переменных также принимает одно из двух значений.
Всего число всех возможных булевых функций от $n$ переменных равно числу способов $n$ раз выбрать
0 или 1. Изобразив дерево полного перебора, увидим, что это полное двоичное дерево высоты $n$,
каждый лист которого соответствует $n$-мерному двоичному вектору. Поэтому всего в нем $2^n$ листьев.
Итак, число всех возможных булевых функций от $n$ переменных равно $2^n$.

Любую булеву функцию можно задать ее таблицей истинности.

Если в формуле не расставлены скобки, операции выполняются в таком порядке: $neg$, $&$, $vee$, $to$.

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

Эквивалентность формул АВ

Формулы $varphi(x_1, x_2, dots, x_n)$ и $psi(x_1, x_2, dots, x_n)$ называются
эквивалентными, если совпадают их таблицы истинности, т.е. на любом наборе значений переменных
$x_1, x_2, dots, x_n$ обе формулы принимают одинаковые значения.

Приведем основные эквивалентности между формулами.

1) $xy = yx$, $x vee y = y vee x$ (коммутативность $&$ и $vee$);

2) $(xy)z = x(yz)$, $(x vee y) vee z = x vee (y vee z)$ (ассоциативность $&$ и $vee$);

3) $x(yvee z) = xy vee xz$ (дистрибутивность $&$ относительно $vee$),
$x vee (y & z) = (x vee y) & (x vee z)$ (дистрибутивность $vee$ относительно $&$);

4) $neg (x & y) = neg x vee neg y$, $neg (x vee y) = neg x & neg y$
(законы двойственности де Моргана);

5) $xy vee x&neg y = x$, $(x vee y)(x vee neg y) = x$ (правила склеивания);

6) $x vee (xy) = x$, $x(x vee y) = x$ (правила поглощения);

7) $(xz) vee (y& neg z) = (xz) vee (y neg z) vee (xy)$ (правило обобщенного склеивания);

$x & x = x$, $x vee x = x$ (законы идемпотентности);

9) $x & 0 = 0$, $x vee 0 = x$, $x & 1 = x$, $x vee 1 = 1$, $(x Rightarrow 0) = overline x$,
$(x Rightarrow 1) = 1$ (свойства относительно констант);

10) $x vee neg x = 1$ (закон исключенного третьего);

11) $x & neg x = 0$ (закон противоречия);

12) $negneg x = x$ (закон двойного отрицания);

13) $x to y = neg x vee y$ (замена импликации);

14) $x vee (neg x & y) = x vee y$, $neg x vee (x & y) = neg x vee y$;

15) $x & (neg x vee y) = x & y$, $neg x & (x vee y) = neg x & y$.

Дизъюнктивные и конъюнктивные нормальные формы АВ

Чтобы определить, равносильны ли формулы (являются ли они тождественными), необходимо привести их
к нормальной форме [Волкова]. В нормальной форме присутствуют только простые логические операции,
и отрицание относится только к элементарным высказываниям.

ДНФ – это дизъюнкция элементарных конъюнкций (конъюнктов), КНФ – это конъюнкция элементарных дизъюнкций (дизъюнктов).
Элементарная дизъюнкция (конъюнкция) – это дизъюнкция (конъюнкция) переменных и их отрицаний, в которую каждая переменная
входит не более одного раза.

Теорема. Для любой формулы $A$ существует равносильная формула $B$, находящаяся в КНФ (ДНФ), и причем не одна.

Чтобы привести формулу к ДНФ, нужно:
1) выразить импликацию по формуле замены импликации, 2) используя законы де Моргана, перенести все отрицания
к переменным и сократить двойные отрицания, 3) используя закон дистрибутивности $&$ относительно $vee$,
преобразовать формулу так, чтобы все конъюнкции выполнялись раньше дизъюнкций.

Совершенные дизъюнктивные и конъюнктивные нормальные формы

В СДНФ (СКНФ) формула приведена к ДНФ (КНФ), и все слагаемые (множители) формулы $A$ попарно различны, причем
каждая переменная входит в каждое слагаемое (множитель) ровно один раз.

Теорема. Каждая не тождественно истинная формула имеет единственную СКНФ.

Теорема. Каждая не тождественно ложная формула имеет единственную СДНФ.

Правило перехода от ДНФ (КНФ) к СДНФ (СКНФ) можно прочитать в [Волкова, с. 11].

Чтобы по таблице истинности записать СДНФ или СКНФ, заметим, что всякий конъюнкт, содержащий все переменные, в котором
каждой 1 соответствует переменная, а 0 – переменная с отрицанием, принимает истинное значение только в одной строчке.
Поэтому дизъюнкция таких конъюнктов по строчкам, в которых функция принимает истинное значение, и даст выражение для
этой функции.

Аналогично строится СКНФ: дизъюнкт, в котором присутствуют переменные с отрицаниями (1 соответствует переменная с отрицанием, 0 – переменная)
будет ложным в этой и только этой строчке. Тогда если мы запишем конъюнкцию таких дизъюнктов по строчкам с 0, то она будет принимать значение “ложь”
во всех этих строчках и “истина” в остальных строчках таблицы истинности.

Для минимизации ДНФ применяют метод Блейка [Волкова], метод Квайна, карты Карно,
а также метод неопределенных коэффициентов [Гринченков, с. 28], который реализуется на ЭВМ. См. [Белоусов, с. 408].

Логическое следствие

Основная задача логики в нахождении общих способов установления связей
логических значений одних высказываний с логическими значениями других высказываний
на основании исследования формальной структуры высказываний.
Это служит средством систематизации знаний. [Игошин, с. 53]

Задача математической логики в вопросах логического следования состоит в том, чтобы
указать такие формы высказываний $A_1, A_2, dots, A_m, B$, когда последнее
высказывание непременно было бы следствием $m$ первых, независимо от конкретного содержания
всех этих высказываний.

Пусть даны формулы $A_1, dots, A_m, B$, которые зависят от переменных $X_1, dots, X_n$.
Формула $B$ называется логическим следствием формул $A_1, dots, A_m$, если, при истинности
одновременно всех формул $A_1, dots, A_m$ истинна и формула $B$ при одних и тех же
значениях переменных $X_1, dots, X_n$. [Волкова]

Для логического следствия используют запись $A_1, dots, A_m models B$ или
$dfrac{A_1,dots,A_m}{B}$, где формулы $A_1,dots,A_m$ – предпосылки,
формула $B$ – заключение.
Логическое следствие проверяют с помощью таблицы истинности [Волкова, с. 27].

Справедлив следующий критерий следования [Волкова, с. 29]: не тождественно истинная
формула $B$ является логическим следствием формул $A_1, dots, A_m$, не все из которых
тождественно истинны, когда все множители формулы $B$, находящейся в СКНФ,
входят в СКНФ формулы $A_1, dots, A_m$.

Чтобы найти все (неравносильные) формулы, являющиеся логическими следствиями из предпосылок
$A_1, dots, A_m$, необходимо выполнить следующие действия:

1) составить конъюнкцию $A_1cdot dotscdot A_m$.

2) найти СКНФ формулы $A_1cdot cdot A_m$;

3) выписать все множители найденной СКНФ, а также всевозможные конъюнкции этих множителей.

Полученные формулы являются логическими следствиями предпосылок $A_1, dots, A_m$.

Теорема (признак логического следствия). [Игошин, с. 56] Формула $G$ будет логическим
следствием формулы $F$ тогда и только тогда, когда формула $F to G$ является тавтологией:
(F models G Leftrightarrow models F to G.)

Замечание. [Игошин, с. 58] Если некоторая формула является тавтологией, то и всякое ее
логическое следствие также является тавтологией:
(models F text{ ;и; } F models G ;Rightarrow; models G.)

Для проверки формул на логическое следование можно использовать метод от противного
[Игошин, с. 59], см. также онлайн-курс на Stepik.

Метод резолюций

Метод резолюций – это правило вывода логических формул, которое применяется для
автоматического доказательства теорем.

Правило резолюции имеет следующий вид [Игошин, с. 60]:
(G vee F, ; H vee neg F ;; models ;; G vee H.)

Нетрудно проверить, что формула $G vee H$ действительно является логическим следствием
двух формул, стоящих слева. При этом говорят, что формула $G vee F$ резольвирует с формулой
$H vee neg F$, формула $G vee H$ называется резольвентой формул $G vee F$ и $H vee neg F$
(по переменной $F$), и пишут $G vee H = {rm Res}_F(G vee F, H vee neg F)$.

Если при этом в условии отсутствует формула $G$ (или она тождественно ложна), то правило
принимает следующий вид:
(F, ; H vee neg F ;; models ;; H,)
представляющий известное правило modus ponens: $F, F to H ; models ; H$.

Если же отсутствует формула $H$, то правило принимает следующий вид:
(G vee F, ; neg F ;; models ;; G.)

Рассмотрим посылки правила резолюции: $G vee F$, $H vee neg F$.
По формуле замены импликации можно представить их в виде $neg G to F$, $Fto H$.
Отсюда по правилу цепного заключения получим $neg G to H$, или $G vee H$.
Итак, мы доказали, что $G vee F, ; H vee neg F ;; models ;; G vee H$,
т.е. правило резолюции.

Метод резолюций, основанный на правиле резолюции,
проверяет формулы алгебры высказываний на логическое следование.
[Игошин, с. 61; Волкова, с. 42]

Перевод с естественного языка на язык математической логики

Перевод высказывания естественного языка в символический вид называется его формализацией.
Формула логики высказываний сама по себе не имеет никакого содержания. В частности, она
не является ни истинной, ни ложной. Она превращается в высказывание, истинное или ложное,
при всякой подстановке вместо всех ее пропозициональных переменных любых конкретных высказываний.
Такой процесс подстановки называется интерпретацией данной формулы алгебры высказываний.
[Игошин, с. 30].

Рассмотрим пример из логического теста.
Дано высказывание: “пуфелки зелёные или йцукенги розовые”.
Требуется из набора высказываний выбрать те, которые из него следуют:

1) если пуфелки не зелёные, то йцукенги розовые

2) если пуфелки зелёные, то йцукенги розовые

3) неправда, что пуфелки не зелёные и йцукенги розовые

4) йцукенги розовые или пуфелки зелёные

5) если пуфелки не зелёные, то йцукенги не розовые

6) неправда, что пуфелки не зелёные и йцукенги не розовые

Обозначим $A$ = “пуфелки зеленые”, $B$ = “йцукенги розовые”.
Исходное высказывание можно переписать в виде $A vee B$.

Требуется выбрать из следующих высказываний тавтологии:

1) $A vee B ; to ; (neg A to B$)

2) $A vee B ; to ; A to B$

3) $A vee B ; to ; neg(neg A & B)$

4) $A vee B ; to ; B vee A$

5) $A vee B ; to ; neg A vee neg B$

6) $A vee B ; to ; neg(neg A & neg B)$

Разбор 1). По теореме о дедукции предложенная импликация эквивалентна тому, что из $A vee B$ и $A$ вытекает $B$.
Проверим это. $(A vee B) & neg A = B & neg A Rightarrow B$.

Разбор 2). Проверим, всегда ли из $A vee B$ и $A$ следует $B$. По правилу поглощения $(A vee B) & A = A$.
Если $A = 1$, $B = 0$, то из левой части не следует правая. Значит, 2) – не тавтология.

Разбор 3). Преобразуем правую часть: $neg(neg A & B) = neg B vee A = B to A$. Тогда 3) эквивалентно
$A vee B ; to ; (B to A)$. Но, как можно видеть из таблицы истинности, из “A или B” не следует $B to A$:
достаточно взять $B = 1$, $A = 0$. Следовательно, 3) – не тавтология.
Можно применить метод резолюций и показать, что конъюнкция левой части импликации и отрицания ее правой части
не будет тождественно ложной. В данном случае $(A vee B) & neg A & B = B&neg Anotequiv 0$.

Использование математической логики для решения практических задач

Язык математической логики универсален, потому что процедура формализации позволяет выделить
форму высказываний и уже для формальных логических выражений провести процедуру логического вывода,
не отвлекаясь на конкретное содержание. Язык математической логики находит применение как при описании
информационных систем, так и при анализе алгоритмов. Кроме того, этот язык используется в моделях
представления знаний [Волкова, с. 60].

Вывод новых знаний в рамках логической модели представления знаний заключается в получении некоторого
утверждения из имеющихся аксиом и правил вывода. Если в результате вывода утверждение получено, то оно
считается истинным и является логическим следствием из аксиом.

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

В качестве простого примера формализации утверждений запишем следующее предложение на языке логики предикатов:
“если некоторые здунцы не едят быстро, то все бутявки не зюмят”.

Определим предикаты $P(x)$ = “$x$ ест быстро”, $Q(x)$ = “$x$ зюмит”.
Утверждается, что $exists x, neg P(x) ; to ; forall y , neg Q(y)$.

Литература

Степанова – Математическая логика. Конспект лекций (2002)

Пак – Дискретная математика (2001)

Пруцков, Волкова – Математическая логика и теория алгоритмов (2018)

Игошин – Математическая логика (2017)

Гринченков, Потоцкий – Математическая логика и теория алгоритмов для программистов (2010)

Белоусов, Ткачев – Дискретная математика (2004)