Нормальные формы

Эквивалентные преобразования формул логики предикатов

Определение. Две формулы логики предикатов F и G одинаковой сигнатуры называются эквивалентными (равносильными), если при любой интерпретации они принимают одинаковые логические значения.

Пояснение. Сигнатурой называется список предикатных символов, функциональных символов и констант данной формулы.

Обозначение: F ~ G.

Таким образом, F ~ G тогда и только тогда, когда |= F G.

Задание. Сформулировать и доказать теорему об эквивалентной замене и теорему о подстановке для логики предикатов.

ОСНОВНЫЕ ЭКВИВАЛЕНТНОСТИ ЛП

Перестановка однородных кванторов:

∀x∀y(F(x, y))≡ ∀y∀x(F(x, y)),

∃x∃y(F(x, y))≡ ∃y∃x(F(x, y))

Переименование связных переменных:

∀xF(x)≡ ∀yF(y),

∃xF(x)≡ ∃yF(y) при отсутствии коллизий (y не входит в F(x)).

Вынос квантора всеобщности:

∀xF1(x) &∀xF2(x)≡∀x(F1(x) & F2(x)),

∀xF1(x) & F2 ≡∀x(F1(x) & F2),

∀xF1(x) ∨ F2 ≡∀x(F1(x) ∨ F2),

∀xF1(x) É F2 ≡∃x(F1(x) É F2),

F1 É ∀x F2(x) ≡∀x(F1É F2(x)),

∀x(F(x)) ≡∃x(F(x))

Вынос квантора существования:

∃xF1(x)∨∃xF2(x)≡∃x(F1(x)∨F2(x)),

∃xF1(x) & F2 ≡∃x(F1(x) & F2),

∃xF1(x) ∨ F2 ≡∃x(F1(x) ∨ F2),

∃xF1(x) É F2 ≡∀x(F1(x) É F2),

F1 É ∃x F2(x) ≡∃x(F1É F2(x)),

∃x(F(x)) ≡∀x (F(x))

НОРМАЛЬНЫЕ ФОРМЫ

Предварённая нормальная форма

Для удобства анализа сложных формул рекомендуется преобразовывать их к некоторой «нормальной» форме.

Если в логике высказываний приняты две нормальные формы ДНФ и КНФ, то в логике предикатов используется предварённая нормальная форма (ПНФ), суть которой сводится к разделению формулы на две части: префикс и матрицу. Для этого все кванторы выносят влево по правилам логики предикатов, указанным выше, формируя префикс, а логические связки соединяют подформулы, формируя матрицу. В результате будет получена формула вида:

Qx1 Qx2 … Qxn(M),

эквивалентная исходной формуле, где Qx1 Qx2 … Qxn - префикс формулы, Q∈{∀, ∃}, а М – матрица формулы, не содержащая кванторов. Затем матрицу формулы обычно преобразуют к виду КНФ по правилам логики высказываний.

Алгоритм приведения формулы к виду ПНФ:

Шаг 1: исключить в формуле всюду логические связки ≡ и →:

(F1≡F2) = (F1→F2) & (F2→F1)=(F1∨F2) & (F2∨F1),

(F1→F2)=(F1∨F2),

Шаг 2: продвинуть отрицание до элементарной формулы:

∀x(F)=∃x(F), ∃x(F)=∀x(F),

(F1∨F2)=(F1 &F2),

(F1&F2) = (F1∨F2)

Шаг 3: вынести кванторы влево по правилам, указанным выше, переименовывая, где необходимо, связанные переменные.

Шаг 4: преобразовать бескванторную матрицу к виду

КНФ, т. е. М=D1 & D2 & D3 &…, где Di – элементарная дизъюнкция.

Алгоритм приведения матрицы формулы к виду КНФ известен.

Очевидно, что в общем случае, для формулы может быть построено много эквивалентных ей ПНФ.

Пример 1. Привести формулу к виду ПНФ.

F=∃x1∀x2(P1(х1)→∀x3 (P2(х1,x3)∨P3(x2, x3))).

F=∀x1(∀x2(P1(х1)→∀x3(P2(х1, x3)∨P3(x2, x3)))) - операция отрицания,

F=∀x1∃x2((P1(х1)→∀x3 (P2(х1, x3)∨P3(x2, x3)))) – операция отрицания,

F=∀x1∃x2((P1(х1)∨∀x3(P2(х1, x3)∨P3(x2, x3)))) удаление связки «→»,

F=∀x1∃x2(P1(х1)&∀x3(P2(х1, x3)∨P3(x2, x3))) - операция отрицания,

F=∀x1∃x2(P1(х1) &∃x3((P2(х1, x3)∨P3(x2, x3)))) - операция отрицания,

F=∀x1∃x2(P1(х1) &∃x3(P2(х1, x3)&P3(x2, x3))) – операция отрицания,

F=∀x1∃x2∃x3 (P1(х1)&P2(х1, x3)&P3(x2, x3)) - перенос квантора ∃x3 влево.

Матрица ПНФ содержит три элементарных дизъюнкта:

K={P1(х1), P2(х1, x3), P3(x2, x3)}.

Пример 2. Дана F=(∀x(P1 (х)→∀y(P2 (y)→P3 (z))))&(∀y(P4 (x, y)→P5(z))). Привести формулу к виду ПНФ.

1) Удаляем логические связки «→»:

F=∀x(P1 (х)∨∀y(P2 (y)∨P3 (z))) &∀y(P4 (x, y)∨P5(z)),

2) Применяем закон ∀x(F(x))≡ ∃x(F(x)):

F=∀x(P1(х)∨∀y(P2 (y)∨P3 (z))) &∃y((P4 (x, y)∨P5(z))),

3) Применяем закон (F1∨F2)≡ (F1&F2):

F=∀x(P1(х)∨∀y(P2 (y)∨P3 (z))) &∃y (P4 (x, y)&P5(z)),

4) Переименовываем связанную переменную левого квантора x=w:

F=∀w(P1 (w)∨∀y(P2 (y)∨P3 (z)))&∃y(P4 (x, y)&(P5(z))),

5) Переименовываем связанную переменную левого квантора y=v:

F=∀w(P1 (w)∨∀v(P2 (v)∨P3 (z))) &∃y(P4 (x, y)&(P5(z))),

6) Выносим квантор ∀v в префикс:

F=∀w∀v(P1 (w)∨P2 (v)∨P3 (z)) &∃y(P4 (x, y)&P5(z)),

7) Вынести квантор ∃y в префикс:

F=∀w∀v∃y((P1 (w)∨P2 (v)∨P3 (z))&P4 (x, y)&P5(z)).

Матрица ПНФ содержит три элементарных дизъюнкта:

K={(P1 (w)∨P2 (v)∨P3 (z)), P4 (x y), P5(z)}.