Лекции по логическо програмиране

Субституции

 (x)  x най-много за краен брой променливи;

ако x₁, x₂, …, x_n са две по две различни променливи и u₁, u₂, …, u_n са термове, то със [x₁/u₁, x₂/u₂, …, x_n/u_n] означаваме субституцията , определена по следния начин:  (x_i) = u_i,

i = 1, 2, …, n,  (x) = x за x  { x₁, x₂, …, x_n};

ако  е произволна субституция и от x  { x₁, x₂, …, x_n} 

 (x) = x (такова крайно множество съществува по дефиниция), то е ясно, че  = [x₁/ (x₁), x₂/ (x₂), …, x_n/ (x_n)];

например  = [x₁/x₁], където x₁ е произволна променлива;

База: ако T  Ф₀, то T = T; ако T  , T =  (T);

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

Стъпка: тогава T = f (T₁, T₂, …, T_n);

 = [X/Y, Y/g (Z)]; последователно получаваме:

f (g (X), Y) = f (g (X), Y) = f (g (X), g (Z)) = f (g (Y), g (Z));
Твърдение: нека T е терм; ако  и  са субституции, които съвпадат върху VAR (T), то T = T;

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

База: ако T  Ф₀, то T = T = T за всеки две субституции  и ;

ако T  , то T = T = T, тъй като T  VAR (T), а  и  съвпадат върху VAR (T);

Предположение: нека T = f (T₁, …, T_n) и твърдението е изпълнено за термовете T₁, …, T_n за произволни субституции  и , съвпадащи върху съответните множества;

Стъпка: нека  и  са произволни субституции, които съвпадат върху VAR (T); за i = 1, 2, …, n имаме VAR (T_i)  VAR (T), така че от индукционното предположение T_i = T_i;

имаме T = f (T₁, …, T_n) = f (T₁, …, T_n) = T;
Tвърдение: нека T е терм; тогава T = T;

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

База: ако T  Ф₀, то T = T по дефиниция;

ако T  , то T =  (T) = T;

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

Стъпка: тогава T = f (T₁, …, T_n) = f (T₁, …, T_n) = T;

субституция ;

Доказателство: нека  е произволна субституция; тогава  и  съвпадат върху VAR (T) =   T = T = T;

Твърдение: нека T е терм,  е субституция;

тогава VAR (T) = ;

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

База: ако T  Ф₀, то VAR (T) = VAR (T) =  и =  - твърдението е изпълнено; ако T  , то VAR (T) = { T},

VAR (T) = VAR ( (T)) и - твърдението е изпълнено;

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

Стъпка: VAR (T) = VAR (f (T₁, …, T_n)) = VAR (T₁)  … VAR (T_n) =  … =

= ;

База: ако F е атомарна формула, F = p (T₁, …, T_n) дефинираме

F = p (T₁, …, T_n), ако F  П₀, то F = F ;

ако F = true или F = fail, дефинираме F = F;

Предположение: нека G, F₁, …, F_n (n > 1) са безкванторни формули и G, F₁, …, F_n са дефинирани;

Стъпка: ако F = G, дефинираме F = (G);

ако F = F₁ & F₂ & … & F_n, дефинираме F = F₁ & F₂ & …& F_n;

ако F = F₁  F₂  …  F_n, дефинираме F = F₁  F₂  … F_n;

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

База: нека  и  са субституции, които съвпадат върху VAR (F);

ако F е атомарна формула и F = p (T₁, …, T_n), то за

i = 1, 2, …, n от VAR (T_i)  VAR (F) и от по-горе  T_i = T_i;

така F = f (T₁, …, T_n) = f (T₁, …, T_n) = F;

ако F е атомарна формула и F  П₀, то F = F = F;

ако F = true или F = fail, то F = F = F;

Предположение: нека твърдението е изпълнено за G, F₁, …, F_n,

n > 1 за произволни субституции  и , които съвпадат върху съответните множества;

Стъпка: нека  и  са произволни субституции, които съвпадат върху VAR (F);

ако F = G, то VAR (G) = VAR (F) и от индукционното предположение G = G; тогава F = (G) = (G) = F;

ако F = F₁ & F₂ & …& F_n, то VAR (F_i)  VAR (F), i = 1, 2, …, n и от индукционното предположение F_i = F_i, i = 1, 2, …, n;

така F = F₁ & F₂ & … & F_n = F₁ & F₂ & … & F_n = F;

ако F = F₁  F₂  … F_n, то VAR (F_i)  VAR (F), i = 1, 2, …, n и от индукционното предположение F_i = F_i, i = 1, 2, …, n;

така F = F₁  F₂  …  F_n = F₁  F₂  …  F_n = F;

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

База: ако F е атомарна формула и F = p (T₁, …, T_n), то

F = p (T₁, …, T_n) = p (T₁, T₂, …, T_n) = F (от съответното твърдение за термове); ако F  П₀, то F = F; ако F = fail или F = true, то F = F;

Предположение: нека G, F₁, …, F_n (n > 1) са такива, че

G = G, F₁ = F₁, …, F_n = F_n;

Стъпка: ако F = G, то F = (G) = G = F;

ако F = F₁ & F₂ & …& F_n, то F = F₁ & …& F_n = F₁ & … & F_n = F;

ако F = F₁  F₂  … F_n, то F = F₁  … F_n = F₁  … F_n = F;
Твърдение: ако F е безкванторна формула и  е субституция, то

VAR (F) = ;

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

База: ако F е атомарна формула и F = p (T₁, …, T_n), то

F = p (T₁, …, T_n), VAR (F) = VAR (T₁)  …  VAR (T_n) =

=  …  = = ; ако F е атомарна формула и F  П₀ или F = fail или F = true то VAR (F) = VAR (F) =  и = ;

Предположение: нека твърдението е изпълнено за формулите

G, F₁, …, F_n (n > 1);

Стъпка:

ако F = G, то VAR (F) = VAR ((G)) = VAR (G); от индукционното предположение VAR (G) = = ;

= VAR (F₁)  VAR (F₂)  …  VAR (F_n); от индукционното предположение имаме VAR (F₁)  VAR (F₂)  …  VAR (F_n) =

=   … =

= = ;

ако F = F₁  F₂  …  F_n, то VAR (F) = VAR (F₁  F₂  …  F_n) =

= VAR (F₁)  VAR (F₂)  …  VAR (F_n); от индукционното предположение имаме VAR (F₁)  VAR (F₂)  …  VAR (F_n) =

=   … =

= = ;

Доказателство: първо да разгледаме случая когато E е терм;

провеждаме индукция по постронието на E;

База: нека  и  са такива субституции, че E = E;

ако E е константа, то очевидно  и  съвпадат върху

VAR (E) = ; ако E  , то E =  (E), E =  (E)   (E) =  (E) 

 и  съвпадат върху VAR (E) = { E};

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

Стъпка: нека  и  са субституции, такива че E = E;

имаме E = f (T₁, T₂, …, T_n), E = f (T₁, T₂, …, T_n); от еднозначния синтактичен анализ на термовете получаваме

T₁ = T₁, T₂ = T₂, …, T_n = T_n; използваме индукционното предположение за термовете T₁, T₂, …, T_n и получаваме, че

 и  съвпадат върху VAR (T₁), VAR (T₂), …, VAR (T_n); тогава

 и  съвпадат върху VAR (T₁)  VAR (T₂)  …  VAR (T_n) = VAR (E);

сега да разгледаме случая когато E е безкванторна формула;

провеждаме индукция по построението на E;

База: нека  и  са такива субституции, че E = E;

нека E = p (T₁, T₂, …, T_n); тогава E = p (T₁, T₂, …, T_n),

E = p (T₁, T₂, …, T_n); от еднозначния синтактичен анализ на атомарните формули получаваме, че T₁ = T₁, T₂ = T₂, …,

T_n = T_n; тъй като T₁, T₂, …, T_n са термове от по-горе  и  съвпадат върху VAR (T₁), VAR (T₂), …, VAR (T_n)   и  съвпадат върху VAR (T₁)  VAR (T₂)  …  VAR (T_n) = VAR (E);

ако E  П₀, E = true или E = fail, то  и  върху VAR (E) = ;

Предположение: нека твърдението е изпълнено за безкванторните формули G, F₁, F₂, …, F_n (n > 2);

Стъпка: нека  и  са такива субституции, че E = E;

ако E = G, то E = (G), E = (G)  G = G; от индукционното предположение  и  съвпадат върху VAR (G) = VAR (F);

ако E = F₁ & F₂ & … & F_n, то E = F₁ & F₂ & … & F_n,

E = F₁ & F₂ & … & F_n; от еднозначния синтактичен анализ на формулите получаваме, че F₁ = F₁, F₂ = F₂, …, F_n = F_n и от индукционното предположение  и  съвпадат върху VAR (F₁),

VAR (F₂), …, VAR (F_n)   и  съвпадат върху

VAR (F₁)  VAR (F₂)  … VAR (F_n) = VAR (E);

ако E = F₁  F₂  …  F_n, то E = F₁  F₂  …  F_n,

E = F₁  F₂  …  F_n; от еднозначния синтактичен анализ на формулите получаваме, че F₁ = F₁, F₂ = F₂, …, F_n = F_n и от индукционното предположение  и  съвпадат върху VAR (F₁),

VAR (F₂), …, VAR (F_n)   и  съвпадат върху

VAR (F₁)  VAR (F₂)  … VAR (F_n) = VAR (E);