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


Логика

В математической бинарной логике высказывание принимает значение истина (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 (его грамматика приведена ниже). Для логического И (конъюнкция, умножение) используются символы "&","*", для логического ИЛИ (дизъюнкция, сложение) - символы: "|","+", а логическое НЕТ может обозначаться тремя эквивалентными способами: "!","~","-":

В этом примере введены 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 находятся описания синтаксических ошибок (если они были).


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

Команды программы позволяют выводить выражения в различном формате:
Возможно также графическое представление дерева выражения в svg-формате:
Кроме базовых логических операций "+","*","!" существует ещё 3:
A == B                       // эквивалентность логических значений
A -> B  ==  !A + B           // логическое следование
A <-> B ==  (A->B)&(B->A)    // следование в обе стороны
Последние 2 операции во всех выражениях можно "убрать" командой defs[]:
В выражении можно разбить собранные вместе операции сложения и умножения. Для этого служит команда split[]. Обратная операция (объединение соседних "+" или "*") проводится командой collect[]. Ещё одна команда sort[] переставляет аргументы операций "+" и "*", так, чтобы сначала шли более короткие ветки, при равной их длине - по алфавиту. Максимальная глубина дерева выводится командой depth[]:
Тоже в графическом представлении:

Случайное выражение можно получить командой rand[макс_глубина, число_переменных, максимум_слагаемых_в_*+]:


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

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

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

Обратим внимание, что некоторые команды могут иметь в качестве аргумента выражение. В этом случае оно обрабатывается командой, но не добавляется к общему списку выражений. Если внутри [] ничего нет, то такая команда применяется ко всем введенным до неё выражениям.

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

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


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

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

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

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

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

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

Дополнительно к этому, в бинарной логике команда simplify[] учитывает закон исключения третьего:


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

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

(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)
В результате получится произведение (конъюнкции) сумм (дизьюнкций):
Совместное выполнение этих действий осуществляется командой cnf[] (коньюктивная нормальная форма) или dnf[] (дизъюктивная нормальная форма). Иногда они не вполне справляются с полным упрощением, поэтому можно попробовать применить их 2 раза по кругу:
Впрочем, необходимо быть острожным, так как применение дистрибутивных правил может радикально увеличить дерево выражения. Если ниже убрать комментарий в последней строке, произойдёт подвисание страницы, так как в результате перемножения скобок получится 4^8=65536 слагаемых:
Для проверки правильности преобразований можно использовать последовательность команд save[]; последовательность_преобразований; check[];. Первая команда сохраняет текущий список выражений в массиве Logic.saves, а вторая стравнивает текущие команды (после выполненных преобразований) с сохранёнными по таблице истинности:
В конце документа приведен тест проверки преобразований, в котором случайным образом генерятся логические выражения, для них проводится cnf и результат по таблице истинности сравнивается с исходным выражением.


Справочник

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

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


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


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