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

Шаг 1. Исключить всюду логические операции ® и « по правилам:

F₁®F₂º ÚF₂;

(F₁«F₂)=(F₁®F₂)Ù (F₂®F₁)=( ÚF₂)Ù( ÚF₁).

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

º$x( ), º ,

º"x( ), º .

Шаг 3. Переименовать связанные переменные по правилу: «найти самое левое вхождение предметной переменной такое, что это вхождение связано некоторым квантором, но существует еще одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной», операцию повторять пока возможна замена связанных переменных;

Шаг 4. Вынести кванторы влево по законам алгебры предикатов.

Шаг 5. Преобразовать бескванторную матрицу к виду КНФ. Алгоритм приведения матрицы формулы к виду КНФ приведен в алгебре высказываний.

Пример. .

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

l) удалить логические связки ®:

;

2) применить закон де Моргана º$x( ):

3) применить закон де Моргана º :

4) переименовать связанную переменную x=w:

5) переименовать связанную переменную y=v:

6) вынести квантор "v влево:

7) вынести квантор $y влево:

.

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

S={ }.

Пример. .

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

1) применить закон º"x( ):

2) применить закон º$x( ):

8) вынести квантор "x по закону дистрибутивности:

4) переименовать связанную переменную y=z:

5) вынести кванторы $z и $y влево:

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

S={ }.

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

1) по закону дистрибутивности:

2) по закону дистрибутивности:

3) по закону дистрибутивности:

4) по закону исключенного третьего:

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

Дизъюнкты матрицы содержат контрарные атомы P₁.(z) и , P₂.(x) и , свободные переменные которых могут быть одинаковыми или разными.

2.2.5. Сколемовская стандартная форма

Наличие разноимен­ных кванторов усложняет вывод заключения. Поэтому рассмотрим класс формул, содержащих только кванторы всеобщности. Фор­мула F называется "–формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т. е.

F = "x₁"x₂ ¼"x_n (M).

Для устранения кванторов существования из префикса формулы разработан алгоритм Сколема, вводящий сколемовскую функциюдля связывания предметной переменной квантора существования с другими предметными переменными.