Методические указания к изучению курса "Дискретная математика" и решению задач для студентов специальности 200900



страница8/9
Дата01.05.2016
Размер0.61 Mb.
ТипМетодические указания
1   2   3   4   5   6   7   8   9

Сколемовские стандартные формы

Ранее было показано, что отношение логического следования F1, F2, , Fn |- B равнозначно общезначимости формулы |- F1& F2& &Fn B или противоречивости (невыполнимости) F1& F2& &Fn& B. Так как в дальнейшем в процедурах доказательства мы будем иметь дело только с невыполнимыми формулами, то без потери общности ограничимся ими.

Очевидно, что если формулы F и Ф равносильны, то F логически невыполнима тогда и только тогда, когда логически невыполнима Ф.

Благодаря этому утверждению и в силу того, что алгоритмы приведения к ПНФ сохраняют равносильность невыполнимых формул, мы ограничимся формулами, имеющими пренексный вид.

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

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


F= x1 x2 xr M,
где M – бескванторная формула.

Таким образом, возникает задача устранения кванторов существования в формулах, представленных в ПНФ. Это можно сделать путем введения сколемовских функций.

Пусть формула F представлена в ПНФ:

F= K1 x1 K2 x2 Kr xr M, где Kj { , }.

Пусть Ki (1 i r) квантор существования в K1 x1 K2 x2 Kr xr . Если i=1, т.е. ни один квантор общности не стоит впереди квантора существования, то выбираем константу c из области определения М, отличную от констант, встречающихся в M, и заменяем х на с в М. Из префикса квантор существования K1 x1 вычеркиваем. Если перед квантором существования Ki стоит , , …, кванторов общности, то выбираем m-местный функциональный символ f, отличный от функциональных символов в М, и заменяем хi на f ( , , …, ), называемую сколемовской функцией, в М. Квантор существования Ki хi вычеркиваем из префикса. Аналогично удаляются и другие кванторы существования в ПНФ. В итоге получаем -формулу. Опишем алгоритм последовательного исключения кванторов существования.


Алгоритм Сколема

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

Шаг 2. Найти наименьший индекс i такой, что K1 , K2 , Ki все равны , но Ki = . Если i = 1, т. е. квантор стоит на первом месте, то вместо х1 в формулу М подставить константу с, отличную от констант, встречающихся в М. Если такого i нет, то СТОП: формула F- является -формулой.

Шаг 3. Взять новый (i – 1)-местный функциональный символ fi, не встречающийся в F. Заменить F на формулу

x1 x2 xi-1 Ki+1 xi+1,, Kr xr M[x1, x2, , xi-1, f (x1, x2, , xi-1), xi+1, , xr].

Шаг 4. Перейти к шагу 2.
Таким образом, алгоритм Сколема, сохраняя свойство невыполнимости, приводит произвольную формулу, имеющую пренексный вид, к -формуле.

Напомним, что атом или его отрицание называется литерой. Литера вида А называется положительной, а вида А – отрицательной.

Рассмотрим теперь преобразование бескванторной части (матрицы) к виду так называемых дизъюнктов. Дизъюнктом называется формула вида

L1 L2 Lk,

где L1 ,L2 ,,Lk – произвольные литеры.

Дизъюнкты, соединенные знаком &, образуют конъюнктивную нормальную форму (КНФ). Существует простой алгоритм равносильного преобразования произвольной бескванторной формулы в КНФ. Представим его в развернутом виде.
Алгоритм приведения к КНФ

Шаг 1. Начало: дана формула F, составленная из литер с применением связок & и . Предполагается, что в формуле исключены скобки между одинаковыми связками, т. е. нет выражений вида

Ф1 2 Ф3), (Ф1 Ф2) Ф3



или

Ф1 & (Ф23), (Ф12) &Ф3.



Шаг 2. Найти первое слева в хождение двух символов ( (или ) ). Если таких вхождений нет, то СТОП: формула F находится в КНФ.

Шаг 3. Пусть первым вхождением указанной пары символов является (. Тогда взять наибольшие формулы Ф1, Ф2, …, Фr, 1, 2, …, s такие, что в F входит формула F1 = Ф1 Ф2 Фr (1& 2& …& s), которая связана с вхождением (. Заменить формулу F на формулу ( Ф1 Ф2 Фr 1)& ( Ф1 Ф2 Фr 2) & …& ( Ф1 Ф2 Фr s).

Шаг 4. Пусть первым вхождением является ) . Тогда взять наибольшие формулы Ф1, Ф2, …, Фr, 1, 2, …, s такие, что в F входит формула F1 = (1& 2& …& s) Ф1 Ф2 Фr, связанная с вхождением ) . Заменить F1 на (1 Ф1 Ф2 Фr)& (2 Ф1 Ф2 Фr) & …& (s Ф1 Ф2 Фr).

Шаг 5. Перейти к шагу 2.
Итак, последовательным применением алгоритма приведения к ПНФ, алгоритма Сколема и алгоритма приведения к КНФ с сохранением свойства невыполнимости любая формула F может быть представлена набором дизъюнктов, объединенных кванторами общности. Такую формулу будем называть формулой, представленной в Сколемовской стандартной форме (ССФ). В дальнейшем формулы вида x1 x2 xr[D1 & D2 & …& Dk] , где D1 , D2 , , Dk - дизъюнкты, а x1 , x2, , xr - различные переменные, входящие в эти дизъюнкты, будет удобно представлять как множество дизъюнктов S ={ D1 , D2 , , Dk }.



  1. Поделитесь с Вашими друзьями:
1   2   3   4   5   6   7   8   9




База данных защищена авторским правом ©zodorov.ru 2020
обратиться к администрации

    Главная страница