Резолюция между хорнова цел и хорнова клауза

Резолюция между хорнова цел и хорнова клауза

C = A₁ :– B₁ & B₂ & … & B_n (n  0) е положителна хорнова клауза;

образуваме G = B₁ & B₂ & … & B_n & A₂ & A₃ & … & A_m; целта G наричаме непосредствена резолвента на хорновата цел G и положителната хорнова клауза C;

ще покажем, че ако G и C са вярни в дадена структура S при оценка v, то G също е вярна в S при оценката v;

G ^{S, v} = 1  B₁^{S, v} = B₂^{S, v} = … = B_n^{S, v} = 1, C^{S, v} = 1  A₁^{S, v} = 1,

A₂^{S, v} = A₃^{S, v} = … = A_m^{S, v} = 1 (тъй като G ^{S, v} = 1) 

G^{S, v} = (A₁ & A₂ & … & A_m)^{S, v} = 1;

като следствие, ако C е тъждествено вярна в S, то импликацията

G  G е тъждествено вярна в S;
нека G и C имат непосредствена резолвента G; тогава за всяка субституция , G и C имат непосредствена резолвента G :

действително G = A₁ & A₂ & … & A_m и

C = A₁ :– B₁ & B₂ & … & B_n имат непосредствена резолвента

B₁ & B₂ & … & B_n & A₂ & A₃ & … & A_m = G;

всяка хорнова цел G, която е непосредствена резолвента на някой частен случай на G и някой частен случай на C наричаме резолвента на G и C; ще отбележим, че частните случаи на G и C може да се получават от различни субституции; ясно е, че

ако G е непосредствена резолвента на G и C, то G е

резолвента на G и C;

очевидно G и C нямат непосредствена резолвента;

имаме G[X/f (f (X))] = p (f (f (X))) & p (f (f (f (X))));

така частният случай G[X/f (f (X))] на G и частният случай C на C имат непосредствена резолвента – p (X) & p (f (f (f (X)))) 

G и C имат резолвента p (X) & p (f (f (f (X))));
Твърдение: нека G и C имат резолвента G; нека C е тъждествено вярна в дадена структура S; тогава, ако G е изпълнима в S, то G също е изпълнима в S;

Доказателство: нека ₁, ₂ са субституции и G е непосредствена резолвента на G₁ и C₂; тъй като C е тъждествено вярна в S, то

C₂ е тъждествено вярна в S  G  G₁ е тъждествено вярна в S;

тъй като G е изпълнима в S  съществува оценка v в S, така че

G ^{S, v} = 1; имаме (G  G₁)^{S, v} = 1  (G₁)^{S, v} = 1, т.е. G₁ е изпълнима в S  G е изпълнима в S, тъй като един неин частен случай е изпълним в S;
Твърдение: нека P е множество от положителни хорнови клаузи; нека G е хорнова цел; нека G има резолвента G с някоя клауза

от P; в такъв случай, ако G е изпълнима при P, то G е изпълнима при P;

Доказателство: нека S е произволен модел на P; тъй като G е изпълнима при P  G е изпълнима в S; G е резолвента на G и някаква клауза C от P, която е тъждествено вярна в S, тъй като S е модел на P; от горното твърдение G е изпълнима в S; така G е изпълнима във всеки модел на P, т.е. G е изпълнима при P;
нека P е множество от положителни хорнови клаузи; резолвентна редица относно P наричаме всяка редица G₁, G₂, …(крайна или безкрайна) от хорнови цели, в която за i = 2, 3, …G_i е резолвента на G_i-1 и някоя клауза от P; считаме, че всяка редица от един член е резолвентна;
Твърдение: ако G₁, G₂, … е резолвентна редица относно P и за някое n  N G_n е изпълнима при P, то G₁, G₂, …, G_n-1 са изпълними при P;

Доказателство: следва непосредствено от предното твърдение;

нека G = p (f (X)); строим резолвентна редица с начало G относно P;

ясно е, че G няма резолвента с p (a), тъй като всеки частен случай на G съдържа функционален символ; една резолвента на G и втората клауза е p (X), която е непосредствена резолвента на

G[X/f (X)] и клаузата; сега p (X)[X/a] = p (a) и тогава p (X) и p (a) имат резолвента true; получаваме следната резолвентна редица:

p (f (X)), p (X), true.

от горното следствие G = p (f (X)) е изпълнима при P;

нека G = p (X) & p (f (X)); отново строим резолвентна редица с начало G относно P; G[X/a] = p (a) & p (f (a))  G има резолвента

p (f (a)) с p (a); ясно е, че p (f (a)) няма резолвента с никоя от клаузите от P; така получихме редицата

p (X) & p (f (X)), p (f (a)).

G[X/f (f (X))] = p (f (f (X))) & p (f (f (f (X))))  G има резолвента

p (X) & p (f (f (f (X)))) с втората клауза; p (X) & p (f (f (f (X))))[X/a] =

= p (a) & p (f (f (f (a)))) има резолвента p (f (f (f (a)))) с първата клауза;

p (f (f (f (a)))) има резолвента само с втората клауза и тя е p (f (a)); така получаваме редицата

p (X) & p (f (X)), p (X) & p (f (f (f (X)))), p (f (f (f (a)))), p (f (a)).

ако използваме само втората клауза ще получим една безкрайна резолвентна редица:

p (X) & p (f (X)), p (X) & p (f³ (X)), p (X) & p (f⁵ (X)), p (X) & p (f⁷ (X)), …;

нека G и G са хорнови цели; ще казваме, че G е резолвентно достижима от G относно P, ако съществува крайна резолвентна редица относно P с първи член G и последен член G;

рефлексивност: за всяка хорнова цел G, G е резолвентно достижима от G относно P – действително редицата с един член G е резолвентна относно P с начало G и край G;

транзитивност: ако G е резолвентно достижима от G относно P и G е резолвентно достижима от G относно P, то G е резолвентно достижима от G относно P – достатъчно е да комбинираме двете резолвентни редици;