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


Модел на множество от формули



Изтегляне 2.18 Mb.
страница11/22
Дата01.06.2017
Размер2.18 Mb.
#22581
ТипЛекции
1   ...   7   8   9   10   11   12   13   14   ...   22

Модел на множество от формули

нека M е множество от формули; модел на M наричаме всяка структура S, в която всички формули от M са тъждествено вярни;


не всяко множество от формули има модел; например множеството { F, F} няма модели;
казваме, че едно множество от затворени формули е изпълнимо, ако това множество има модел;
една формула наричаме литерал, ако тя има вида A или A, където A е атомарна формула; литералите A и A наричаме противоположни;
Твърдение: Едно множество M от затворени литерали е изпълнимо  в M няма противоположни литерали;

Доказателство: ако в M има противоположни литерали, то очевидно M няма модел, т.е. M не е изпълнимо;

нека в M няма противоположни литерали; ще покажем, че съществува ербранова структура, която е модел на M;

нека M0  M е множеството от всички атомарни формули в M;

както знаем, съществува ербранова структура S, такава че за всяка атомарна формула A, AS = 1  A  M0;

ще покажем, че тази структура S е модел на M; нека F  M;

ако F  M0, то FS = 1 по дефиницията на S;

акo F  M\M0, то F = A, където A е атомарна формула и A  M0, тъй като M не съдържа противоположни литерали  AS = 0;

така FS = (A)S = 1 – AS = 1;

Твърдение: ако M е множество от литерали, то M има модел  множеството от всички затворени частни случаи на литералите от M е изпълнимо;

Доказателство: нека M е множество от литерали, M е множеството от всички затворени частни случаи на литералите от M;

нека S е модел на M; тъй като всеки литерал от M е тъждествено верен в S, то всички затворени частни случаи на този литерал са верни в SS е модел на M  M е изпълнимо;

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



S е модел на M;
ще отбележим, че е вярно по-общо твърдение за множество от безкванторни формули;
пример: нека M = { p (X, b), p (a, Y) };

тогава M = { p (a, b), p (b, b), p (a, b), p (a, a) } и M очевидно не е изпълнимо, тъй като съдържа два противоположни литерала 

M = { p (X, b), p (a, Y) } няма модел;

нека M = { p (a), p (f (X))};

тогава M = { p (a), p (f (a)), p (f (f (a)), …}; очевидно M не съдържа противоположни литерали  M има модел; ербрановият модел S

на M има носител { a, f (a), f (f (a)), …} и pS (A) = 1  A = a;

ще построим краен модел S на M; нека носителят е D = { , };

определяме f S () = , f S () = , pS () = 1, pS () = 0, aS = ;

имаме p (a)S = pS (aS) = pS () = 1  p (a) е вярна в S;

нека v е произволна оценка в S; тогава

p (f (X))S, v = 1 - p (f (X))S, v = 1 - pS (f (X)S, v) = 1 - pS (f S (v (X)) =

= 1 - pS () = 1; така p (f (X)) е тъждествено вярна в S;



Хорнови клаузи



положителни хорнови клаузи наричаме формули от вида

A  B1  B2  …  Bn, n  0, A, B1, B2, …, Bn са атомарни формули;



отрицателни хорнови клаузи наричаме формули от вида

B1  B2  …  Bn, n  0, B1, B2, …, Bn са атомарни формули;

при n = 0 отрицателната хорнова клауза е fail;
положителните хорнови клаузи записваме

по следния начин: A :– B1, B2, …, Bn;

отрицателните хорнови записваме

по следния начин: :– B1, B2, …, Bn;


конюнкцията B1 & B2 & … & Bn се нарича тяло на положителната хорнова клауза A :– B1, B2, …, Bn, формулата A наричаме глава или заключение на клаузата; отделните формули B1, B2, …, Bn се наричат предпоставки на клаузата;

ще покажем, че A :– B1, B2, …, Bn  B1 & B2 & … & Bn  A;

действително, нека S е структура, v е оценка в S;

имаме (A :– B1, B2, …, Bn)S, v = 0  AS, v = 0, B1S, v = 1, …, BnS, v = 1  AS, v = 0, (B1 & B2 & … & Bn)S, v = 1  (B1 & B2 & … & Bn  A)S, v = 0;

разсъждението е валидно и при n = 0, тъй като

B1 & B2 & … & Bn = true;


конюнкцията B1 & B2 & … & Bn се нарича тяло и за отрицателната хорнова клауза :– B1, B2, …, Bn; при това

:– B1, B2, …, Bn  (B1 & B2 & … & Bn) (доказано е при еквивалентност на формули); при n = 0 тази еквивалентност изразява, че fail  true;
пример: нека r е двуместен предикатен символ;

положителната хорнова клауза r (X, Y) :– r (X, Z), r (Z, Y) е тъждествено вярна в някаква структура S, ако r S е транзитивна релация;

отрицателната хорнова клауза :– r (X, Y), r (X, Y) е тъждествено вярна в някаква структура S, ако r S e антисиметрична релация;

в структурата на семейство Вазови, положителната хорнова клауза

distinct (X, Y) :– male (X), female (Y) е тъждествено вярна;
нека A :– B1, B2, …, Bn е положителна хорнова клауза;

ако  е субституция, то (A :– B1, B2, …, Bn) = A :– B1, B2, …, Bn; това следва директно от дефиницията за прилагане на субституции върху безкванторни формули;

ясно е, че VAR (A :– B1, B2, …, Bn) =

VAR (A)  VAR (B1)  …  VAR (Bn); в частност A :– B1, B2, …, Bn е затворена формула  A, B1, B2, …, Bn са затворени формули;

аналогично, ако :– B1, B2, …, Bn е отрицателна хорнова клауза,

(:– B1, B2, …, Bn) = :– B1, B2, …, Bn за всяка субституция ,

VAR (:– B1, B2, …, Bn) = VAR (B1)  …  VAR (Bn); в частност

:– B1, B2, …, Bn е затворена формула  B1, B2, …, Bn са затворени формули;
основният проблем с който ще се занимаваме по-нататък е следния: дадено е множество M от положителни и отрицателни хорнови клаузи (възможно е M да е безкрайно); питаме се дали

M притежава модели;


ако M се състои само от положителни хорнови клаузи, то M има модел – това е структура, в която всички предикати приемат стойност 1 за произволни стойности на променливите;
ако M се състои само от непразни отрицателни хорнови клаузи, то M има модел – това е структура, в която всички предикати приемат стойност 0 за произволни стойности на променливите;
под логическа програма разбираме крайно множество от положителни хорнови клаузи;

под наредена логическа програма (хорнова програма) разбираме крайна редица от положителни хорнови клаузи;


хорнова цел ще наричаме формула от вида A1 & A2 & … & An,

n  0, където Ai са атомарни формули; ясно е, че тялото на всяка положителна или отрицателна хорнова клауза е хорнова цел;


нека P е множество от положителни хорнови клаузи и G е хорнова цел; казваме, че G е изпълнима при P, ако G е изпълнима във всеки модел на P;
Твърдение: нека M е множество от положителни и отрицателни хорнови клаузи, в което има точно една отрицателна хорнова клауза, т.е. M = P  { :– B1, B2, …, Bn}, където P се състои само от положителни хорнови клаузи; нека G = B1 & B2 & …& Bn;

тогава M няма модел  G е изпълнима при P;

Доказателство: нека M няма модел; тъй като P се състои само от положителни хорнови клаузи, то P има модел; нека S е произволен модел на P; S не е модел на M  :– B1, B2, …, Bn не е тъждествено вярна в S  G е изпълнима в S; така G е изпълнима във всеки модел на P, т.е. G е изпълнима при P;

нека G е изпълнима при P; да допуснем, че M има модел S;

тогава S е модел на P, тъй като P  M; S е модел на M 

:– B1, B2, …, Bn е тъждествено вярна в S  G не е изпълнима в S, което е противоречие;
да разгледаме следния пример със сигнатурата на семейство Вазови; нека P = { parent (mincho, ivan), male (mincho), male (ivan) };

нека G = parent (X, Y) & male (X) & male (Y);

тогава G[X/mincho, Y/ivan] = parent (mincho, ivan) & male (mincho) & male (ivan); очевидно, ако S е модел на P, този частен случай на G е верен в S  G е изпълнима в S; това означава, че G е изпълнима във всеки модел на P, т.е. G е изпълнима при P;

нека G1 = parent (X, Y) & male (X) & female (Y);

тази хорнова цел е изпълнима в структурата на семейство Вазови, но тя не е изпълнима при P – например, P има модел S в който

femaleS приема стойност 0 за всяка стойност на променливите;





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

Сподели с приятели:
1   ...   7   8   9   10   11   12   13   14   ...   22



©obuch.info 2024
отнасят до администрацията
    Начална страница
Автореферат
Анализ
Бизнес-план
Биография
Глава
Диплом
Доклад
Задача
Закон
Занятие
Заседание