Логические эквивалентные преобразования в исчислении предикатов 1-го порядка. Алгоритм приведения к ПНФ

В отличии от исчислений высказываний, в логике предикатов не существует детерминированного алгоритма, который определял бы к какому классу принадлежит произвольная формула исчисления предикатов.

Переменные, находящиеся в сфере действия кванторов называются связанными, остальные – свободными.

Пренексная нормальная форма (ПНФ).

Опр. Формула, состоящая из префикса, т.е. конечной последовательности кванторов и матрицы, т.е. формулы, не содержащей кванторы.

В общем виде ПНФ: K₁x₁ K₂x₂ … K_nx_n M

префикс матрица

K_i { , } – квантор

Ех: x y ((Q(x, y) (P(f(x)) R(x, y))) – ПНФ

x(P(x) y Q(x, y)) – не ПНФ

Теорема: Для всякой формулы F существует формула G, равносильная F и имеющая ПНФ.

Алгоритм преобразования в ПНФ:

1. Исключить эквиваленцию и импликацию

A B A B

A B (A B) (B A)

2. В случае необходимости производится переименование переменных так, что все переменные, связанные разными кванторами стали различными и чтобы никакая переменная не имела одновременно свободных и связанных вхождений.

x(P(x)) x Q(x) x P(x) y Q(y)

x(P(x) x Q(x, y)) x (P(x) y Q(z, y))

3. Удаляются те кванторы, область действия которых не содержит вхождения квантифицированной переменной.

4. Знаки отрицаний переносятся внутрь формул, пока они не останутся перед атомами (законы де Моргана и снятия двойного отрицания).

(A B) A B (A B) A B

( xA) ( x A)

( xA) ( x A)

5. Все кванторы переносят в начало формул

для : ( xA xB) x(A B)

для : ( xA xB) x(A B)

когда B не содержит x:

( xA B) x(A B) ( xA B) x(A B)

( xA B) x(A B) ( xA B) x(A B)

когда A не содержит x:

(A QxB) Qx(A B)

(A QxB) Qx(A B)

Q – любой квантор (, )

Ех: привести формулу к ПНФ

x(P(x) y x (Q(x, y) z R(a, x, y)))

1) x(P(x) y x(Q(x, y) zR(a, x, y))) 2) x(P(x) y x(Q(x, y) zR(a, x, y)))

3) x(P(x) y u(Q(u, y) zR(a, u, y))) 4) x(P(x) y u(Q(u, y) R(a, u, y)))

x y u(P(x) (Q(u, y) R(a, u, y)))