LOGIKA ALGORYTMICZNA 6. Paramodulacja.
W tym rozdziale zak ladamy, ˙ze r´owno´s´c (=) mo˙ze wyst¸epowa´c w dyzjunktach.
6.1. Niech C1 i C2 s¸a dyzjunktami bez wsp´olnych zmiennych i t b¸edzie termem wyst¸epuj¸acym w C1. Niech C1 = L ∨ C10, gdzie t wyst¸epuje w L, i C2 = C20 ∨ (r = s).
Niech σ jest najog´olniejszym unifikatorem zbioru {t, r}. Wtedy dyzjunkt C10σ ∪ C20σ ∪ {Lσ[sσ]} otrzymany przez zast¸epowanie tylko jednego wyst¸epowania tσ w Lσ przez sσ, nazywa si¸e binarnym paramodulantem, a litera ly L i r = s nazywaj¸a si¸e litera lami sparamodulowanymi.
Zadanie. Znale´z´c paramodulant binarny dyzjunkt´ow Q(x)∨P (g(f (x)))∨¬L(x, y) i (f (g(b)) = a) ∨ R(g(c)).
Paramodulantem dyzjunkt´ow C1 i C2 nazywa si¸e binarny paramodulant C1 (lub pewnego faktora dyzjunktu C1) z C2 (lub z pewnym faktorem dyzjunktu C2).
Uwaga. Je´sli C jest paramodulantem dyzjunkt´ow C1 i C2, to {C1, C2} |= C.
Zadanie. Znale´z´c wszystkie paramodulanty dyzjunkt´ow P (f (x, g(x))) ∨ Q(x) i (a = b) ∨ (g(a) = a) ∨ (f (a, g(a)) = b).
6.2. 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 C1, ..., Ck, ˙ze Ck = C i ka˙zdy Ci lub nale˙zy do S, lub jest rezolwent¸a lub paramodu- lantem dyzjunkt´ow wyst¸epuj¸acych przed Ci. W tym przypadku m´owimy, ˙ze C jest wyprowadzalny z S. Je´sli C jest dyzjunktem pustym 2, to powy˙zszy ci¸ag C1, ..., Ck nazywamy zaprzeczeniem zbioru S.
Drzewo dowodu dyzjunktu C odpowiadaj¸ace dowodowi C1, ..., Ck, z Ck = C, nazy- wamy drzewo binarne (rosn¸ace do g´ory), w kt´orym ka˙zdemu wierzcho lkowi jest przyp- isany pewien Cl, 1 ≤ l ≤ k, (Ck wyst¸epuje w korzeniu drzewa), i je´sli Ci i Cj s¸a bezpo´srednimi nast¸epnikami Cl, to w dowodzie C1, ..., Ck dyzjunkt Cl wyst¸epuje jako rezolwenta lub paramodulant dyzjunkt´ow Ci i Cj.
Twierdzenie o zupe lno´sci rachunku rezolucyjnego. Zbi´or dyzjunkt´ow S jest sprzeczny wtedy i tylko wtedy gdy dyzjunkt2 jest wyprowadzalny z rozszerzenia zbioru S ∪ {x = x} przez aksjomaty r´owno´sci postaci f (x1, ..., xn) = f (x1, ..., xn).
Zadanie. Znale´z´c dow´od rezolucyjny dyzjunktu C ze zbioru S (i narysowa´c odpowiednie drzewo dowodu), gdy:
C = 2 i S = {P (b) ∨ Q(a) , P (a) ∨ ¬Q(b) , ¬P (a) ∨ Q(b) , ¬P (b) ∨ ¬Q(a) , a = b}
6.3. Niech ≤P b¸edzie pewnym uporz¸adkowaniem symboli relacyjnych wyst¸epuj¸acych w S. Niech dyzjunkty C1 i C2 maj¸a tylko pozytywne litera ly. Wtedy paramodulant C dyzjunkt´ow C1 i C2 nazywa si¸e ≤P-hiperparamodulantem, je´sli litera ly sparamod- ulowane zawieraj¸a najwi¸eksze symbole wzgl¸edem ≤P w swoich dyzjunktach.
Dla ustalonego ≤P ci¸ag C1, ..., Ck nazywa si¸e ≤P-hiperdowodem dyzjunktu Ck ze zbioru S, je´sli ka˙zdy dyzjunkt Cinale˙zy do S lub jest ≤P-hiperrezolwent¸a (pozytywn¸a) lub ≤P-hiperparamodulantem z poprzednich dyzjunkt´ow.
Zadanie. Znale´z´c ≤P-dow´od dyzjunktu pustego2 ze zbioru ¬Q(a)∨¬R(a)∨(a = b) , Q(a) ∨ (a = b) , R(a) , f (a) 6= f (b) , f (x) = f (x). Zak ladamy, ˙ze =≤P R ≤P Q.
1
Twierdzenie o zupe lno´sci hiperrezolucji z hiperparamodulacj¸a. Dla ustalonego
≤P i dowolnego sprzecznego zbi´oru dyzjunkt´ow S istnieje ≤P-hiperdow´od dyzjunktu pustego 2 z rozszerzenia zbioru S ∪ {x = x} przez aksjomaty r´owno´sci postaci f (x1, ..., xn) = f (x1, ..., xn).
Zadanie. Znale´z´c ≤P-hiperdow´od zbioru 2 z nast¸epuj¸acego zbioru dyzjunkt´ow:
R(a) ∨ R(b) , ¬D(y) ∨ L(a, y) , ¬R(x) ∨ ¬Q(y) ∨ ¬L(x, y) , D(a) ∨ ¬Q(a) , Q(b) ∨ ¬R(b) , a = b.
Zak ladamy, ˙ze R <P Q <P D <P L <P=.
Powt´orzy´c zadanie dla R >P Q >P D >P L >P=.
6.4. Rezolucja liniowa. Dow´od rezolucyjny C1, ..., Cn dyzjunktu Cn ze zbioru dyzjunkt´ow S nazywa si¸e liniowym, je´sli ka˙zdy Ci+1 jest rezolwent¸a lub paramodu- lantem dyzjunktu Ci i pewnego dyzjunktu Bi nale˙z¸acego do S ∪ {C0, ..., Ci−1}.
Twierdzenie o zupe lno´sci rezolucji liniowej. Niech zbi´or dyzjunkt´ow S jest sprzeczny i C ∈ S. Je´sli S \ {C} jest niesprzeczny, to istnieje liniowy dow´od re- zolucyjny dyzjunktu pustego 2 z rozszerzenia zbioru S ∪ {x = x} przez aksjomaty r´owno´sci postaci f (x1, ..., xn) = f (x1, ..., xn). Przy tym C mo˙ze by´c wybrany jako dyzjunkt pocz¸atkowy.
Zadanie. Znale´z´c dow´od liniowy dyzjunktu2 z nast¸epuj¸acego zbioru dyzjunkt´ow:
{P (b) ∨ Q(a) , P (a) ∨ ¬Q(b) , ¬P (a) ∨ Q(b) , ¬P (b) ∨ ¬Q(a) , (a = b)}.
Znale´z´c dow´od2, w kt´orym pierwszy dyzjunkt jest pocz¸atkowy i dow´od w kt´orym a = b jest pocz¸atkowy.
2
