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

Шаг 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).

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