Твърдение: ако A и B са две унифицируеми атомарни формули, то измежду техните унификатори има най-общ, т.е. съществува унификатор на A и B, така че всички унификатори на A и B
са , където е произволна субституция;
Доказателство: тъй като A и B са унифицируеми,
то A = p (T1, T2, …, Tn), B = (U1, U2, …, Un), n 0;
при n = 0 очевидно тъждествената субституция е най-общ унификатор на A и B;
нека n 1; тогава унификаторите на A и B са решенията на системата T1 = U1, …, Tn = Un; тази система има решение, тъй като A и B са унифицируеми, така че тя притежава общо решение и всички други решения на системата са , където е произволна субституция; така е най-общ унификатор на A и на B;
Най-обща резолвента на хорнова цел и хорнова клауза
нека G е хорнова цел, C е положителна хорнова клауза;
под най-обща резолвента на G и C разбираме такава резолвента R на G и C, че всички други резолвенти на G и C
са частни случаи на R; ясно е, че ако R е най-обща резолвента на
G и C, то частните случаи на R и само те са резолвентите на G и C;
действително, ако R е резолвента на G и C, т.е. R е непосредствена резолвента на G и C, то R е непосредствена резолвента на
G и C, т.е. R е резолвента на G и C;
Твърдение: ако една хорнова цел G и положителна хорнова
клауза C имат резолвента, то те имат и най-обща резолвента;
Доказателство: нека G и C имат резолвента; разглеждаме вариант
C на C, такъв че VAR (G) VAR (C) = ; тъй като частните случаи на C и C са едни и същи, то резолвентите на G и C и резолвентите на G и C са едни и същи; така от това че G и C имат резолвента
G и C също имат резолвента; имаме, че частен случай на G съвпада с частен случай на C частен случай на първия член
на G съвпада с частен случай на заключението на C, но
VAR (G) VAR (C) = първия член на G и заключението на C са унифицируеми атомарни формули; нека е най-общ унификатор на първия член на G и заключението на C;
разглеждаме формулите G и C; те имат непосредствена резолвента, тъй като първия член на G съвпада със заключението на C; нека R е непосредствена резолвента на G и C;
ясно е, че R е резолвента на G и C; ще покажем, че R е най-обща резолвента на G и C;G sdf нека R е произволна резолвента на G и C, т.е. R е непосредствена резолвента на G1 и C2 за някои субституции
1, 2 (отновно използваме, че частните случаи на C и C са едни и същи); дефинираме (x) = 1 (x), ако x VAR (G) и (x) = 2 (x), ако
x \VAR (G); е субституция, тъй като от (x) x следва
1 (x) x или 2 (x) x, но 1 (x) x или 2 (x) x за краен брой променливи, така че (x) x за краен брой променливи;
тъй като и 1 съвпадат върху VAR (G), то G = G1;
и 2 съвпадат върху VAR (C), тъй като VAR (C) VAR (G) =
VAR (C) \VAR (G); така C = C2; така R е непосредствена резолвента на G и C първият член на G и заключението на
C съвпадат е унификатор на първия член на G и заключението на C; от друга страна е най-общ унификатор на първия член на G и заключението на C = за някоя субституция ; така G = G, C = C; имаме, че R е непосредствена резолвента на G и C R е непосредствена резолвента на G = G и C = C, т.е. R = R;
така R е най-обща резолвента на G и C;
ясно е, че най-общата резолвента на хорнова цел и положителна хорнова клауза е определена с точност до вариант;
Пълнота на резолюцията между хорнови цели и хорнови клаузи при използване на канонични резолвентни редици
нека P е множество от положителни хорнови клаузи;
редицата от хорнови цели G0, G1, …, Gn, …наричаме канонична резолвентна редица относно P, ако за всяко i = 1, 2, …, n, …
имаме Gi е най-обща резолвента на Gi-1 с някоя клауза от P;
нека C1, C2, …, Cn е редица от положителни хорнови клаузи;
резолвентна редица, съответна на редицата C1, C2, …, Cn наричаме редица G0, G1, …, Gn от хорнови цели, така че за
i = 1, 2, …, n имаме Gi е резолвента на Gi-1 и Ci;
казваме още, че Gn е резолвентно достижима от G0 чрез редицата C1, C2, …, Cn или, че Gn е резолвента на G0 с редицата
C1, C2, …, Cn;
нека C1, C2, …, Cn е редица от положителни хорнови клаузи;
канонична резолвентна редица, съответна на редицата
C1, C2, …, Cn наричаме редица G0, G1, …, Gn от хорнови цели, така че за i = 1, 2, …, n имаме Gi е най-обща резолвента на Gi-1 и Ci;
казваме още, че Gn е канонично резолвентно достижима от G0 чрез редицата C1, C2, …, Cn или, че Gn е канонична резолвента на G0 с редицата C1, C2, …, Cn;
Твърдение: нека G има канонична резолвента G с редицата от положителни хорнови клаузи C1, C2, …, Cn; тогава G е най-обща измежду резолвентите на G с редицата C1, C2, …, Cn;
Доказателство: нека G = G0, G1, …, Gn = G е канонична резолвента редица, съответна на редицата C1, C2, …, Cn, т.е. за i = 1, 2, …, n
Gi е най-обща резолвента на Gi-1 и Ci; нека R е произволна резолвента на G с редицата C1, C2, …, Cn;
нека G = R0, R1, …, Rn = R е резолвентна редица, съответна на редицата C1, C2, …, Cn, т.е. за i = 1, 2, …, n Ri е резолвента на
Ri-1 и Ci; с индукция по i = 1, 2, …, n ще покажем, че Ri е частен случай на Gi; в частност при i = m получаваме, че R е частен случай на G, което доказва твърдението;
База: при i = 0 имаме R0 = G0 = G и очевидно R0 е частен
случай на G0;
Предположение: нека 1 i n и Ri-1 е частен случай на Gi-1;
Стъпка: от индукционното предположение Ri-1 е частен случай на Gi-1 и Ri е резолвента на Ri-1 и Ci, то Ri е резолвента на Gi-1 и Ci;
от друга страна Gi е най-обща резолвента на Gi-1 и Ci Ri е частен случай на Gi;
Теорема: нека G има резолвента с редицата от положителни хорнови клаузи C1, C2, …, Cn; тогава G има канонична резолвента с редицата C1, C2, …, Cn;
Доказателство: провеждаме индукция по n;
База: при n = 1 G има резолвента с C1 G има най-обща резолвента G1 с C1 и G, G1 е канонична резолвентна редица относно едночленната редица C1;
Предположение: нека 1 m < n и е изпълнено, че ако G има резолвента с редицата C1, C2, …, Cm, то G има канонична резолвента с редицата C1, C2, …, Cm;
Стъпка: нека G има резолвента с редицата C1, C2, …, Cm, Cm+1;
ясно е, че в такъв случай G има резолвента G с редицата
C1, C2, …, Cm и G има резолвента G с Cm+1; от индукционното предположение G има канонична резолвента R с C1, C2, …, Cm и от предното твърдение G е частен случай на R; при това положение
R има резолвента G с Cm+1, тъй като всеки частен случай на G е частен случай на R R има най-обща резолвента R с Cm+1;
тъй като R е канонична резолвента на G с редицата
C1, C2, …, Cm и R е най-обща резолвента на R и Cm+1, то
R е канонична резолвента на G с редицата C1, C2, …, Cm, Cm+1;
да разгледаме един пример;
нека е дадено следното множество от положителни хорнови клаузи: P = { p (f (f (X)), f (X)) ; p (X, f (Y)) :– p (X, f (Z)), p (Y, Z) };
нека G е хорновата цел p (U, U);
питаме се дали G e изпълнима при P; за тази цел true трябва да е резолвентно достижима от G относно P и тогава true трябва да е канонично резолвентно достижима относно P;
търсим най-обща резолвента на G с първата клауза;
тъй като G и първата клауза нямат общи променливи, не е нужно да образуваме вариант на клаузата; решаваме следната система от термове: U = f (f (X)), U = f (X) (заместване) f (X) = f (f (X)), U = f (X)
(разпадане) X = f (X), U = f (X); получихме явно нерешима система; така G няма резолвента с първата клауза;
търсим най-обща резолвента на G с втората клауза;
отново няма нужда от вариант на клаузата; решаваме следната система от термове: U = X, U = f (Y) (заместване) U = X, X = f (Y)
(заместване) U = f (Y), X = f (Y); получихме система в решен вид и нейното общо решение е субституцията [U/f (Y), X/f (Y)], която е най-общ унификатор на атомарните формули p (X, f (Y)) и p (U, U);
частните случаи p (f (Y), f (Y)) :– p (f (Y), f (Z)), p (Y, Z) и
p (f (Y), f (Y)) на втората клауза и G имат непосредствена резолвента
p (f (Y), f (Z)), p (Y, Z), която е най-обща резолвента на G и втората клауза; да означим с G1 новата цел p (f (Y), f (Z)), p (Y, Z);
търсим най-обща резолвента на G1 с първата клауза;
тъй като G1 няма общи променливи с първата клауза, няма нужда да образуваме вариант на клаузата; решаваме следната система от термове: f (Y) = f (f (X)), f (Z) = f (X) (разпадане) Y = f (X), f (Z) = f (X) (разпадане) Y = f (X), Z = X; получихме система в решен вид и нейното общо решение е субституцията [Y/f (X), Z/X], която е
най-общ унификатор на атомарните формули p (f (Y), f (Z)) и
p (f (f (X)), f (X)); така частните случаи p (f (f (X)), f (X)) и
p (f (f (X)), f (X)), p (f (X), X) на първата клауза и целта G1 имат непосредствена резолвента p (f (X), X), която е най-обща резолвента на първата клауза и G1; да означим с G2 новата цел p (f (X), X);
търсим най-обща резолвента на G2 с първата клауза;
тъй като G2 и първата клауза имат общи променливи, трябва да вземем вариант на клаузата, който няма общи променливи с G2, например p (f (f (T)), f (T)); решаваме следната система от термове:
f (X) = f (f (T)), X = f (T) (разпадане) X = f (T), X = f (T) (заместване) f (T) = f (T), X = f (T) (премахване на тъждество)
X = f (T); получихме система в решен вид с най-общо решение
субституцията [X/f (T)], която е най-общ унификатор на атомарните формули p (f (f (T)), f (T)) и p (f (X), X); така частните случаи p (f (f (T)), f (T)) и p (f (f (T)), f (T)) на първата клауза и целта G2 имат непосредствена резолвента празната цел true, така че първата клауза има резолвента true с целта G2;
получихме канонична резолвентна редица G, G1, G2, true относно двете клаузи G е изпълнима при P, т.е. G е изпълнима във всички модели на P;
за да намерим частен случай на G, който е тъждествено верен във всички модели на P образуваме композиция на субституциите
[U/f (Y), X/f (Y)][Y/f (X), Z/f (X)][X/f (T)] =
= [U/f (f (f (T))), X/f (f (f (T))), Y/f (f (T)), Z/f (f (T))] = ;
така частният случай G = p (U, U) = p (f (f (f (T))), f (f (f (T)))) е тъждествено верен във всички модели на P;
ще отбележим, че ако на втората или третата стъпка изберем да търсим най-обща резолвента с втората клауза от P, то в общия случай можем да получим и други канонични резолвентни редици с начало G и край true;
Сподели с приятели: |