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

Изтегляне 2.18 Mb.

страница	10/22
Дата	01.06.2017
Размер	2.18 Mb.
	#22581
Тип	Лекции

1 ... 6 7 8 9 10 11 12 13 ... 22

Еквивалентност на формули

Ербранови структури

множеството от всички затворени термове наричаме ербранов универсум – бележим го с H;

казваме, че една структура S е ербранова, ако е изпълнено:

носителят на S е H;
ако c  Ф₀, то c^S = c;
ако f  Ф_n, n > 0, то f ^S (T₁, T₂, …, T_n) = f (T₁, T₂, …, T_n) са всяка наредена n-торка T₁, T₂, …, T_n от елементи на H;

например за сигнатурата на семейство Вазови без функционалните символи next и prev ербрановият универсум е

H = { ivan, mincho, syba };

ако включим функционалните символи next и prev, ербрановият универсум H вече съдържа безброй много елементи;

Твърдение: ако S е ербранова структура, то за всеки затворен терм T имаме T ^S = T;

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

База: ако T е константа, по дефиницията за ербранова структура имаме T^S = T;

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

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

= f (T₁, T₂, …, T_n) = T; използвали сме индукционното предположение и дефиницията за ербранова структура;

Следствие: всяка ербранова структура S има термално породен носител;

Доказателство: действително всеки затворен терм от H е стойност на същия затворен терм в S;

друго следствие от твърдението е, че всеки елемент на носителя на ербранова структура е стойност на точно един затворен терм;
Твърдение: нека M е множество от затворени атомарни формули; тогава съществува единствена ербранова структура S, такава че измежду всички затворени атомарни формули в S са вярни точно онези, които принадлежат на M;

Доказателство: ще построим ербрановата структура S; тя има носител H и функционалните символи са интерпретирани по дефиницията за ербранова структура; нека p е n-местен предикатен символ;

ако n > 0 определяме p^S (T₁, T₂, …, T_n) = 1  p (T₁, T₂, …, T_n)  M за всяка наредена n-торка T₁, T₂, …, T_n от елементи на H;

при n = 0 определяме p^S = 1  p  M;

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

нека A е затворена атомарна формула;

ако A = p (T₁, T₂, …, T_n), то

A^S = p^S (T₁^S, T₂^S, …, T_n^S) = p^S (T₁, T₂, …, T_n) = 1 

p (T₁, T₂, …, T_n)  M, т.е. A^S = 1  A  M;

ако A = p  П₀, то A^S = p^S = 1  p  M, т.е. A^S = 1  A  M;

нека S е произволна ербранова структура с описаното свойство;

нека p е n-местен предикатен символ;

при n > 0 имаме p^S (T₁, T₂, …, T_n) = 1  p^S (T₁^S, T₂^S, …, T_n^S) = 1 

p (T₁, T₂, …, T_n)^S = 1  p (T₁, T₂, …, T_n)  M;

при n = 0 имаме p^S = 1  p  M;

така ербрановата структура с описаното свойство е единствена;

по този начин всяка ербранова структура се определя еднозначно, ако се зададе кои атомарни формули са вярни в нея;

Еквивалентност на формули

нека F и G са формули; казваме, че F и G са еквивалентни, ако

F ^S^,^v = G^S^,^v за произволна структура S и произволна оценка v в S;

бележим F  G;

еквивалентността е релация на еквивалентност:

рефлексивност: F  F;

симетричност: F  G  G  F (от симетричността на равенството);

транзитивност: F  G, G  H  F  H (от транзитивността на равенството);

примери:

true  fail;

fail  true;

F  F;

(F₁ & F₂ & … & F_n)  F₁  F₂  …  F_n;

(F₁  F₂  …  F_n)  F₁ & F₂ & … & F_n;

x F  x F;

x F  x F;

например ще покажем, че x F  x F;

нека S е произволна структура с носител D; нека v е произволна оценка в S; тогава (x F)^S^,^v = 1 – (x F)^S^,^v =

= 1 – min { F ^{S, v}^[^x^{: d]} | d  D } = 0  min { F ^{S, v}^[^x^{: d]} | d  D } = 1 

F ^{S, v}^[^x^{: d]} = 1 за всяко d  D  (F) ^{S, v}^[^x^{: d]} = 0 за всяко d  D 

max { (F) ^{S, v}^[^x^{: d]} | d  D } = 0, т.е. (x F)^{S, v} = 0;

така (x F)^{S, v} = 0  (x F)^{S, v} = 0  x F  x F;

съвсем аналогично се показва, че x F  x F;
ако x  FVAR (F), то x F  F, x F  F;

нека S е произволна структура с носител D; нека v е произволна оценка в S; тогава (x F)^S^,^v = max { F ^S^,^v^[^x^:^d^] | d  D };

за всяко d  D, v и v[x : d] съвпадат върху FVAR (F),

тъй като x  FVAR (F)  за всяко d  D, F ^{S, v}^[^x^{: d]} = F ^{S, v};

така (x F)^{S, v} = max { F ^{S, v}^[^x^{: d]} | d  D } = F ^{S, v}  x F  F;

съвсем аналогично се показва, че x F  F;

Твърдение: ако F  G, то F  G;

Доказателство: нека S е произволна структура, v е оценка на променливите в S;

имаме (F)^{S, v} = 1 – F ^{S, v} = 1 – G^{S, v} = (G)^{S, v}  F  G;

Твърдение: ако F₁  G₁, F₂  G₂, …, F_n  G_n, то F₁ & F₂ & … & F_n 

 G₁ & G₂ & … & G_n и F₁  F₂  …  F_n  G₁  G₂  …  G_n;

Доказателство: нека S е произволна структура, v е оценка на променливите в S; (F₁ & F₂ & … & F_n)^{S, v} = min { F₁^{S, v}, F₂^{S, v}, …, F_n^{S, v}} = min { G₁^{S, v}, G₂^{S, v}, …, G_n^{S, v}} = (G₁ & G₂ & … & G_n)^{S, v} 

F₁ & F₂ & … & F_n  G₁ & G₂ & … & G_n; съвсем аналогично,

F₁  F₂  …  F_n  G₁  G₂  …  G_n;
Твърдение: ако F  G, то x F  x G, x F  x G;

Доказателство: нека S е произволна структура с носител D,

v е оценка на променливите в S; (x F)^S^,^v = min { F ^S^,^v^[^x^:^d^] | d  D } = min { G ^S^,^v^[^x^:^d^] | d  D } = (x G)^S^,^v  x F  x G; съвсем аналогично, x F  x G;
по дефиниция F  G = F  G; като използваме горните твърдения, ще покажем че F  G  (F  G);

действително (F  G)  F  G  F  G = F  G, тъй като

F  F, G  G;

Каталог: fmi
fmi -> Софтуерни технологии
fmi -> Лекции и семинарни занятия по аналитична геометрия
fmi -> 3d-алгоритъм на Chaikin
fmi -> Лекции по увод в програмирането
fmi -> Лекции и семинарни занятия по линейна алгебра
fmi -> Конкурентно Програмиране
fmi -> Лекции по компютърни мрежи и комуникации
fmi -> Ще предпочетеш да наблюдаваш света отстрани или ще се присъединиш към най-голяма студентска организация?
fmi -> Лекции по обектно-ориентирано програмиране

Изтегляне 2.18 Mb.

Сподели с приятели:

1 ... 6 7 8 9 10 11 12 13 ... 22