Шаги 1 – 3 – те же, что и в предыдущем алгоритме.
Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме (алгоритм описан в §5 главы 1).
Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага мы получили формулу
F = (∃ x)(∀ y)(∃ z)(∀ u)(∃ v) H (x, y, z, u, v), где H – не содержит кванторов. Предположим, что она не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле H заменим x на c, z – на f (y), v заменим на g (y, u). Все кванторы существования вычеркнем. Получим формулу
G = (∀ y)(∀ u) H (c, y, f (y), u, g (y, u)). Это и есть результат выполнения шага 5.
Пример 2. Приведем пример приведения к СНФ. Пусть
F = (∃ x)(∀ y)[ P (x, y) → (∃ z)(Q (x, z) & R (y))].
Применяя законы 20 и 23, получаем формулу
F 1 = (∃ x)(∀ y)(∃ z)[ P (x, y) ∨ (Q (x, z) & R (y))].
Она имеет предваренную нормальную форму. Используя закон 12, приводим бескванторную часть к КНФ:
F 2 = (∃ 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))].
Теорема 2.4. Для всякой формулы F существует формула G, имеющая сколемовскую нормальную форму и одновременно с F выполнимая или невыполнимая.
Доказательство. Пусть G – результат работы алгоритма приведения к СНФ. То, что результатом работы алгоритма является формула в сколемовской нормальной форме, ясно из описания алгоритма. Формула, которая получается после выполнения шагов 1–4, равносильна исходной, и, в частности, одновременно с ней выполнима или невыполнима.
Проанализируем шаг 5. Предположим вначале, что исключается квантор существования, впереди которого нет кванторов общности. Можно считать, что это первый квантор в записи формулы, т.е.
E (u 1, …, un) = (∃ y) E /(y, u 1, …, un).
(Формула E / может содержать кванторы.) Рассмотрим интерпретацию ϕ с областью M, при которой формула E выполнима. Выполнимость означает, что найдутся элементы а1, …, an ∈ M такие, что высказывание (ϕ E)(a 1, …, an) или (что тоже самое) высказывание (∃ y)(ϕ E /)(y, a 1, …, an) истинно. Отсюда следует, что существует элемент b ∈ M такой, что высказывание (ϕ E /)(b, a 1, …, an) также истинно. Исключение квантора существования по y на пятом шаге приводит к формуле D (u 1, …, un) = E /(c, u 1, …, un), где c – константа, отсутствующая в E /. Расмотрим интерпретацию ψ, которая совпадает с ϕ на всех символах предикатов и функций, входящих в запись формулы F, и ψ(c) = b. Тогда
(ψ D)(a 1, …, an) = (ϕ E /)(b, a 1, …, an). Мы доказали, что если формула E выполнима, то выполнима и формула D. Предположим теперь, что выполнима формула D (u 1, …, un) = E /(c, u 1, …, un).
|
|
Это означает, что существует интерпретация ψ с областью M и элементы а1, …, an ∈ M такие, что высказывание (ψ E /)(ψ(c), a 1, …, an) истинно. Но отсюда следует истинность высказывания (∃ y)(ψ E /)(y, a 1, …, an). Следовательно, формула E (u 1, …, un) выполнима. Мы доказали, что из выполнимости формулы D следует выполнимость формулы E.
Рассмотрим теперь случай, когда исключается квантор существования, впереди которого есть k кванторов общности, т.е.
E (u 1, …, un) = (∀ x 1)…(∀ xk)(∃ y) E /(x 1, …, xk, y, u 1, …, un).
(Формула E / может содержать кванторы.) Исключение квантора по у на шаге 5 приведет к формуле D (u 1, …, un) =
(∀ x 1)…(∀ xk) E (x 1, …, xk, f (x 1, …, xk), u 1, …, un), где f – символ k -местной функции, не содержащийся в E. Предположим, что формула E выполнима. Выполнимость означает существование интерпретации ϕ с областью M и элементов a 1, …, an ∈ M таких, что высказывание (ϕ E)(a 1, …, an) истинно. Истинность этого высказывания означает, что для любых элементов x 1, …, xk ∈ M найдется элемент y ∈ M такой, что высказывание E /(x 1, …, xk, y, a 1, …, an) истинно. Если для данных элементов x 1, …, xk таких элементов y несколько, то зафиксируем один. Тем самым мы определили на M функцию i: Mx … xM → M такую, что высказывание
(ϕ E /)(x 1, …, xk, i (x 1, …, xk), a 1, …, an) истинно для всех x 1, …, xk ∈ M. Рассмотрим интерпрета-
цию ψ, которая совпадает с ϕ на всех символах функций и предикатов, входящих в запись формулы Е, и (ψ f)(x 1, …, xn)
= i (x 1, …, xn). Тогда
(ψ D)(a 1, …, an) =
(∀ x 1)…(∀ xk)(ϕ E /)(x 1, …, xk, i (x 1, …, xk), a 1, …, a n).
Последнее высказывание, как мы видели истинно. Следовательно, формула D (u 1, …, un) выполнима. Мы показали, что из выполнимости формулы E следует выполнимость формулы D.
Пусть выполнима формула D. Это означает, что существует интерпретация ψ с областью M и элементы a 1, …, an ∈ M такие, что высказывание (ψ D)(a 1, …, an) или (что то же самое) высказывание
(∀ x 1)…(∀ xk)(ψ E /)(x 1, …, xk, (ψ f)(x 1, …, xk), a 1, …, an) истинно. Отсюда следует, что для любых x 1, …, xk найдется y (равный (ϕ f)(x 1, …, xk)) такой, что высказывание
(ψ E /)(x 1, …, xk, y, a 1, …, an)
истинно. Следовательно, истинно высказывание
(∀ x 1)…(∀ xk)(∃ y)(ψ E /)(x 1, …, xk, y, a 1, …, an),
т.е. высказывание (ψ E)(a 1, …, an). Мы доказали, что из выполнимости формулы D следует выполнимость формулы E.