Сколемовская и клаузальная формы

Для того, чтобы легче и эффективнее было доказывать невыполнимость формулы или некоторого их множества, устанавливают ещё более строгие пределы использования механизма квантификации. Каждой формуле А сопоставляется некоторая формула SA с гарантией, что формулы либо обе выполнимы, либо обе невыполнимы. (SA É А). Форма SA называется сколемовскойформой для соответствующей формулы А.

Сколемовская форма – это такая предварённая форма, в которой исключены кванторы существования. Сколемовская форма – это еще более узкий класс формул, так называемых "-формул. Формула F называется "-формулой, если она представлена в ПНФ, причем кванторная часть состоит только из кванторов всеобщности, т.е. F = " x ₁ " x ₂ …" x_m P, где P – бескванторная формула.

Отсюда возникает задача устранения кванторов существования в формулах, представленных в ПНФ.

Сколемовское преобразование (исключение $-квантификации):

Сколемовская нормальная форма (СНФ) строится в соответствии со следующими правилами:

1. Формула логики предикатов представляется в ПНФ.

2. Последовательно (слева направо) вычеркиваем каждый квантор существования, например $ y. Эта процедура заключается в следующем. Если на первом месте в формуле стоит квантор существования, то стоящая под ним предметная переменная всюду в данной формуле заменяется некоторым конкретным предметом (индивидом), и сам квантор существования опускается. Например, для формулы ($ x)(" y)(P (x, y)) эта процедура даёт (" y)(P (а, y)). Если перед квантором существования $ y стоят кванторы общности " x ₁,…, " x_k, то выбирается новый k-местный функциональный символ f и все у в формуле заменяются на f (x ₁,..., х _k), а квантор $ у опускается. Функциональный символ f является сколемовской функцией.

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

Переход от ПНФ к сколемовской нормальной форме не затрагивает свойство формулы быть невыполнимой (противоречивой). Это доказывается следующей теоремой.

Теорема. Пусть формула F задана в ПНФ и преобразована в СНФ. Тогда F в ПНФ логически невыполнима тогда и только тогда, когда невыполнима СНФ для F.

Однако следует заметить, что если имеется выполнимая формула F, то может оказаться, что СНФ для F будет невыполнимой.

Рассмотрим теперь преобразование бескванторной части к виду так называемых дизъюнктов. Дизъюнктом называется формула вида L ₁Ú L ₂Ú…Ú L_k, где L_i – произвольная литера. Дизъюнкт, не имеющий литер, называется пустым дизъюнктом (ÿ). По определению он всегда ложен.

Дизъюнкты, соединенные знаком Ù, образуют КНФ.

Рассмотрим алгоритм равносильного преобразования произвольной бескванторной формулы в КНФ.

Шаг 1. Дана формула F, составленная из литер с применением связок Ù и Ú. Предполагается, что в формуле исключены скобки между одинаковыми связками, т.е. нет выражений вида Φ ₁Ú(Φ ₂Ú Φ ₃), (Φ 1Ú Φ 2)Ú Φ 3, (Φ 1Ù Φ 2)Ù Φ 3, Φ ₁Ù(Φ ₂Ù Φ ₃).

Шаг 2. Найти первое слева вхождение символов «Ú(» или «)Ú» (здесь предполагается, что скобка не является скобкой атома). Если таких вхождений нет, то формула F находится в КНФ.

Шаг 3. Пусть первым вхождением указанной пары символов является «˅(». Тогда нужно взять наибольшие формулы Φ ₁, Φ ₂,…, Φ _l, Ψ ₁, Ψ ₂,…, Ψ _s такие, что в F входит формула F ₁ = Φ ₁Ú Φ ₂Ú…Ú Φ _l Ú(Ψ ₁Ù Ψ ₂Ù…Ù Ψ _s), которая связана с вхождением «Ú(». Заменить формулу F ₁ на формулу

(Φ ₁Ú Φ ₂Ú…Ú Φ _l Ú Ψ ₁) Ù (Φ ₁Ú Φ ₂Ú…Ú Φ _l Ú Ψ ₂) Ù … Ù (Φ ₁Ú Φ ₂Ú…Ú Φ _l Ú Ψ _s)

Шаг 4. Пусть первым вхождением является «)Ú». Тогда взять наибольшие формулы Φ ₁, Φ ₂,…, Φ _l, Ψ ₁, Ψ ₂,…, Ψ _s такие, что в F входит формула F ₁ = (Ψ ₁Ù Ψ ₂Ù…Ù Ψ _s)Ú Φ ₁Ú Φ ₂Ú…Ú Φ _l, связанная с вхождением «)Ú». Заменить F ₁ на формулу

(Ψ ₁Ú Φ ₁Ú Φ ₂Ú…Ú Φ _l) Ù (Ψ ₂Ú Φ ₁Ú Φ ₂Ú…Ú Φ _l) Ù … Ù (Ψ _s Ú Φ ₁Ú Φ ₂Ú…Ú Φ _l)

Шаг 5. Перейти к шагу 2.

Кроме того, в алгоритме надо предусмотреть приведение подобных членов, а также всевозможные склеивания и поглощения.

Клаузальной формой называется такая сколемовская форма, матрица которой является КНФ. Любая сколемовская форма допускает эквивалентную клаузальную форму.

Итак, последовательным применением алгоритма приведения к ПНФ, алгоритма получения СНФ и алгоритма приведения к КНФ с сохранением свойства невыполнимости любая формула F может быть представлена набором дизъюнктов, объединенных кванторами общности. Такую формулу будем называть формулой, представленной в сколемовской стандартной форме (ССФ).

В дальнейшем формулы вида " x ₁" x ₂" x_r [ D ₁Ù D ₂Ù…Ù D_k ], где D ₁, D ₂,…, D_k – дизъюнкты, а x ₁, x ₂, x_r – различные переменные, входящие в эти дизъюнкты, будет удобно представлять как множество дизъюнктов S = { D ₁, D ₂,…, D_k }.

Например, множеству дизъюнктов

соответствует следующее представление в ССФ

И, наконец, когда говорят, что множество дизъюнктов S = { D ₁, D ₂,…, D_k } невыполнимо (противоречиво), то всегда подразумевают невыполнимость формулы " x ₁" x ₂" x_r [ D ₁Ù D ₂Ù…Ù D_k ], где x ₁, x ₂, x_r – различные переменные, входящие в дизъюнкты.

Доказательство правильности логического вывода основано на следующих теоремах.

Теорема 1. Даны формулы F ₁, F ₂, F_n и G. Формула G является логическим следствием формул F ₁, F ₂, F_n тогда и только тогда, когда формула F ₁Ù F ₂Ù…Ù F_n → G общезначима.

Теорема 2. Даны формулы F ₁, F ₂, F_n и G. Формула G является логическим следствием формул F ₁, F ₂, F_n тогда и только тогда, когда формула F ₁Ù F ₂Ù…Ù F_n Ù G противоречива.