Търсене на атомарна формула, която е частен случай на всяка от две дадени атомарни формули

Решаване на системи от уравнения между термове

от вида T = U, където T и U са термове; решение на това уравнение наричаме субституция , такава че T = U;

T₁ = U₁, T₂ = U₂, …, T_n = U_n;

 е решение на системата T₁ = U₁, T₂ = U₂, …, T_n = U_n;

Доказателство: нека  е произволна субституция;

имаме A = p (T₁, T₂, …, T_n), B = p (U₁, U₂, …, U_n);

от еднозначния синтактичен анализ имаме:

A = B  T₁ = U₁, T₂ = U₂, …, T_n = U_n, т.е.  е унификатор на A и B   е решение на системата T₁ = U₁, T₂ = U₂, …, T_n = U_n;

X = f (Y), f (X) = Z, Y = c;

тъй като x₁, x₂, …, x_n са две по две различни помежду си можем да построим субституцията ₀ = [x₁/U₁, x₂/U₂, …, x_n/U_n];

Доказателство: за i = 1, 2, …, n имаме x_i₀ = U_i, U_i₀ = U_i = U_i, тъй като ₀ и  съвпадат върху VAR (U_i); така x_i₀ = U_i = U_i₀,

i = 1, 2, …, n  ₀ е решение на системата;

нека  е произволно решение на системата, т.е. x_i = U_i,

i = 1, 2, …, n; тогава x_i(₀) = (x_i₀) = U_i = x_i, i = 1, 2, …, n;

също за всяко x  \{ x₁, x₂, …, x_n} x(₀) = (x₀) = x; така  = ₀;

 е решение на системата;

субституцията ₀ = [x₁/U₁, x₂/U₂, …, x_n/U_n] е общо решение, така че решенията на системата се изчерпват със ₀, където  е произволна субституция;

U  x и x  VAR (U);

Доказателство: с индукция по построението ще покажем, че за всеки терм W, ако x  VAR (W) и x  W, то |W| > |x| за всяка субституция ;

База: ако W е константа, то VAR (W) =  - противоречие

(x  VAR (W)); ако W е променлива, то от x  VAR (W) получаваме

W = x – противоречие (W  x);

Предположение: нека W = f (W₁, W₂, …, W_k) и твърдението е изпълнено за термовете W₁, W₂, …, W_k;

Стъпка: нека  е произволна субституция; имаме

W = f (W₁, W₂, …, W_k); ясно е, че |W| > |W_i| за всяко

i = 1, 2, …, n; тъй като x  VAR (W), то x  VAR (W_i)

за някое i  { 1, 2, …, k }; ако W_i  x, то по индукционното предположение|W_i| > |x|  |W| > |W_i| > |x|;

ако W_i = x, то |W| > |W_i| = |x|; така и в двата случая

|W| > |x|;

сега, ако допуснем, че  е решение на системата x = U ще получим, че |x|= |U|, което е противоречие;
уравнения от горните два вида наричаме явно нерешими; казваме, че една система е явно нерешима, ако тя съдържа явно нерешимо уравнение; ясно е, че такава система няма решение;
две системи от уравнения между термове наричаме еквивалентни, ако множествата от решенията им съвпадат;
ще посочим четири еквивалентни преобразувания на системи, т.е. преобразувания чрез които една система преминава в еквивалентна на нея система;

нека T₁ = U₁, T₂ = U₂, …, T_n = U_n е система от уравнения между термове;

1. 
   премахване на тъждество – ако за някое i  { 1, 2, …, n} имаме T_i = U_i премахваме това уравнение от системата;
   

2. 
   разпадане – ако за някое i  { 1, 2, …, n} имаме
   

V₁ = W₁, V₂ = W₂, …, V_m = W_m; системата преминава в еквивалентна на нея, тъй като  е решение на T_i = U_i,

т.е. T_i = U_i  f (V₁, V₂, …, V_m) = f (W₁, W₂, …, W_m)  (от еднозначния синтактичен анализ)

V₁ = W₁, V₂ = W₂, …, V_m = U_m;

изисква се T_i  U_i, тъй като при T_i = U_i е удачно да се извърши премахване на тъждество;

3. 
   обръщане – ако за някое i  { 1, 2, …, n} имаме T_i  , U_i  ,
   

4. 
   заместване – ако за някое i  { 1, 2, …, n} имаме T_i  ,
   

T₁[T_i/U_i] = U₁[T_i/U_i], …, T_i-1[T_i/U_i] = U_i-1[T_i/U_i],

T_i = U_i, T_i+1[T_i/U_i] = U_i+1[T_i/U_i], …, T_n[T_i/U_i] = U_n[T_i/U_i];

ще покажем, че двете системи са еквивалентни;

да означим ₀ = [T_i/U_i]; нека  е произволно решение на изходната система; тъй като  е решение на уравнението

T_i = U_i, то  = ₀; за j  i  { 1, 2, …, n} T_j = T_j(₀) = (T_j₀)

и U_j = U_j(₀) = (U_j₀)  (T_j₀) = (U_j₀); така  е решение и на преобразуваната система;

нека  е произволно решение на преобразуваната система; тъй като  е решение на уравнението T_i = U_i, то  = ₀;

за j  i  { 1, 2, …, n} T_j = T_j(₀) = (T_j₀) и

U_j = U_j(₀) = (U_j₀)  T_j = U_j, т.е.  е решение на изходната система;

(обръщане) X = f (Y), Z = f (X), Y = c;

(заместване) X = f (Y), Z = f (f (Y)), Y = c;

(заместване) X = f (c), Z = f (f (c)), Y = c;

получената система е в решен вид и нейното общо решение се дава със субституцията ₀ = [X/f (c), Z/f (f (c)), Y/c];

така унификаторите на формулите A = p (X, f (X), Y) и

B = p (f (Y), Z, c) се изчерпват със ₀, където  е произволна субституция;
Теорема: всяка система от уравнения между термове може да се приведе чрез четирите еквивалентни преобразувания до система в решен вид или до явно нерешима система;
Доказателство:

ще посочим алгоритъм за преобразуване на произволна система чрез еквивалентните преобразувания до система в решен вид или до явно нерешима система:

1. 
   ако системата не е в решен вид или не е явно
   

2. 
   към системата прилагаме някое от четирите еквивалентни преобразувания (което е възможно); към 1.;
   

• 
  ако една система не е в решен вид и не е явно нерешима, то е възможно да се извърши някое от четирите преобразувания;
  
• 
  алгоритъмът приключва след краен брой стъпки;
  

нека T₁ = U₁, T₂ = U₂, …, T_n = U_n е система от уравнения между термове, която не е в решен вид и не е явно нерешима; да допуснем, че не е възможно да извършим никое от четирите преобразувания; ще покажем, че T₁, T₂, …, T_n са променливи;

да допуснем, че за някое i  { 1, 2, …, n} T_i не е променлива;

ако U_i е променлива, тогава можем да извършим обръщане – противоречие; ако U_i не е променлива и T_i = U_i, то можем да извършим премахване на тъждество – противоречие;

ако U_i е константа и T_i  U_i, то уравнението T_i = U_i е явно нерешимо  системата е явно нерешима – противоречие;

ако U_i е съставен терм, T_i  U_i и T_i, U_i имат еднакви функционални символи с един и същ брой аргументи, то можем да извършим разпадане – противоречие; ако U_i е съставен терм, T_i  U_i и T_i, U_i имат различни функционални символи или функционални символи с различен брой аргументи, то уравнението T_i = U_i е явно нерешимо  системата е явно нерешима – противоречие; във всички случаи получихме противоречие с допускането, че T_i не е променлива  T₁, T₂, …, T_n са променливи;

за i = 1, 2, …, n имаме T_i  U_i, тъй като в противен случай можем да извършим премахване на тъждество;

по предположение системата е явно нерешима и тъй като T_i  U_i, то T_i  VAR (U_i), i = 1, 2, …, n;

ако допуснем, че за някои i  j  { 1, 2, …, n} T_i  VAR (U_j)  { T_j} ще получим противоречие, тъй като в такъв случай можем да извършим заместване; така променливите T₁, T₂, …, T_n са две по две различни и T_i  VAR (U_j) за всеки i, j  { 1, 2, …, n }, т.е. системата е в решен вид – противоречие с допускането, че системата не в в решен вид; така към всяка система от уравнения между термове, която не е в решен вид и не е явно нерешима може да се приложи някое от четирите еквивалентни преобразувания;

ще покажем, че алгоритъмът завършва след краен брой стъпки;

нека T е терм; дефинираме височина на терма h (T) с индукция по построението:

База: ако T е променлива, дефинираме h (T) = 1; ако T е константа, дефинираме h (T) = 2;

Предположение: нека T = f (T₁, T₂, …, T_n) и h (T₁), h (T₂), …, h (T_n) са дефинирани;

Стъпка: дефинираме h (T) = h (T₁) + h (T₂) + … + h (T_n) + 1;

съвсем лесно с индукция по построението се проверява, че

височината на всеки терм е строго положително число; при това термовете, които не са променливи имат височина строго

по-голяма от 1;

под височина на системата от уравнения между термове

T₁ = U₁, T₂ = U₂, …, T_n = U_n ще разбираме числото

h (T₁) + h (T₂) + … + h (T_n); ще изследваме как се променя височината на системата при извършване на еквивалентните преобразувания:

• 
  при премахване на тъждество височината строго намалява, тъй като от лявата страна премахваме терм и височината на всеки терм е строго положителна;
  
• 
  при разпадане от лявата страна премахваме съставен терм
  

• 
  при обръщане от лявата страна премахваме терм който не е променлива и го заменяме с променлива; тъй като всеки терм, който не е променлива има височина по-голяма от 1, а променливите имат височина 1, то височината на системата строго намалява;
  
• 
  при заместване лявата страна или не се променя или променливи се заместват с термове, така че височината на системата или не се променя или нараства;
  

ще казваме, че системата от уравнения между термове

T₁ = U₁, T₂ = U₂, …, T_n = U_n е решена относно променливата x,

ако x = T_i за някое i  { 1, 2, …, n}, x  VAR (T_j)  VAR (U_j),

j  i  { 1, 2, …, n} и x  VAR (U_i), т.е. x не се среща никъде другаде в системата освен като лява част на точно едно уравнение;

например, ако системата е в решен вид, то тя е решена относно

променливите T₁, T₂, …, T_n;

нека системата е решена относно променливата x, x = T_i;

ще покажем, че при всяко от еквивалентните преобразувания системата остава решена относно x:

• 
  при премахване на тъждество не можем да премахнем
  

• 
  при разпадане уравнението T_i = U_i не се променя, тъй като T_i не е съставен терм; ясно е, че в новодобавените уравнения x не присъства, тъй като x не присъства в уравнението, което се разпада; така системата остава решена относно x;
  
• 
  при обръщане уравнението T_i = U_i не се променя, тъй като T_i е променлива; системата очевидно остава решена относно x;
  
• 
  при заместване не можем да използваме уравнението T_i = U_i, тъй като променливата x не се среща никъде другаде в системата; така заместваме променлива, различна от x и тогава получената системата ще остане решена относно x;
  

разглеждаме броят на променливите от ₀, относно които системата не е решена; съгласно горните разсъждения при извършване на кое да е от четирите еквивалентни преобразувания този брой не може да нарастне; освен това при заместване този брой намалява строго с 1: ако заместваме променливата Т_i, то тази система не е решена относно T_i, тъй като T_i се среща поне на още едно място в системата; също T_i  VAR (U_i) и след заместване на T_i с U_i в другите уравнения ще получим система, която е решена относно T_i;

от направените разсъждения получаваме, че алгоритъмът може да извърши само краен брой пъти заместване – в противен случай ще получим, че ₀ е безкрайно множество;

така алгоритъмът извършва само краен брой пъти заместване и само краен брой пъти последователно първите три преобразувания, така че той приключва след краен брой стъпки;