Намиране на частен случай на изпълнима хорнова цел, тъждествено верен във всички модели на дадено множество от положителни хорнови клаузи

Намиране на частен случай на изпълнима хорнова цел, тъждествено верен във всички модели на дадено множество от положителни хорнови клаузи

нека P е множество от положителни хорнови клаузи;

нека G и G са хорнови цели и нека ₁, ₂, …, _n е крайна редица от субституции;

ще казваме, че G е резолвентно достижима от G относно P чрез редицата от субституции ₁, ₂, …, _n, ако съществува такава редица G₀, G₁, …, G_n от хорнови цели, че:

1. 
   G₀ = G, G_n = G;
   
2. 
   за i = 1, 2, …, n G_i е непосредствена резолвента на G_i-1_i и някой частен случай на клауза от P;
   

ясно е, че редицата в дефиницията е резолвента редица относно P с начало G и край G;

пример: нека P = { p (a), p (f (f (X)) :– p (X) }; нека G = p (f (X));

строим резолвентна редица относно P с начало G:

G₀ = p (f (X)), G₁ = p (X), G₂ = true.

при това частният случай на G₀, който има непосредствена резолвента G₁ с втората клауза от P е G₀[X/f (X)] = p (f (f (X))); частният случай на G₁, който има непосредствена резолвента

G₂ = true с първата клауза от P е G₁[X/a] = p (a);

така празната цел true е достижима от G относно P чрез редицата от субституции [X/f (X)], [X/a];

₁, ₂, …, _n, то формулата G₁₂…_n е тъждествено вярна във всеки модел на P;

Доказателство: нека G = G₀, G₁, …, G_n = true е редица от хорнови цели, такава че за i = 1, 2, …, n G_i е непосредствена резолвента на

G_i-1_i и частен случай на клауза от P; с индукция по i = n, n-1, …0 ще покажем, че G_i_i+1_i+2…_n е тъждествено вярна във всеки

модел на P;

База: при i = n G_n_n+1…_n = G_n = true и формулата е вярна във всяка структура, в частност във всеки модел на P;

Предположение: нека 0 < i  n и G_i_i+1_i+2…_n е тъждествено вярна във всеки модел на P;

Стъпка: ще покажем, че G_i-1_i_i+1…_n е тъждествено вярна във всеки модел на P; имаме, че G_i е непосредствена резолвента на

G_i-1_i и частен случай на клауза от P; тогава импликацията

G_i  G_i-1_i е тъждествено вярна във всеки модел на P;

тогава всички частни случаи на G_i  G_i-1_i са тъждествено

вярни във всеки модел на P, в частност (G_i  G_i-1)_i_i+1_i+2…_n =

= G_i_i+1_i+2…_n  (G_i-1_i)(_i+1_i+2…_n) =

= G_i_i+1_i+2…_n  G_i-1_i_i+1…_n е тъждествено вярна във всеки модел на P (използвали сме асоциативност на умножението на субституции); по индукционното предположение G_i_i+1_i+2…_n е тъждествено вярна във всеки модел на P  G_i-1_i_i+1…_n е тъждествено вярна във всеки модел на P;

при i = 0 получаваме, че частният случай G₁₂…_n на G е тъждествено верен във всички модели на P;
пример: в горния пример, празната цел true е достижима от

G = p (f (X)) относно P чрез редицата от субституции [X/f (X)], [X/a];

тогава G([X/f (X)][X/a]) = p (f (f (X)))[X/a] = p (f (f (a))) е тъждествено вярна във всички модели на P;

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

нека P е множество от положителни хорнови клаузи;

казваме, че една атомарна формула A е резолвентно отстранима относно P, ако при всеки избор на атомарните формули

B₁, B₂, …, B_n (n  0) целта B₁ & B₂ & …& B_n е резолвентно достижима от A & B₁ & B₂ & … & B_n относно P;

Доказателство: нека B₁, B₂, …, B_n (n  0) са произволни атомарни формули; с индукция по дефиницията за изводимост ще покажем, че B₁ & B₂ & … & B_n е резолвентно достижима от

A & B₁ & B₂ & … & B_n относно P;

База: нека A е затворен частен случай на атомарна

формула C от P; тогава A & B₁ & B₂ & … & B_n има резолвента

B₁ & B₂ & …& B_n с C  B₁ & B₂ & …& B_n е резолвентно достижима от A & B₁ & B₂ & … & B_n относно P, т.е. A е резолвентно отстранима относно P;

Предположение: нека A :– C₁, C₂, …, C_m, m > 0 е затворен частен случай на клауза C от P и C₁, C₂, …, C_m са резолвентно отстраними относно P;

Стъпка: тогава A & B₁ & B₂ & …& B_n има непосредствена резолвента C₁ & C₂ & …& C_m & B₁ & B₂ & …& B_n с

A :– C₁, C₂, …, C_m  A & B₁ & B₂ & …& B_n има резолвента

C₁ & C₂ & …& C_m & B₁ & B₂ & …& B_n с C, т.е.

C₁ & C₂ & …& C_m & B₁ & B₂ & …& B_n е резолвентно достижима от

A & B₁ & B₂ & …& B_n относно P; по индукционното предположение C₁ е резолвентно отстранима относно P 

C₂ & …& C_m & B₁ & B₂ & …& B_n е резолвентно достижима от

C₁ & C₂ & …& C_m & B₁ & B₂ & …& B_n относно P; по индукционното предположение C₂ е резолвентно отстранима относно P 

C₃ & …& C_m & B₁ & B₂ & …& B_n е резолвентно достижима от

C₂ & C₃ & …& C_m & B₁ & B₂ & …& B_n относно P; след m стъпки получаваме, че B₁ & B₂ & …& B_n е резолвентно достижима от

C_m & B₁ & B₂ & …& B_n относно P; по транзитивността на резолвентната достижимост получаваме, че B₁ & B₂ & …& B_n е резолвентно достижима от A & B₁ & B₂ & …& B_n относно P;

така A е резолвентно отстранима относно P;

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

цел true;

Доказателство: първо ще проведем доказателството в частния случай когато G е затворена цел;

нека G = A₁ & A₂ & … & A_n, където A₁, A₂, …, A_n са затворени атомарни формули; тъй като G е изпълнима при P, то G е изпълнима в минималния ербранов модел S_P  A₁, A₂, …, A_n са вярни в S_P  A₁, A₂, …, A_n са изводими от P  (горната лема)

A₁, A₂, …, A_n са резолвентно отстраними относно P;

последователно получаваме: A₂ & A₃ & …& A_n е резолвентно достижима от A₁ & A₂ & …& A_n относно P; A₃ & A₄ & …& A_n е резолвентно достижима от A₂ & A₃ & …& A_n относно P;

след n стъпки получаваме, че празната цел true е резолвентно достижима от A_n относно P; по транзитивността на резолвентната достижимост получаваме, че празната цел true е достижима от G относно P;

нека G е произволна хорнова цел, която е изпълнима при P; тогава съществува затворен частен случай G ( - субституция) на G, който е верен във всички модели на P, т.е. G е изпълним при P и от горните разсъждения празната цел true е резолвентно достижима от G относно P, т.е. съществува резолвентна редица

G = G₀, G₁, …, G_k = true относно P;

при k = 0 имаме G = true  G = true и очевидно true е резолвентно достижима от G относно P;

при k > 0 разглеждаме редицата G, G₁, …, G_k = true; твърдим, че това е резолвентна редица относно P – трябва да проверим, че

G₁ е резолвента на G и някоя клауза от P; действително G има непосредствена резолвента G₁ със затворен частен случай на клауза C от P  G има резолвента G₁ с C; така празната цел true е резолвентно достижима от G относно P;