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

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

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

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

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

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

: (Q₁x₁)…(Q_nx_n)

где Q_i – квантор  или  и  - формула без кванторов (префикс , матрица ).

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

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

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

(AB)  (AB)(BA)

(AB)  (A  B)

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

(A  B)  (A  B) (A  B)  (A  B) A  A

((x)A)  (x)(A) ((x)A)  (x)(A)

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

((x)A(x))  ((x)B(x))  (x)(A(x)  B(x))

((x)A(x))  ((x)B(x))  (x)(A(x)  B(x))

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

   ((x)A(x))  B  (x)(A(x)  B) ((x)A(x))  B  (x)(A(x)  B)

   ((x)A(x))  B  (x)(A(x)  B) ((x)A(x))  B  (x)(A(x)  B)

2. Пусть 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.

: (x)P(x)  (x)R(x)

: ((x)P(x))  ((x)R(x))

: ((x)P(x))  ((x)R(x))

: (x)(P(x)  R(x)) (ПНФ)

Пример 2.

: (x)(y)[(z)(P(x,z)  P(y,z))  (u)R(x,y,u)]

: (x)(y)[(z)(P(x,z)  P(y,z))  (u)R(x,y,u)]

: (x)(y)[(z)(P(x,z)  P(y,z))  (u)R(x,y,u)]

: (x)(y)(z)(u)[P(x,z)  P(y,z)  R(x,y,u)] (ПНФ)

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

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

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

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

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

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

Пример 3.

: (x)(y)(z)(v)P(x, y, z, v)

: (x)(z)(v)P(x, f(x), z, v)

: (x)(z)P(x, f(x), z, g(x,z)) (СНФ)

Пример 4.

: (y)(x)(z)Q(x, y, z)

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

Теоретико-множественное представление предложений PrL

Определение. Пусть предложение  находится в СНФ:

: (x₁) … (x_n)[С₁(x₁, … , x_n) …  С_k(x₁, … , x_n)] где

С_i(x₁, … , x_n) – дизъюнкция атомов или их отрицаний P₁, … , P_k. Тогда теоретико-множественным представлением предложения  называется множество

S={{ , … , }, … , { , … , }}

Пример 5.

: (y)(x)(z)[P(x, y)  (Q(x)  R(z))  (D(z,x))]

ТМФ: {{ P(x, y)}, {Q(x), R(z)}, {D(z,x)}}