Алгебра логики


Логика

В математической бинарной логике высказывание принимает значение истина (1) или ложь (0). Примеры высказываний: A="Сейчас идёт дождь" или B="Все блондинки умны". При помощи логических операций И (&), ИЛИ () и НЕ (¬) из элементарных высказываний можно строить составные: ¬(A & B ∨ C).

Кроме высказываний, в конкретных теориях, рассматриваются предметные константы, переменные и функции. Например, в арифметике функция add(x,1) прибавляет к переменной x константу 1 и возвращает некоторое значение, т.е. каждому x и 1 ставит в соответствие некоторую константу (число).

Если логическое высказывание зависит от предметных величин, то оно называется предикатом. Например, в арифметике логическая функция меньше LT(x,y) зависит от двух предметных переменных и принимает значение истина, если x меньше y и ложь в противном случае.

Предметные переменные, константы и функции принято обозначать маленькими буквами: $x, a, f($x) (что бы отличить переменную от константы, будем перед именем переменной ставить знак доллара). Предикаты и высказывания (константные предикаты) обозначаются большими буквами: A, B(x), C(x,f(y)).


Многозначная логика

В многзначной логике для логического ИЛИ будем использоваться функцию максимума a+b = max(a,b), для логического И - функция минимума a*b = min(a,b) и для отрицания !a = maxVal-a. Для нечёткой логики с непрерывными значениями в диапазоне [0...1] существуют также альтернативные возможности, которые мы приведём для справки:

x !x x | y max(x,y) x+y-x*y x & y min(x,y) x*y
       

В принципе, эти возможности можно использовать и в многозначной логике, деля предварительно значения на maxVal.


Логические операции

Аналогично парсеру арифметических выражений пишется парсер логических выражений logic.js (его грамматика приведена ниже). Для логического И (конъюнкция, умножение) используются символы "&","*", для логического ИЛИ (дизъюнкция, сложение) - символы: "|","+", а логическое НЕТ может обозначаться тремя эквивалентными способами: "!","~","-":

A+B+C;
(A*B)+C;
C+(A*B);
(A+A+!C)*D*D;
В этом примере введены 4 логических выражения, разделённых точкой с запятой (";"), а затем команда out[], которая справа от поля редактирования распечатывает эти выражения. Здесь и далее можно менять поле редактирования. Повторный прасинг программы проводится после ввода точки с запятой ";" (можно любую ";" удалить и тут же вернуть или добавить её после выражения). Отметим, следующие моменты:

Грамматика

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

   PRG   :- COM; PRG    |  COM              // программа = выражения или команды, через ;
   COM   :- #NAME[LST_E]|  E                // комнанда преобразования или вывода
   LST_E :- E,LST_E     |  E                // список аргументов команды - это выражения
   E     :- VAR := E    |  T1               // подстановка логической переменной
   T1    :- T2 <-> T1   |  T2 == T1 | T2    // следование в обе стороны и тождество
   T2    :- T3 -> T3    |  T3               // логическое следование
   T3    :- T4 {+|} T3  |  T4               // один из перечисленных символов в {...}
   T4    :- T5 {*&} T4  |  T5               // коньюнкция (логическое И) - выше приоритет
   T5    :- {-~!}T5     |  T6               // самый высокий приоритет у отрицания
   T6    :- [F{NAME=}F] | NAME[LST]  | T7   // предикат (логическая функция)
   T7    :- (E)         | NUM  | VAR        // логическое значение или переменная
   LST   :- F,LST       |   F               // аргуметы предметной функции
   F     :- NAME(LST)   | $VAR | CONST | NUM// предметные функции, константы, числа

   VAR   :- NAME                            // предметная переменная
   CONST :- NAME                            // предметная константа
Выражение представляется структурой: {op, nm, ar}, где op - тип операции, nm - значение (для чисел, имён переменных, констант, функций), ar - массив аргументов, если они есть (для бинарных операций состоит из двух элементов).

Используются следующие типы операций: "N" - число от 0 до maxVal (многозначная логика), "V" - переменное высказывание, "+", "*", "!", "->", "<->", "==" - логические операции "P" - предикат (логическая функция), "G" - отрицание предиката (сокращение для {op:"!",ar:[{op:"P",nm:...}]} => {op:"G",nm:...}), "F" - предметная функция, "X" - предметная переменная, "C" - предметная константа, "CM" - команда управления. Например Parent($x, f(a)) & A это:

{op:"*", ar:[
   {op:"P", nm:"Parent",ar:[{op:"X",nm:"$x"},{op:"F",nm:"f",ar:[{op:"C",nm:"a"}]}]},
   {op:"V", nm:"A"}
]};
После парсинга (функция parse) получается массив exprs выражений и команд. Функция parse также возвращает строку откликов команд, а в переменной err находятся описания синтаксических ошибок (если они были).


Печать выражений

Команды программы позволяют выводить выражения в различном формате:
!A*!(A+B);
¬A&¬(A∨B);

{op:"*",ar:[{op:"!",ar:[{op:"V",nm:"A"}]},{op:"!",ar:[{op:"+",ar:[{op:"V",nm:"A"},{op:"V",nm:"B"}]}]}]};
Возможно также графическое представление дерева выражения в svg-формате:
!A*!(A+B); A+(B*C*D)+1; (P[x]*[x Q f(x,y)]*[$x=y])->!Bad[s];
!A!+AB +ABCD1 PxQxfxy=$xy!Bads
Кроме базовых логических операций "+","*","!" существует ещё 3:
A == B                       // эквивалентность логических значений
A -> B  ==  !A + B           // логическое следование
A <-> B ==  (A->B)&(B->A)    // следование в обе стороны
Последние 2 операции во всех выражениях можно "убрать" командой defs[]:
!A+B;
(!A+B)*(!B+A);
!(!A+B)+C;
В выражении можно разбить собранные вместе операции сложения и умножения. Для этого служит команда split[]. Обратная операция (объединение соседних "+" или "*") проводится командой collect[]. Ещё одна команда sort[] переставляет аргументы операций "+" и "*", так, чтобы сначала шли более короткие ветки, при равной их длине - по алфавиту. Максимальная глубина дерева выводится командой depth[]:
((C*D)+!B)*!F*(E+D+E)*(B+A);

((((C*D)+!B)*!F)*((E+D)+E))*(B+A);
((C*D)+!B)*!F*(E+D+E)*(B+A);
!F*(A+B)*(D+E+E)*(!B+(C*D));

3 <= !F*(A+B)*(D+E+E)*(!B+(C*D))
Тоже в графическом представлении:

+CD!B!F+EDE+BA +CD!B!F++EDE+BA +CD!B!F+EDE+BA !F+AB+DEE+!BCD
Случайное выражение можно получить командой rand[макс_глубина, число_переменных, максимум_слагаемых_в_*+]:
!A1BB0+BAA1B


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

В бинарной логике логические переменные принимают значения 0 (ЛОЖЬ) или 1 (ИСТИНА). При помощи символа ":=" можно присвоить логическим переменным те или иные значения (или выражения). Такое присваивание интерпретируется не как выражение, в как подстановка, которая хранится в отдельном массиве Logic.subs. При парсинге все подстановки, введенные ранее, заменяют соответствующие логические переменные. Команда subs[] выводит текущие значения всех подстановок.

1*0;
1+0;
!1*(1+D);

A:=1; B:=0; C:=1+D;

Команда table[выражение] выводит таблицу истинности выражения, а base[3] - вместо двоичной логики (по умолчанию) задаёт троичную логику. Степень истинности выражения true[] возвращает отношение суммы всех результирующих значений в таблице истинности к сумме максимальных значений (1 в бинарной логике, 2 - в троичной) в этой же таблице:

A*B:
A|012012012
B|000111222
=|000011012

0.27778 <= A*B
0.72222 <= A+B
base=2, maxVal=1;
Обратим внимание, что некоторые команды могут иметь в качестве аргумента выражение. В этом случае оно обрабатывается командой, но не добавляется к общему списку выражений. Если внутри [] ничего нет, то такая команда применяется ко всем введенным до неё выражениям.

Двойное равенство A==B сравнивает логические значения и если они совпадают, возвращает Logic.maxVal (для бинарной логики 1) или 0, если не совпадают:

Операции A<->B и A==B совпадают только в бинарной логике. Выше стоит поменять в команде base 3 на 2 (не забываем затем добавить или изменить разделитель ";").

A==B:
A|012012012
B|000111222
=|200020002
A<->B:
A|012012012
B|000111222
=|210111012


Алгебра логики

Логические выражения, стоящие слева и справа от знака "==" имеют одинаковые таблицы истинности. Если "A==B" всегда истинно, его называют тождеством. Ниже приведены основные тождества алгебры логики. Операции "*" (&) и "+" (|) коммутативны, ассоциативны и взаимно дистрибутивны (первые 6 формул). Кроме этого, справедливы законы поглощения (следующие 4 тождества), 2 правила де-Моргана и закон двойного отрицания !!A==A:

1 <= (A*B)==(B*A)
1 <= (A+B)==(B+A)
1 <= (A*B*C)==((A*B)*C)
1 <= (A*B*C)==((A*B)*C)
1 <= (A*(B+C))==((A*B)+(A*C))
1 <= (A+(B*C))==((A+B)*(A+C))
1 <= (A*A)==A
1 <= (A+A)==A
1 <= ((A+B)*A)==A
1 <= ((A*B)+A)==A
1 <= !(A*B)==(!A+!B)
1 <= !(A+B)==(!A*!B)
1 <= !!A==A
0.83333 <= A+!A
0.88889 <= (A*(!A+B))==(A*B)
0.88889 <= (A+(!A*B))==(A+B)
Формула A + !A (закон исключения третьего) и следующие за ней, справедливы только в бинарной логике и не выполняются в многозначных логиках (поменяйте 3 на 2).

Преобразовать выражения при помощи правил де-Моргана и двойного отрицания можно командой morgan[]:

!A+!B;
!A*!B;
A;
A+(B*C);
Дистрибутивные законы можно применять при помощи команд mult[] (для конъюнкции) или add[] (для дизъюнкции). Кроме "перемножения", они проводят элементарные упрощения: A*A==A, A*0==0, A*1==A и т.д.
A*(B+C);
(A*B)+(A*C);
A*(A+C)*(B+A)*(B+C);

В выражениях можно использовать числа: 0 - ЛОЖЬ или 1 - ИСТИНА (для бинарной логики). В троичной логике ИСТИНА равна 2 и т.д. Эти значения учитываются в командах table[] и true[]. Их также можно упростить при помощи команды simplify[]:

base=3, maxVal=2;
2;
A;
A;
0;
A;
A;
Дополнительно к этому, в бинарной логике команда simplify[] учитывает закон исключения третьего:
B;
0;


Коньюктивная нормальная форма

Коньюктивная нормальная форма - это преобразование исходного выражения при помощи алгебры логики в следующий вид:

(A1 + A2 + A3 + ...) * (B1 + B2 + B3 + ...) *  (C1 + C2 + C3 + ...) * ...,
где в круглых скобках стоит сумма (дизьюнкция) простых высказываний A,B,... или их отрицаний !A, !B,.... Для такого преобразования, сначала необходимо рекурсивно подставить определения для следований, затем при помощи правил де-Моргана и двойного отрицания прижать знак отрицания к высказываниям и, наконец, применить закон дистрибутивности по отношению к дизьюнкции:
A <-> B == (A -> B)*(B -> A);    A -> B == !A + B;
!!A == A;  !(A*B) == !A + !B;   !(A+B)  == !A * !B;
A+(B*C) == (A+B)*(A+C);         (B*C)+A == (B+A)*(C+A)
В результате получится произведение (конъюнкции) сумм (дизьюнкций):
!(B<->A)*A;
!((!B+A)*(!A+B))*A;
((B*!A)+(A*!B))*A;
((B+A)*(B+!B)*(!A+A)*(!A+!B))*A;
(B+A)*(B+!B)*(!A+A)*(!A+!B)*A;
!B*A;

1 <= (!(B<->A)*A)==(!B*A)
Совместное выполнение этих действий осуществляется командой cnf[] (коньюктивная нормальная форма) или dnf[] (дизъюктивная нормальная форма). Иногда они не вполне справляются с полным упрощением, поэтому можно попробовать применить их 2 раза по кругу:
(C+A)*(B+A+!C);
(A+C)*(A+B+!C);
A+(B*C);
(A+B)*(A+C);

1 <= ((A+C)*(!C+A+B))==(A+(B*C))
1 <= ((A+C)*(!C+A+B))==((A+B)*(A+C))
Впрочем, необходимо быть острожным, так как применение дистрибутивных правил может радикально увеличить дерево выражения. Если ниже убрать комментарий в последней строке, произойдёт подвисание страницы, так как в результате перемножения скобок получится 4^8=65536 слагаемых:
((A<->B)<->C)<->D;
(A+B+C+!D)*(A+B+D+!C)*(A+C+D+!B)*(A+!B+!C+!D)*(B+C+D+!A)*(B+!A+!C+!D)*(C+!A+!B+!D)*(D+!A+!B+!C);
Для проверки правильности преобразований можно использовать последовательность команд save[]; последовательность_преобразований; check[];. Первая команда сохраняет текущий список выражений в массиве Logic.saves, а вторая стравнивает текущие команды (после выполненных преобразований) с сохранёнными по таблице истинности:
save 1 expression
(A+C+D)*(B+!A+!D)*(D+!A+!B);
1 <= (!((A<->(B+!A))<->(C+A+(B*C)+D))<->(D->!A))==((A+C+D)*(B+!A+!D)*(D+!A+!B))
В конце документа приведен тест проверки преобразований, в котором случайным образом генерятся логические выражения, для них проводится cnf и результат по таблице истинности сравнивается с исходным выражением.


Справочник

Базовые логические операции:

Для управления выводом результатов вычислений используются следующие команды: Следующие команды используются для управления собственно вычислениями. Если команда не имеет аргумента, она применяется ко всем введенным до неё логическим выражениями. Иначе, обрабатывает выражение которое находится внутри неё между скобками [ ]. При этом это выражение в список команд не добавляется (отладочная мода). Вычисления, изменения внутреннего представления: Унификация, подстановка, вывод:


Редактор логических выражений


A+(A*B);

Проверка правильности алгебраических преобразований:


Арифметический парсер <