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



Изтегляне 2.18 Mb.
страница4/22
Дата01.06.2017
Размер2.18 Mb.
#22581
ТипЛекции
1   2   3   4   5   6   7   8   9   ...   22

Атомарни формули

фиксирана е сигнатура , ;

дефинираме атомарна формула:

ако p  Пn, n > 0 и T1, T2, …, Tn са термове, то p (T1, T2, …, Tn) е атомарна формула;

ако p  П0, то p е атомарна формула;
ясно е, че всяка атомарна формула е префиксен израз над , което допълнително с достатъчното условие осигурява еднозначен синтактичен анализ на атомарните формули; също, атомарните формули и термове съществено се различават, тъй като

nn = , n = 0, 1, …;

примери за атомарни формули със сигнатурата на семейство Вазови:

parent (mincho, ivan)

distinct (X, mincho)

female (Y)

parent (X, Y)

parent (ivan, next (X))


за всяка атомарна формула A определяме VAR (A) – множеството на променливите на A;

ако A = p (T1, T2, …, Tn), VAR (A) = VAR (T1)  VAR (T2)  … VAR (Tn);

ако A  П0, VAR (A) = ;

очевидно VAR (A) е крайно множество, тъй като е или крайно обединение на крайни множества или празното множество;


една атомарна формула наричаме затворена, ако VAR (A) = ;

от дефиницията за множеството на променливите на атомарна формула е ясно, че атомарната формула A е затворена 

A  П0 или A = p (T1, T2, …, Tn), където T1, T2, …, Tn са затворени термове;

Семантика на атомарните формули

фиксираме структура S с носител D и интерпретации 0, 1, …;

0, 1, …; съответно на функционалните и на предикатните символи;
на всяка затворена атомарна формула А съпоставяме елемент

от { 0, 1}, наречен стойност на A в S;

стойността на A бележим с AS;

по дефиниция, ако A = p (T1, …, Tn), то AS = pS (T1S, …, TnS);

(дефиницията е коректна, тъй като T1, …, Tn са затворени термове); ако A  П0, то AS = 0 (A);

ако AS = 1, казваме че A е вярна в S;

ако AS = 0, казваме че A не е вярна в S;
нека v е оценка на променливите; на всяка атомарна формула А съпоставяме елемент от { 0, 1}, наречен стойност на A в S при оценка v; бележим стойността на A в S при оценка v с AS, v;

по дефиниция, ако A = p (T1, T2, …, Tn),

то AS, v = pS (T1S, v, T2S, v, …, TnS, v); ако A  П0, то AS, v = 0 (A);
Твърдение: ако A е затворена атомарна формула, то AS, v = AS за всяка оценка v;

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

ако A = p (T1, T2, …, Tn), където T1, …, Tn са затворени термове, то

AS, v = pS (T1S, v, T2S, v, …, TnS, v) = pS (T1S, T2S, …, TnS) = AS; (от съответната теорема при семантика на термовете)

ако A  П0, то AS, v = 0 (A) = AS;
Твърдение: ако А е атомарна формула, а v и u са оценки, които съвпадат върху VAR (A), то AS, v = AS, u;

Доказателство:

ако A = p (T1, T2, …, Tn), то VAR (Ti)  VAR (A), i = 1, 2, …, n 

v и u съвпадат върху VAR (Ti), i = 1, 2, …, n и от съответната теорема при семантика на термовете имаме TiS, v = TiS, u,

i = 1, 2, …, n; така AS, v = pS (T1S, v, T2S, v, …, TnS, v) =

= p S (T1S, u, T2S, u, …, TnS, u) = A S, u;

ако A  П0, то AS, v = AS = AS, u;



Логически формули

фиксирана е сигнатура , ;

дефинираме индуктивно логическа формула:

База: всяка атомарна формула е логическа формула;

думите true, fail са логически формули;

Предположение: нека F е логическа формула, n > 1 и

F1, F2, …, Fn са логически формули;

Стъпка: думата not (F) е логическа формула – нарича се отрицание на F; думата (F1, F2, …, Fn) е логическа формула – нарича се конюнкция на формулите F1, F2, …, Fn; думата

(F1; F2; …; Fn) е логическа формула – нарича се дизюнкция на формулите F1, F2, …, Fn; ако x е променлива, думата

for_all (x: F) е логическа формула – нарича се генерализация на F по x; ако x е променлива, думата for_some (x: F) е логическа формула – нарича се екзистенциализация на F по x;


ще възприемем и други означения:

логическата формула not(F) често ще означаваме с F;

логическата формула (F1, F2, …, Fn) често ще означаваме с

F1 & F2 & … & Fn;

логическата формула (F1; F2; …; Fn) често ще означаваме с

F1  F2  …  Fn;

логическата формула for_all (x: F) често ще означаваме с x F;

логическата формула for_some (x: F) често ще означаваме с x F;


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

под празна конюнкция (конюнкция на нула формули) ще разбираме логическата формула true;

под празна дизюнкция (дизюнкция на нула формули) ще разбираме логическата формула fail;
нека S е структура; за всяка формула F дефинираме множество на променливите на F – VAR (F) с индукция по построението;

База: ако F е атомарна формула, то VAR (F) е вече дефинирано;

ако F = true или F = fail, дефинираме VAR (F) = ;

Предположение: нека F, F1, …, Fn (n > 1) са формули и VAR (G),

VAR (F1), …, VAR (Fn) са вече дефинирани;

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

VAR (F1 & F2 & …& Fn) = VAR (F1)  VAR (F2)  … VAR (Fn);

VAR (F1  F2  …  Fn) = VAR (F1)  VAR (F2)  … VAR (Fn);

VAR (x F) = VAR (F)  { x}, VAR (x F) = VAR (F)  { x};
както при термове, с индукция по построението може да се покаже, че за всяка формула F, VAR (F) е крайно множество;
нека S е структура, F е формула;

за формулата F дефинираме множество на свободните променливите на F – FVAR (F) с индукция по построението;

База: ако F е атомарна формула, то FVAR (F) = VAR (F);

ако F = true или F = fail, дефинираме FVAR (F) = ;

Предположение: нека F, F1, …, Fn (n > 1) са формули и FVAR (F),

FVAR (F1), …, FVAR (Fn) са вече дефинирани;

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

FVAR (F1 & F2 & … Fn) = FVAR (F1)  FVAR (F2)  … FVAR (Fn);

FVAR (F1  F2  …  Fn) = FVAR (F1)  FVAR (F2)  … FVAR (Fn);

FVAR (x F) = FVAR (F)\{ x}, FVAR (x F) = FVAR (F)\{ x};


например FVAR (X p(X)) = ;
казваме, че една формула е затворена, ако FVAR (F) = ;

ако A е атомарна формула, то FVAR (A) = VAR (A), така че за атомарни формули тази дефиниция съвпада с предишната дефиниция за затвореност;


ще дадем индуктивна дефиниция за безкванторни формули;

База: всяка атомарна формула е безкванторна формула;

думите true, fail са безкванторни формули;

Предположение: нека F е безкванторна формула, n > 1 и

F1, F2, …, Fn са безкванторни формули;

Стъпка: тогава F, F1 & F2 & …& Fn, F1  F2  … Fn са безкванторни формули;

Заключение: няма други безкванторни формули;
Твърдение: ако F е безкванторна формула, то FVAR (F) = VAR (F);

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

База: ако F е атомарна формула, то FVAR (F) = VAR (F) по дефиниция; ако F е true или fail, то FVAR (F) = VAR (F) =  по дефиниция;

Предположение: нека G, F1, …, Fn (n > 1) са безкванторни формули и VAR (G) = FVAR (G), VAR (F1) = FVAR (F1), …, VAR (Fn) = FVAR (Fn);

Стъпка: ако F = G, то VAR (F) = VAR (G) = VAR (G) = FVAR (G),

FVAR (F) = FVAR (G) = FVAR (G)  VAR (F) = FVAR (F);

ако F = F1 & F2 & … & Fn, то VAR (F) = VAR (F1 & F2 & … & Fn) =

= VAR (F1)  VAR (F2)  … VAR (Fn) =

= FVAR (F1)  FVAR (F2)  … FVAR (Fn),

FVAR (F) = FVAR (F1 & F2 & … & Fn) = FVAR (F1)  FVAR (F2)  …

 FVAR (Fn)  VAR (F) = FVAR (F);

ако F = F1  F2  …  Fn, то VAR (F) = VAR (F1  F2  …  Fn) =

= VAR (F1)  VAR (F2)  … VAR (Fn) =

= FVAR (F1)  FVAR (F2)  … FVAR (Fn),

FVAR (F) = FVAR (F1  F2  …  Fn) = FVAR (F1)  FVAR (F2)  …

 FVAR (Fn)  VAR (F) = FVAR (F);





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

Сподели с приятели:
1   2   3   4   5   6   7   8   9   ...   22



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