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

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

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

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

Пример 1. Пусть

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, применение закона 28 дает формулу

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 ₅^/ = (∃ x)(∀ 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)] не имеют.