LOGIKA ALGORYTMICZNA 5. Rachunek rezolucyjny.

LOGIKA ALGORYTMICZNA 5. Rachunek rezolucyjny.

W tym rozdziale zak ladamy, ˙ze r´owno´s´c (=) nie wyst¸epuje w dyzjunktach.

Je´sli pewien unifikowalny podzbi´or dyzjunktu D zawiera przynajmniej dwa lit- era ly i σ jest jego najog´olniejszym unifikatorem, to dyzjunkt Dσ nazywamy faktorem dyzjunktu D. Faktor sk ladaj¸acy si¸e z jednego litera lu nazywamy faktorem jednos- tkowym.

5.1. Zadanie. Znale´z´c faktor dyzjunktu ¬Q(a, x) ∨ P (y) ∨ ¬Q(y, f (y)).

Niech C₁ i C₂ s¸a dyzjunktami bez wsp´olnych zmiennych (sytuacja ta jest osi¸agalna przez r´ownowa˙zno´sci 1.6 Listy 1). Je´sli dla pewnych litera l´ow L₁ ∈ C₁ i L₂ ∈ C₂zbi´or {L1, ¬L2} ma najog´olniejszy unifikator σ, to dyzjunkt (C1σ\L1σ)∪(C2σ\L2σ) nazywa si¸e binarn¸a rezolwent¸a, a litera ly L₁ i ¬L₂ nazywaj¸a si¸e litera lami odcinanymi.

5.2. Zadanie. Znale´z´c rezolwent¸e binarn¸a dyzjunkt´ow ¬Q(y) ∨ ¬P (x) ∨ ¬L(x, y) i P (a) ∨ R(x).

Rezolwent¸a dyzjunkt´ow C₁ i C₂ nazywa si¸e binarna rezolwenta C₁ (lub pewnego faktora dyzjunktu C₁) z C₂ (lub z pewnym faktorem dyzjunktu C₂).

5.3. Uwaga. Je´sli C jest rezolwent¸a dyzjunkt´ow C₁ i C₂, to {C₁, C₂} |= C.

5.4. Zadanie. Znale´z´c rezolwent¸e dyzjunkt´ow ¬Q(g(a), b) i Q(g(x), b) ∨ Q(y, z) ∨ R(x).

Niech S b¸edzie zbiorem dyzjunkt´ow, a C b¸edzie pewnym dyzjunktem. Dowodem rezolucyjnym dyzjunktu C ze zbioru S nazywamy taki ci¸ag dyzjunkt´ow C₁, ..., C_k, ˙ze C_k = C i ka˙zdy C_i lub nale˙zy do S, lub jest rezolwent¸a dyzjunkt´ow wyst¸epuj¸acych przed C_i. W tym przypadku m´owimy, ˙ze C jest wyprowadzalny z S. Je´sli C jest dyzjunktem pustym 2, to powy˙zszy ci¸ag C1, ..., C_k nazywamy zaprzeczeniem zbioru S.

Drzewo dowodu dyzjunktu C odpowiadaj¸ace dowodowi C₁, ..., C_k, z C_k = C, nazy- wamy drzewo binarne (rosn¸ace do g´ory), w kt´orym ka˙zdemu wierzcho lkowi jest przyp- isany pewien C_l, 1 ≤ l ≤ k, (C_k wyst¸epuje w korzeniu drzewa), i je´sli C_i i C_j s¸a bezpo´srednimi nast¸epnikami C_l, to w dowodzie C₁, ..., C_k dyzjunkt C_l wyst¸epuje jako rezolwenta dyzjunkt´ow C_i i C_j.

5.5. Zadanie. Znale´z´c dow´od rezolucyjny dyzjunktu C ze zbioru S (i narysowa´c odpowiednie drzewo dowodu), gdy:

(a) C = ¬L(a, b) , S = {P (a) , Q(b) , ¬P (x) ∨ ¬Q(y) ∨ ¬L(x, y)};

(b) C = 2 , S = {P (a) , Q(a) , ¬P (x) ∨ ¬R(x) , ¬Q(x) ∨ W (x) , ¬Q(x) ∨ R(x)};

(c) C = 2 , S = {¬E(x) ∨ Q(x) ∨ R(x, f(x)) , ¬E(x) ∨ Q(x) ∨ T (f(x)) , P (a) , E(a) , ¬R(a, y) ∨ P (y) , ¬P (x) ∨ ¬Q(x) , ¬P (x) ∨ ¬T (x)}.

5.6. Twierdzenie o zupe lno´sci rachunku rezolucyjnego. Zbi´or dyzjunkt´ow S jest sprzeczny wtedy i tylko wtedy gdy dyzjunkt 2 jest wyprowadzalny z S (tzn.

S jest zaprzeczalny).

1

Niech B = {B₁, B₂, ..., B_i, ...} b¸edzie baz¸a Herbranda zbioru dyzjunkt´ow S. Ustalmy pewn¸a H-struktur¸e M i odpowiedni ci¸ag B_M = {B₁^ε1, B₂^ε2, ..., B_i^εi, ...}, gdzie ε_j ∈ {0, 1}, B_j¹ := B_j i B_j⁰ := ¬B_j (zak ladamy, ˙ze B_i^ε ∈ B_M, je´sli M |= B_i^ε). Niech ≤_P b¸edzie pewnym uporz¸adkowaniem symboli relacyjnych wyst¸epuj¸acych w S.

(≤_P B_M)-Sprzeczno´sci¸a nazywamy sko´nczony zbi´or sk ladaj¸acy si¸e z dyzjunkt´ow- elektron´ow E₁, ..., E_q, 1 ≤ q, i dyzjunktu-j¸adra N takich, ˙ze spe lnione s¸a nast¸epuj¸ace warunki:

(1) E₁, ..., E_q s¸a falszywe wzgl¸edem B_M;

(2) zak ladaj¸ac, ˙ze R₁ = N i dla i ≤ q, R_i+1 jest rezolwent¸a R_i i E_i, mamy:

(a) litera l odcinany na kroku i ma najwi¸ekszy symbol relacyjny w Ei

wzgl¸edem ≤_P;

(b) R_q+1 jest falszywy wzgl¸edem B_M.

W tym przypadku m´owimy, ˙ze R_q+1 jest (≤_P B_M)-rezolwent¸a (≤_P B_M)-sprzeczno´sci {E₁, ..., E_q, N }.

Uwaga. W tej sytacji j¸adro N ma podstawowy przyk lad spe lniony w M .

5.7. Zadanie. Znale´z´c (≤_P B_M)-rezolwent¸e (je´sli istnieje) nast¸epuj¸acych (≤_P B_M)-sprzeczno´sci

(a) {E₁, E₂, N }, gdzie S <_P R <_P Q , E₁ = ¬Q(z) ∨ ¬Q(a) , E₂ = R(b) ∨ S(c) , N = Q(x) ∨ Q(a) ∨ ¬R(y) ∨ ¬R(b) ∨ S(c) i

B_M = {Q(a), Q(b), Q(c), ¬R(a), ¬R(b), ¬R(c), ¬S(a), ¬S(b), ¬S(c)}.

(b) {E₁, E₂, E₃, N }, gdzie P <_P Q <_P R <_P W , E₁ = P (a) , E₂ = Q(a) , E₃ = R(a) , N = ¬P (a) ∨ ¬Q(a) ∨ ¬R(a) ∨ ¬W (a) i B_M = {¬P (a), ¬Q(a), ¬R(a), W (a)}.

(c) {E₁, E₂, N }, gdzie S <_P R <_P Q <_P P , E₁ = P (a) , E₂ = Q(a, b) ∨ S(b, c) , N = R(x) ∨ ¬P (x) ∨ ¬Q(x, y) i B_M = {¬P (a), P (b), ¬Q(a, b), ¬S(b, c), ¬R(a)}.

Rezolucja semantyczna. Dla ustalonych ≤_P i B_M ci¸ag C₁, ..., C_k nazywa si¸e (≤_P B_M)-dowodem dyzjunktu C_k ze zbioru S, je´sli ka˙zdy dyzjunkt C_i nale˙zy do S lub jest (≤_P B_M)-rezolwent¸a (≤_P B_M)-sprzeczno´sci sk ladaj¸acej si¸e z poprzednich dyzjunkt´ow.

W przypadku, gdy B_M sk lada si¸e tylko z litera l´ow negatywnych, rezolucja seman- tyczna nazywa si¸e hiperrezolucj¸a pozytywn¸a.

W przypadku, gdy B_M sk lada si¸e tylko z litera l´ow pozytywnych, rezolucja seman- tyczna nazywa si¸e hiperrezolucj¸a negatywn¸a.

5.8. Zadanie. Znale´z´c (≤_P B_M)-dow´od dyzjunktu pustego 2 ze zbioru {A(a) ∨ B(a) , A(a) ∨ ¬B(a) , ¬A(a) ∨ B(a) , ¬A(a) ∨ ¬B(a)} , gdzie A <_P B i B_M = {A(a), ¬B(a)}. Rozpatrzy´c przypadki B ≤_P A i B_M = {A(a), B(a)}.

5.9. Twierdzenie o zupe lno´sci rezolucji semantycznej. Dla ustalonych ≤_P i B_M ka˙zdy sprzeczny zbi´or dyzjunkt´ow S ma (≤_P B_M)-dow´od dyzjunktu pustego 2.

5.10. Rezolucja liniowa. Dow´od rezolucyjny C1, ..., Cn dyzjunktu Cn ze zbioru dyzjunkt´ow S nazywa si¸e liniowym, je´sli ka˙zdy C_i+1 jest rezolwent¸a C_i i pewnego dyzjunktu B_i nale˙z¸acego do S ∪ {C₀, ..., C_i−1}.

2

Zadanie. Znale´z´c dow´od liniowy dyzjunktu2 z nast¸epuj¸acych zbior´ow dyzjunkt´ow:

(a) {A(a) ∨ B(a) , A(a) ∨ ¬B(a) , ¬A(a) ∨ B(a) , ¬A(a) ∨ ¬B(a)}.

(b) {M (a, s(c), s(b)) , P (a) , M (x, x, s(x)) , ¬M (x, y, z) ∨ M (y, x, z) , D(x, z) ∨

¬M (x, y, z) , ¬P (x) ∨ ¬M (y, z, u) ∨ ¬D(x, u) ∨ D(x, y) ∨ D(x, z) , ¬D(a, b)}.

(c) ze zbior´ow S zada´n 5.5(b,c).

5.11. Input-rezolucja i unit-rezolucja. Dow´od rezolucyjny C₁, ..., C_ndyzjunktu C_nze zbioru dyzjunkt´ow S nazywa si¸e input-dowodem, je´sli ka˙zdy C_i+1jest rezolwent¸a dw´och dyzjunkt´ow ze zbioru S ∪ {C₀, ..., C_i}, przy tym jeden z nich nale˙zy do S.

Dow´od rezolucyjny C₁, ..., C_n dyzjunktu C_n ze zbioru dyzjunkt´ow S nazywa si¸e unit-dowodem, je´sli ka˙zdy C_i+1 jest rezolwent¸a dw´och dyzjunkt´ow ze zbioru S ∪ {C₀, ..., C_i}, przy tym jeden z nich wyst¸epuje w postaci faktora jednostkowego.

Uwaga. Input-rezolucja i unit-rezolucja nie s¸a zupe lne.

Twierdzenie. Zbi´or dyzjunkt´ow S ma input-zaprzeczenie wtedy i tylko wtedy, gdy ma unit-zaprzeczenie.

Zadanie. Znale´z´c input- i unit-dowody dyzjunktu 2 z nast¸epuj¸acych zbior´ow dyzjunkt´ow:

(a) {P (s(x), x, e), P (e, x, x) , ¬P (x, y, u) ∨ ¬P (y, z, v) ∨ ¬P (u, z, w) ∨ P (x, v, w) ,

¬P (x, y, u) ∨ ¬P (y, z, v) ∨ ¬P (x, v, w) ∨ P (u, z, w) , ¬P (a, x, e)}.

(b) {D(x, x) , ¬D(x, y) ∨ ¬D(y, z) ∨ D(x, z) , P (x) ∨ D(g(x), x) , P (x) ∨ L(l, g(x)) , P (x) ∨ L(g(x), x) , L(l, a) , ¬P (x) ∨ ¬D(x, a) , ¬L(l, x) ∨ ¬L(x, a) ∨ P (f (x)) ,

¬L(l, x) ∨ ¬L(x, a) ∨ D(f (x), x)}.

3