Метод резолюций в ИВ.

Напомним, что если x логическая переменная, а ,то выражение

называется литерой.

Пусть D₁=B₁VA, D₂=B₂VA — дизъюнкты. Дизъюнкт B₁VB₂ называется резольвентой дизъюнктов D₁ и D₂ по литере А и обозначается через res_A(D₁,D₂). Резольвентой дизъюнктов D₁ и D₂

называется резольвента по некоторой литере и обозначается через . res(D₁D₂). Очевидно, что res(A,┐A)=0. Действительно, т.к. A=AV0 и -┐A=┐AV0, то res(A,┐A)=0V0=0. Если дизъюнкты D₁и D₂ не содержат контрарных литер, то резольвент у них не существует.

Пример 2.4.1. Если D1=AVBVC, D2 = ┐A V┐ В VQ, то

res_A(D_1,D₂)=BVCV┐B VQ, res_B(D₁,D₂)=AVCV┐ A VQ,

res_c(D_1,D₂) не существует.

Утверждение 2.4.1. Если res(D₁,D₂) существует, то D_1,D₂+ res(D₁,D₂).

Пусть S=(D₁,D₂,...,D_n) - множество дизъюнктов. Последовательность формул F₁,F₂,...,F_n называется резолютивным выводом из S, если для каждой формулы F_k выполняется одно из условий:

1. F_kS;

2. Существуют j, k <i такие, что F_i=res(F_j,F_k).

Теорема 2.4.2. (о полноте метода резолюций). Множество дизъюнктов S противоречиво в том и только в том случае, когда существует, резолютивный вывод из S, заканчивающийся 0.

Отметим, что метод резолюций можно использовать для проверки выводимости формулы F из данного множества формул F₁,F₂,...,F_n. Действительно, условие F₁,F₂,...,F_n+F равносильно условию F₁,F₂,...,F_n ,┐F+ (множество формул противоречиво), что cвою очередь равносильно условию Q+, где Q=F₁^F₂^...^F_n^(┐F). Приведем формулу Q к КНФ: Q=D₁^D₂^...^D_m, тогда Q+ D₁^D₂^...^D_m+ D₁,D₂,...,D_m+.

Таким образом, задача проверки выводимости F₁,F₂,...,F_n +F сводится к проверке противоречивости множества дизъюнктов S={D₁,D₂,...,D_m}, что равносильно существованию резолютивного вывода 0 из S.

Пример 2.4.2. Проверить методом резолюций cоотношение

А(ВС), CDE, ┐FD&(┐)E + A(BF).

Согласно утверждению 2.4.1. надо проверить на противоречивость множество формул

S = {А(ВС), CDE, ┐FD&(┐)E, ┐(A(BF))}.

Приведем все формулы из. S к КНФ:

S = {┐A V┐ В VC,C D V E,F V D┐E,┐AV┐BVF)} =

=.{┐A V┐ В VC,┐C V┐D V E,(F V D)(FV┐E),AB┐F}

Таким образом, получаем множество дизъюнктов

S =.{┐A V┐ В VC,┐C V┐D V E,F V D,FV┐E,AB┐F}

Построим резолютивный вывод из S, заканчивающийся 0:

1) res _A{┐A V┐ В V С,А} = ┐В V С ;

2) res_B{┐B V С,В} = С ;

3) res_D{┐C V┐DVE,FVD} = ┐C VEVF;

4) res_E{┐C V E V F,F V┐E} = ┐С VF ;

5) res_c{C,┐C VF} = F;

6) res {F, ┐F} = 0 .

Итак, заключаем, что формула A(BF) выводима из множества формул А(ВС), CDE, ┐FD&()E .

Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает

Следствие 2.4.1. Если множество дизъюнктов S содержит резольвенты всех своих элементов, то S выполнимо тогда и только тогда, когда 0S.

Задания для самостоятельной работы по теме 2.

1) Доказать тождественную истинность следующих формул:

1. (" х)(u(x) B(x))º (" x)u(x) (" x)B(x)

2. ($ x)(U(x) B(x)) º ($ x)U(x) ($ x)B(x)

3. ($ x)( $ y)P(x,y) º ($ y)( $ x)P(x,y)

4. (" x)( " y)P(x,y) º (" y)( " x)P(x,y)

5. ($ x)(P(x) Q(x)) º ($ x)P(x) ($ x)Q(x)

6. (" x)(P(x) Q(x)) º (" x)P(x) (" x)Q(x)

7. (" x)(P(x) Q(y)) º (" x)P(x) Q(y)

8. ($ x)(P(x) Q(y) º ($ x)P(x) Q(y)

9. ($ x)( " y)P(x,y) ® (" y)( $ x)P(x,y)

2) Выполнимы ли следующие формулы:

1. ($ x)P(x)

2. (" х)Р(х)

3. ($ х)( " у)(Q(x,x))

4. ($ x)( " y)(Q(x,y) ® (" z)R(x,y,z))

5. P(x) ® (" y)P(y)

3) Привести к предваренной нормальной форме

1. ($ x)($ y)P(x,y)® ($ x)($ y)Q(x,y)

2. ($ x)(" y)P(x,y)Ù ($ x)(" y)Q(x,y)

3. (" x) (A(x)® ($ y) B(y))

4) Перевести на русский язык:

1. ($ z)(z× z)=x

2. ($ z)(3z=x)

3. ($ y)(yy=x)

5) Для следующей интерпретации D={a,b}; P(a,a)=P(b,b)=И, P(a,b)=P(b,a)=Л определить истинностные значения следующих формул:

1. (" х)($ у)Р(х,y)

2. (" х)(" у)Р(х,y)

3. (" х)( " у)(Р(х,y) ® Р(y,х)