Алгоритм преобразования ПНФ в ССФ

Алгоритм преобразования формул в ДНФ и КНФ.

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

Шаг 2. Многократно используем закон двойного отрицания, и законы де Моргана, чтобы внести знак отрицания внутрь формулы.

Шаг 3. Несколько раз используем дистрибутивные законы и другие законы, чтобы получить НФ.

Алгоритм преобразования формулы (K₁x₁)…(K_nx_n) (M), где каждое (K_ix_i), i = 1,…,n, есть или ("x_i) или ($x_i), и M есть КНФ в скулемовскую нормальную форму (СНФ) приведен ниже.

Шаг 1. Представим формулу в ПНФ (K₁x₁)…(K_nx_n) (M), где M есть КНФ. Пусть K_r есть квантор существования в префиксе (K₁x₁)…(K_nx_n), 1<=r<=n.

Шаг 2. Если никакой квантор всеобщности не стоит левее K_r – выберем новую константу c, отличную от других констант, входящих в M, заменим все x_r в M на c и вычеркнем K_rx_r из префикса. Если K₁,…K_i – список всех кванторов всеобщности, встречающихся в M левее K_r, 1< i<r, выберем новый i –местный функциональный символ f, отличный от других функциональных символов, заменим все x_r в M на f(x₁, x₂,…x_i) и вычеркнем K_rx_r из префикса.

Шаг 3. Применим шаг 2 для всех кванторов существования в префиксе. Последняя из полученных формул есть скулемовская стандартная форма формулы. Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.

Пример 7. Получить ССФ для формулы ($x)("y)("z)($u)("v)($w) (P(x, y, z, u, v, w).

В этой формуле левее ($x) нет никаких кванторов всеобщности, левее ($u) стоят ("y) и ("z), а левее ($w) стоят ("y), ("z) и ("v). Следовательно, мы заменим переменную x на константу a, переменную u - на двухместную f(y, z), переменную w - на трехместную функцию g(y, z, v). Таким образом, мы получаем следующую стандартную форму написанной выше формулы:

("y)("z)("v)(P(a, y, z, f(y, z), g(y, z, v)).

Определение 22: Дизъюнктом называется дизъюнкция литералов. Дизъюнкт, содержащий r литералов, называется r- литеральным дизъюнктом. Однолитеральный дизъюнкт называется единичным дизъюнктом. Если дизъюнкт не содержит никаких литералов, то он называется пустым дизъюнктом- я. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен.

Определение 23: Множество дизъюнктов S есть конъюнкция всех дизъюнктов из S, где каждая переменная в S считается управляемой квантором всеобщности.

Вследствие последнего определения, ССФ может быть представлена множеством дизъюнктов.

Пример 8: ССФ ("x)((ШP(x, f(x))Ъ R(x, f(x), g(x)))Щ (Q (x, g(x)) Ъ R(x, f(x), g(x)))) представить в виде множества дизъюнктов.

{ШP(x, f(x))Ъ R(x, f(x), g(x)), Q (x, g(x)) Ъ R(x, f(x), g(x))}.

Теорема 3. Пусть S – множество дизъюнктов, которые представляют ССФ формулы F. Тогда F противоречива в том и только в том случае, когда S противоречиво.

На основании теорем 2 и 3 можно сделать вывод, что формула G является логическим следствием формулы F тогда, когда противоречива конъюнкция множества S и формулы ШG, то есть противоречива формула S₁ Щ S₂ Щ …S_n Щ ШG. Таким образом, если в множество S добавить негативный литерал ШG и доказать, что полученное множество противоречиво, то тем самым можно доказать выводимость G из множества S.

Дата добавления: 2015-06-27