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

Опр. Формула G имеет СНФ, если G = ( x)…( x_n) H,

где формула Н не содержит кванторов и имеет КНФ (конъюктивную нормальную форму).

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

Алгоритм приведения к СНФ:

1. Привод к ПНФ

2. Привести матрицу Н к ПНФ

3. Исключить кванторы

1) Если левее квантора (существования) нет квантора (всеобщности), то переменную, связанную этим квантором заменяем не встречающейся в формуле константой, а квантификацию отбрасываем. х(Р(х)) Р(а)

2) Если левее квантора находятся n кванторов , то переменная, связанная этим квантором заменяется на n-местный функциональный символ, зависящий от переменных, связанных этими кванторами , а сама квантификация отбрасывается.

Ех: после 2го шага имеем:

F = ( x) ( y) ( z) ( u) ( v) H (x, y, z, u, v)

предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g.

Тогда в формуле Н заменим:

х – на с

z – на f (y)

v – на g (y,u)

F = ( x) ( y) ( z) ( u) ( v) H (x, y, z, u, v)

тогда G = ( y) ( u) H (c, y, f(y), u, g(y, u))

Ех: привести функцию к СНФ

F = ( x) ( y) [P(x, y) ( z) (Q(x, z)) R(y))]

Применяя законы:

A B A B;

(A Q x B) Q x (A B), если A не содержит x, получаем формулу:

F₁ = ( x) ( y) ( z) [ P(x, y) (Q(x, z) R(y))]

которая имеет ПНФ

приводим к КНФ

F₂ = ( x) ( y) ( z) [(P(x, y) Q(x, z)) (P(x, y) R(y))]

сделаем подстановку x = a, z = f(y), получим

G = ( y) [ P(a, y) Q(a, f(y))) (P(a, y) R(y))]