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

Шаг 1. Используя законы 21 и 20, исключить эквиваленцию и импликацию.

Шаг 2. Занести отрицание к атомарным формулам, пользуясь законами 17-19 и 26-27.

Шаг 3. С помощью законов 22-23, 28-31 вынести кванторы вперед, используя при необходимости переименование связанных переменных (законы 32-33).

Рассмотрим пример. Пусть F=("x)P(x)®($y)("z)(P(y)&Q(y,z)).

Выполнив шаг 1 (с помощью закона 20), получим формулу F₁=Ø("x)P(x)Ú($y)("z)(P(y)&Q(y,z)).

С помощью закона 26 перейдем к формуле F₂=($x)ØP(x)Ú($y)("z)(P(y)&Q(y,z)).

Тем самым, шаг 2 также выполнен. Применим закон 30 слева направо Q₁=$, Q₂=$, u=y, получим формулу F₃=($x)($y)[ØP(x)Ú("z)(P(y)ÚQ(y,z))].

(Пользуемся тем, что ØP(x) не содержит y, а ("z)(P(y)&Q(Y,z)) не содержит х. Так как формула ØP(x) не содержит z, то применение закона 26 слева направо дает формулу F₄=($x)($y)("z)[ØP(x)ÚÚ(P(y)&Q(y,z))].

Это и есть искомая формула, имеющая ПНФ и равносильная формуле F.

В предыдущем примере выполнение шага 3 можно организовать по-другому. В формуле F₂ связанную переменную y заменим на переменную х (закон 33), получим формулу F₃^/=($x)ØP(x)Ú($x)("z)(P(x)&Q(x,z)).

Используя закон 23, перейдем к формуле F₄^/=($x)[ØP(x)Ú("z)(P(x)&Q(x,z))].

Затем, как и в предыдущем абзаце, с помощью закона 28 вынесем квантор по z за квадратную скобку. Получим формулу F₅^/=($z)("z)[ØP(x)Ú(P(x)&Q(x,z)].

Формула F₅^, как и формула F₄, имеет предваренную нормальную форму и равносильна формуле F. В некоторых ситуациях формула F₅^ предпочтительнее формулы F₄, поскольку содержит меньше кванторов. (Кстати, бескванторную часть формулы F₅^ можно упростить).

Перейдем к изучению сколемовской нормальной формы. Отметим вначале, что в логике первого порядка понятие конъюнктивной нормальной формы вводится точно так же, как и в логике высказываний. Сохраняется полностью алгоритм приведения к КНФ и утверждение теоремы 1.3.

Определение. Формула G имеет сколемовскую нормальную форму (сокращенно: СНФ), если G=("x)…("x_n)H, где формула Н не содержит кванторов и имеет конъюнктивную нормальную форму.

Например, формула ("x)[P(x)Ú(P(y)&Q(x,y)] имеет сколемовскую нормальную форму, а формулы ("x)($y)Q(x,y), ("x)[P(x)&(P(y)ÚQ(x,y)] не имеют.

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