Нормальные формы в логике предикатов

В логике предикатов рассматриваются следующие нормальные формы:

· КНФ, ДНФ – конъюнктивная и дизъюнктивная нормальные формы;

· ПНФ – предваренная нормальная форма

· СНФ – сколемовская нормальная форма

Определение (предваренной нормальной формы). Формула j находится в предваренной нормальной форме, если она имеет вид

j: (Q₁x₁)…(Q_nx_n)s

где Q_i – квантор $ или " и s - формула без кванторов (префикс j, матрица j).

Использование ПНФ – для сравнения, проверки эквивалентности формул, для приведения к СНФ.

Алгоритм (приведения к предваренной нормальной форме)

1. Избавляемся от операций {«, ®} с помощью формул

(A«B) « (A®B)Ù(B®A)

(A®B) « (ØA Ú B)

2. Продвижение знака отрицания до атома с помощью формул

3. Кванторы выносятся наружу с помощью формул

(("x)A(x)) Ù (("x)B(x)) « ("x)(A(x) Ù B(x))

(($x)A(x)) Ú (($x)B(x)) « ($x)(A(x) Ú B(x))

a. Если формула B не содержит свободных вхождений переменной x, то

b. Пусть Q1, Q2 – кванторы $ или ". Формула B не содержит свободных вхождений переменной x. Переменная z не входит в формулу B, и не входит свободно в формулу A. B(z) – результат замены x на z.

((Q₁x)A(x)) Ú ((Q₂x)B(x)) « (Q₁x)(Q₂z)(A(x) Ú B(z))

((Q₁x)A(x)) Ù ((Q₂x)B(x)) « (Q₁x)(Q₂z)(A(x) Ù B(z))

Пример 1.

j: ("x)P(x) ® ($x)R(x)

j: Ø(("x)P(x)) Ú (($x)R(x))

j: (($x)ØP(x)) Ú (($x)R(x))

j: ($x)(ØP(x) Ú R(x)) (ПНФ)

Пример 2.

j: ("x)("y)[($z)(P(x,z) Ù P(y,z)) ® ($u)R(x,y,u)]

j: ("x)("y)[Ø($z)(P(x,z) Ù P(y,z)) Ú ($u)R(x,y,u)]

j: ("x)("y)[("z)(ØP(x,z) Ú ØP(y,z)) Ú ($u)R(x,y,u)]

j: ("x)("y)("z)($u)[ØP(x,z) Ú ØP(y,z) Ú R(x,y,u)] (ПНФ)

Определение (сколемовской нормальной формы). Формула j находится в сколемовской нормальной форме, если формула находится в ПНФ и используется только квантор всеобщности (").

Теорема (Сколема). Для каждого предложения j логики предикатов можно построить универсальное предложение j^* (СНФ) такое, что j выполнимо тогда и только тогда, если j^* выполнимо.

Алгоритм (приведения к сколемовской нормальной форме).

1. Строим ПНФ предложения j.

2. Последовательно, слева - направо вычеркиваем каждый квантор существования ($y), заменяя все вхождения переменной y на новый, еще не использованный функциональный символ f, в качестве аргумента f берем все переменные, связанные предшествующими ($y) кванторами всеобщности.

Функциональный символ f называется сколемовской функцией.

Пример 3.

j: ("x)($y)("z)($v)P(x, y, z, v)

j: ("x)("z)($v)P(x, f(x), z, v)

j: ("x)("z)P(x, f(x), z, g(x,z)) (СНФ)

Пример 4.

j: ($y)("x)("z)Q(x, y, z)

j: ("x)("z)Q(x, c, z) (c - константа) (СНФ)