Намиране на частен случай на изпълнима хорнова цел, тъждествено верен във всички модели на дадено множество от положителни хорнови клаузи
нека P е множество от положителни хорнови клаузи;
нека G и G са хорнови цели и нека 1, 2, …, n е крайна редица от субституции;
ще казваме, че G е резолвентно достижима от G относно P чрез редицата от субституции 1, 2, …, n, ако съществува такава редица G0, G1, …, Gn от хорнови цели, че:
-
G0 = G, Gn = G;
-
за i = 1, 2, …, n Gi е непосредствена резолвента на Gi-1i и някой частен случай на клауза от P;
ясно е, че редицата в дефиницията е резолвента редица относно P с начало G и край G;
пример: нека P = { p (a), p (f (f (X)) :– p (X) }; нека G = p (f (X));
строим резолвентна редица относно P с начало G:
G0 = p (f (X)), G1 = p (X), G2 = true.
при това частният случай на G0, който има непосредствена резолвента G1 с втората клауза от P е G0[X/f (X)] = p (f (f (X))); частният случай на G1, който има непосредствена резолвента
G2 = true с първата клауза от P е G1[X/a] = p (a);
така празната цел true е достижима от G относно P чрез редицата от субституции [X/f (X)], [X/a];
Теорема: ако празната цел true е резолвентно достижима от хорнова цел G относно P чрез редицата от субституции
1, 2, …, n, то формулата G12…n е тъждествено вярна във всеки модел на P;
Доказателство: нека G = G0, G1, …, Gn = true е редица от хорнови цели, такава че за i = 1, 2, …, n Gi е непосредствена резолвента на
Gi-1i и частен случай на клауза от P; с индукция по i = n, n-1, …0 ще покажем, че Gii+1i+2…n е тъждествено вярна във всеки
модел на P;
База: при i = n Gnn+1…n = Gn = true и формулата е вярна във всяка структура, в частност във всеки модел на P;
Предположение: нека 0 < i n и Gii+1i+2…n е тъждествено вярна във всеки модел на P;
Стъпка: ще покажем, че Gi-1ii+1…n е тъждествено вярна във всеки модел на P; имаме, че Gi е непосредствена резолвента на
Gi-1i и частен случай на клауза от P; тогава импликацията
Gi Gi-1i е тъждествено вярна във всеки модел на P;
тогава всички частни случаи на Gi Gi-1i са тъждествено
вярни във всеки модел на P, в частност (Gi Gi-1)ii+1i+2…n =
= Gii+1i+2…n (Gi-1i)(i+1i+2…n) =
= Gii+1i+2…n Gi-1ii+1…n е тъждествено вярна във всеки модел на P (използвали сме асоциативност на умножението на субституции); по индукционното предположение Gii+1i+2…n е тъждествено вярна във всеки модел на P Gi-1ii+1…n е тъждествено вярна във всеки модел на P;
при i = 0 получаваме, че частният случай G12…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, ако при всеки избор на атомарните формули
B1, B2, …, Bn (n 0) целта B1 & B2 & …& Bn е резолвентно достижима от A & B1 & B2 & … & Bn относно P;
Лема: нека A е затворена формула, която е изводима от P; тогава A е резолвентно отстранима относно P;
Доказателство: нека B1, B2, …, Bn (n 0) са произволни атомарни формули; с индукция по дефиницията за изводимост ще покажем, че B1 & B2 & … & Bn е резолвентно достижима от
A & B1 & B2 & … & Bn относно P;
База: нека A е затворен частен случай на атомарна
формула C от P; тогава A & B1 & B2 & … & Bn има резолвента
B1 & B2 & …& Bn с C B1 & B2 & …& Bn е резолвентно достижима от A & B1 & B2 & … & Bn относно P, т.е. A е резолвентно отстранима относно P;
Предположение: нека A :– C1, C2, …, Cm, m > 0 е затворен частен случай на клауза C от P и C1, C2, …, Cm са резолвентно отстраними относно P;
Стъпка: тогава A & B1 & B2 & …& Bn има непосредствена резолвента C1 & C2 & …& Cm & B1 & B2 & …& Bn с
A :– C1, C2, …, Cm A & B1 & B2 & …& Bn има резолвента
C1 & C2 & …& Cm & B1 & B2 & …& Bn с C, т.е.
C1 & C2 & …& Cm & B1 & B2 & …& Bn е резолвентно достижима от
A & B1 & B2 & …& Bn относно P; по индукционното предположение C1 е резолвентно отстранима относно P
C2 & …& Cm & B1 & B2 & …& Bn е резолвентно достижима от
C1 & C2 & …& Cm & B1 & B2 & …& Bn относно P; по индукционното предположение C2 е резолвентно отстранима относно P
C3 & …& Cm & B1 & B2 & …& Bn е резолвентно достижима от
C2 & C3 & …& Cm & B1 & B2 & …& Bn относно P; след m стъпки получаваме, че B1 & B2 & …& Bn е резолвентно достижима от
Cm & B1 & B2 & …& Bn относно P; по транзитивността на резолвентната достижимост получаваме, че B1 & B2 & …& Bn е резолвентно достижима от A & B1 & B2 & …& Bn относно P;
така A е резолвентно отстранима относно P;
Теорема: нека P е множество от положителни хорнови клаузи;
ако G е хорнова цел, която е изпълнима при P, то празната цел true е резолвентно достижима от G относно P, т.е. съществува крайна резолвентна редица относно P с начало G и край празната
цел true;
Доказателство: първо ще проведем доказателството в частния случай когато G е затворена цел;
нека G = A1 & A2 & … & An, където A1, A2, …, An са затворени атомарни формули; тъй като G е изпълнима при P, то G е изпълнима в минималния ербранов модел SP A1, A2, …, An са вярни в SP A1, A2, …, An са изводими от P (горната лема)
A1, A2, …, An са резолвентно отстраними относно P;
последователно получаваме: A2 & A3 & …& An е резолвентно достижима от A1 & A2 & …& An относно P; A3 & A4 & …& An е резолвентно достижима от A2 & A3 & …& An относно P;
след n стъпки получаваме, че празната цел true е резолвентно достижима от An относно P; по транзитивността на резолвентната достижимост получаваме, че празната цел true е достижима от G относно P;
нека G е произволна хорнова цел, която е изпълнима при P; тогава съществува затворен частен случай G ( - субституция) на G, който е верен във всички модели на P, т.е. G е изпълним при P и от горните разсъждения празната цел true е резолвентно достижима от G относно P, т.е. съществува резолвентна редица
G = G0, G1, …, Gk = true относно P;
при k = 0 имаме G = true G = true и очевидно true е резолвентно достижима от G относно P;
при k > 0 разглеждаме редицата G, G1, …, Gk = true; твърдим, че това е резолвентна редица относно P – трябва да проверим, че
G1 е резолвента на G и някоя клауза от P; действително G има непосредствена резолвента G1 със затворен частен случай на клауза C от P G има резолвента G1 с C; така празната цел true е резолвентно достижима от G относно P;
Сподели с приятели: |