lec10

Пусть S – множество дизъюнктов Ci.

S = {C1, C2, … Ci, … Cn}

Резольвентой множества S – R(S) (или Res(S)) называется множество

R(S) = S {D},

где D – резольвента дизъюнктов Ci, Cj: 1≤i,j≤n.

Пример 10.6.

S = {{A, B, C},{B,D},{ A, D}}.

резольвента по (A/ A), где C1 = {A, B, C}, C3 = { A, D}

{C1\{A}} {C3\{ A}} = { B, C} { D} = { B, C, D} или запись

Res((A B C),( A D)) = B C D и т.д.

R(S) = {A, B, C},{B,D},{ A, D},{A,D, C},{B, A},{ B, C, D}

31

Последовательно применяя метод резольвент получим множества:

R0(S) = S, R1(S) = R0(S) R(S), R2(S) = R1(S) R(R1(S)), … … Rn(S) = Rn-1(S) R(Rn-1(S)).

затем объединив все множества можем получить R*(S):

R*(S) = ∞n=1 Rn S

!!! R*(S) конечно тогда и только тогда, когда S конечно.

Содержательная подоплёка метода резолюции: если истинное означивание подтверждает дизъюнкты С1 и С2 , то оно также подтверждает их резольвенту D. Аналогично, если истинностное означивание подтверждает множество S, то оно также подтверждает R(S).

!!! Res(C1,С2) содержит меньше информации, чем сами дизъюнкты С1 и С2.

Пример 10.7.

S = {{A,B},{ B}}. D = R(S) = {A}.

Резольвент не содержит никакой информации о литерале В.	32

Пример 10.8.

S = {{ A,B, C},{A, D},{ B,D}}.

D1 = { A,B, C}, D2={A, D}, D3={ B,D}.

D4	- резольвента D1,D2		по (A/ A)):	D = {B, C, D}
				4
D5	- резольвента D2,D3	по (D/ D)):		D5	= {A, B}
D6	- резольвента D1,D3	по (B/ B)):		D6	= { A, C,D}
D7 - (резольвента D4,D5			по (B/ B)):	D7 = {A, C, D}
D8 - (резольвента D6,D7			по (A/ A)):	D8 = { C, D, C, D} = { C, D, D}

D8 = { C, D, D} = ( C D D) ≡1

Т.е. КНФ для S истинна для любых значений A,B,C,D.

33

Пусть S – множество дизъюнктов.

Резолюционным выводом из S назовём такую конечную последовательность дизъюнктов C1, C2, … Ci, … Cn, что для каждого Ci (1≤i≤n):

Ci S, либо

Ci R({Cj,Ck}) при 1≤j,k<i.

Дизъюнкт C считается резолютивно выводимым из S, если существует резолютивный вывод из S, последний дизъюнкт которого – С = Cn. Очевидно что C R*(S). Этот факт обозначается:

S ⱶR С

Пустой дизъюнкт является всегда неподтверждённым. Обозначение: □.

Множество дизъюнктов S не подтверждаемо (или невыполнимо) тогда и только тогда, когда R*(S) содержит пустой дизъюнкт:

□ R*(S).

.

34

Т.о. применяя метод резолюции к множеству S получаем пустой дизъюнкт, то множество S будет неподтверждаемым.

Так как правило резолюции – это выводимое правило логики высказываний, то можно использовать теорему 10.2 дедукции, по которой

{S K} ⱶ L S ⱶ (К→L)

{S B} ⱶ □ S ⱶ ( B → □)

{S B } ⱶ □ S ⱶ B □

S ⱶ B (S B) ⱶ □

35

Пример 10.9. Резолютивный вывод высказывания B: S ⱶR B.

S = {{A, B},{ A, B, C},{ A, B,C}}.

Доказать, что высказывание B резолютивно выводимо из множества S.

D1	= {A, B}
D2	= { A, B, C}
D3	= { A, B,C}

D4 - резольвента D1,D2	по (A/ A)):
D5 - резольвента D1,D3	по (A/ A)):
D6 - резольвента D2,D3	по (C/ C)):

D7 - (резольвента D4,D5 по (C/ C)):

D4 = { B, B, C} = { B, C} D5 = { B, B,C} = { B,C}

D6 = { A, B, A, B} = { A, B} D7 = { B}

Итог: S ⱶR B

36