Най-общ унификатор на две атомарни формули

Най-обща резолвента на хорнова цел и хорнова клауза

нека 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 е непосредствена резолвента на G₁ и C₂ за някои субституции

₁, ₂ (отновно използваме, че частните случаи на C и C са едни и същи); дефинираме  (x) = ₁ (x), ако x  VAR (G) и  (x) = ₂ (x), ако

₁ (x)  x или ₂ (x)  x, но ₁ (x)  x или ₂ (x)  x за краен брой променливи, така че  (x)  x за краен брой променливи;

тъй като  и ₁ съвпадат върху VAR (G), то G = G₁;

 и ₂ съвпадат върху VAR (C), тъй като VAR (C)  VAR (G) =  

VAR (C)  \VAR (G); така C = C₂; така 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 е множество от положителни хорнови клаузи;

редицата от хорнови цели G₀, G₁, …, G_n, …наричаме канонична резолвентна редица относно P, ако за всяко i = 1, 2, …, n, …

имаме G_i е най-обща резолвента на G_i-1 с някоя клауза от P;

i = 1, 2, …, n имаме G_i е резолвента на G_i-1 и C_i;

казваме още, че G_n е резолвентно достижима от G₀ чрез редицата C₁, C₂, …, C_n или, че G_n е резолвента на G₀ с редицата

C₁, C₂, …, C_n;

C₁, C₂, …, C_n наричаме редица G₀, G₁, …, G_n от хорнови цели, така че за i = 1, 2, …, n имаме G_i е най-обща резолвента на G_i-1 и C_i;

казваме още, че G_n е канонично резолвентно достижима от G₀ чрез редицата C₁, C₂, …, C_n или, че G_n е канонична резолвента на G₀ с редицата C₁, C₂, …, C_n;
Твърдение: нека G има канонична резолвента G с редицата от положителни хорнови клаузи C₁, C₂, …, C_n; тогава G е най-обща измежду резолвентите на G с редицата C₁, C₂, …, C_n;

Доказателство: нека G = G₀, G₁, …, G_n = G е канонична резолвента редица, съответна на редицата C₁, C₂, …, C_n, т.е. за i = 1, 2, …, n

G_i е най-обща резолвента на G_i-1 и C_i; нека R е произволна резолвента на G с редицата C₁, C₂, …, C_n;

нека G = R₀, R₁, …, R_n = R е резолвентна редица, съответна на редицата C₁, C₂, …, C_n, т.е. за i = 1, 2, …, n R_i е резолвента на

R_i-1 и C_i; с индукция по i = 1, 2, …, n ще покажем, че R_i е частен случай на G_i; в частност при i = m получаваме, че R е частен случай на G, което доказва твърдението;

База: при i = 0 имаме R₀ = G₀ = G и очевидно R₀ е частен

случай на G₀;

Предположение: нека 1  i  n и R_i-1 е частен случай на G_i-1;

Стъпка: от индукционното предположение R_i-1 е частен случай на G_i-1 и R_i е резолвента на R_i-1 и C_i, то R_i е резолвента на G_i-1 и C_i;

от друга страна G_i е най-обща резолвента на G_i-1 и C_i  R_i е частен случай на G_i;

Доказателство: провеждаме индукция по n;

База: при n = 1 G има резолвента с C₁  G има най-обща резолвента G₁ с C₁ и G, G₁ е канонична резолвентна редица относно едночленната редица C₁;

Предположение: нека 1  m < n и е изпълнено, че ако G има резолвента с редицата C₁, C₂, …, C_m, то G има канонична резолвента с редицата C₁, C₂, …, C_m;

Стъпка: нека G има резолвента с редицата C₁, C₂, …, C_m, C_m+1;

ясно е, че в такъв случай G има резолвента G с редицата

C₁, C₂, …, C_m и G има резолвента G с C_m+1; от индукционното предположение G има канонична резолвента R с C₁, C₂, …, C_m и от предното твърдение G е частен случай на R; при това положение

R има резолвента G с C_m+1, тъй като всеки частен случай на G е частен случай на R  R има най-обща резолвента R с C_m+1;

тъй като R е канонична резолвента на G с редицата

C₁, C₂, …, C_m и R е най-обща резолвента на R и C_m+1, то

R е канонична резолвента на G с редицата C₁, C₂, …, C_m, C_m+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 и втората клауза; да означим с G₁ новата цел p (f (Y), f (Z)), p (Y, Z);

търсим най-обща резолвента на G₁ с първата клауза;

тъй като G₁ няма общи променливи с първата клауза, няма нужда да образуваме вариант на клаузата; решаваме следната система от термове: 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) на първата клауза и целта G₁ имат непосредствена резолвента p (f (X), X), която е най-обща резолвента на първата клауза и G₁; да означим с G₂ новата цел p (f (X), X);

търсим най-обща резолвента на G₂ с първата клауза;

тъй като G₂ и първата клауза имат общи променливи, трябва да вземем вариант на клаузата, който няма общи променливи с G₂, например 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)) на първата клауза и целта G₂ имат непосредствена резолвента празната цел true, така че първата клауза има резолвента true с целта G₂;

получихме канонична резолвентна редица G, G₁, G₂, 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;