Лекции по логическо програмиране
Изтегляне 2.18 Mb.
|
- Навигация на страницата:
- Край 18.06.2003
Скулемизацияпроцесът на скулемизация се състои в премахване на кванторите за съществуване в една формула и заместване на свързаните с тях променливи с подходящи термове, така че получената формула да е в някакъв смисъл еквивалентна на първоначалната; нека F е формула от вида F = x G; ако FVAR (F) = , образуваме формулата F = G[x/a], където a 0 и a не участва в F; ако FVAR (F) = { x1, x2, …, xn }, n > 0, xi xj при i j { 1, 2, …, n }, образуваме формулата F = G[x/f (x1, x2, …, xn)], където f n и f не участва в F; ако съответните функционални символи не могат да се изберат от изходната сигнатура, ще си мислим че сме добавили нови функционални символи към тази сигнатура; в случая FVAR (F) = субституцията [x/a] е приложима към G, тъй като VAR (a) = ; в случая FVAR (F) = { x1, x2, …, xn } субституцията [x/f (x1, x2, …, xn)] не винаги е приложима към G; едно достатъчно условие за приложимост е x1, x2, …, xn BVAR (G); например, ако G е в пренексен вид това е изпълнено, тъй като в такъв случай BVAR (G) FVAR (G) = ; така оттук нататък ще си мислим, че G е в пренексен вид; основната цел е да покажем, че съществува структура, в която F е тъждествено вярна съществува структура, в която F е тъждествено вярна; обратната посока е същността на следното Твърдение: F  F;
Доказателство: имаме F = G, където е някаква субституция, приложима към G; от едно твърдение по-горе получаваме, че F = G x G = F;
правата посока е същността на следната Теорема: ако F е тъждествено вярна в структура S, то F е тъждествено вярна в някоя структура S; по-точно S се различава от S по интерпретацията на функционалните символи a, ако F = G[x/a] или f, ако F = G[x/f (x1, x2, …, xn)]; Доказателство: първо ще разгледаме случаят FVAR (F) = ; нека D е носителят на структурата S; нека v е произволна оценка на променливите в S; имаме F S = 1 F S, v = 1, т.е. max { G S, v[x : d]|d D } = 1 съществува d D, такова че G S, v[x : d] = 1; определяме структурата S по следния начин: носителят на S е носителя на S; сигнатурата на S е сигнатурата на S, интерпретацията на S се различава от интерпретацията на S само за функционалния символ a: aS = d; ще покажем, че формулата F = G[x/a] е тъждествено вярна в S; нека v е произволна оценка на променливите в S (или в S); имаме G[x/a]S, v =  =  =  = 1, тъй като интерпретацията на S се отличава от интерпретацията на S само по функционалния символ a, който не участва в G;
сега ще разгледаме случаят FVAR (F) = { x1, x2, …, xn }, n > 1, xi xj при i j { 1, 2, …, n }; за всяка n-торка (d1, d2, …, dn) Dn, дефинираме оценка  на променливите в S по следния начин: (y) = di, ако y = xi, i { 1, 2, …, n-1},
(y) = dn в противен случай; тъй като F е тъждествено вярна в S, то  = 1, т.е. max {  |d D } = 1 съществува d D, такова че = 1; определяме структурата S по следния начин: носителят на S е носителя на S, сигнатурата на S е сигнатурата на S, а интерпретацията на S се различава от интерпретацията на S само за функционалния символ f: f S : Dn D, за всяко (d1, d2, …, dn) Dn, f S (d1, d2, …, dn) е такова, че  = 1;
ще покажем, че F = G[x/f (x1, x2, …, xn)] е тъждествено вярна в S; нека v е произволна оценка на променливите в S (или в S); имаме G[x/f (x1, x2, …, xn)]S, v =  =
=  ; нека di = v (xi), i = 1, 2, …, n;
ще покажем, че v [x : f S (d1, d2, …, dn)] и [x : f S (d1, d2, …, dn)] съвпадат върху FVAR (G);
имаме FVAR (F) = { x1, x2, …, xn } = FVAR (G)\ { x } FVAR (G) = { x1, x2, …, xn } или FVAR (G) = { x1, x2, …, xn, x }; v [x : f S (d1, d2, …, dn)] и тъй като стойността им за променливата x е f S (d1, d2, …, dn); така =  = = 1, тъй като интерпретацията на S се отличава от интерпретацията на S само по функционалния символ f, който не участва в G;
нека F е произволна формула; питаме се дали съществува структура, в която F е тъждествено вярна; за целта на първа стъпка привеждаме F в пренексен вид; след това последователно премахваме кванторите на F отляво надясно по следния алгоритъм: ако най-отпред има квантор за общност го премахваме и получената формула ще е еквивалентна на изходната; ако най-отпред има квантор за съществуване извършваме скулемизация и за получената формула ще съществува структура, в която тя е тъждествено вярна, точно когато за изходната формула съществува структура, в която тя е тъждествено вярна; при тези преобразувания в крайна сметка получаваме безкванторна формула, която е тъждествено вярна в някаква структура изходната формула е тъждествено вярна в някаква структура; за тази безкванторна формула прилагаме по-горе описания метод на резолюцията; Край 18.06.2003 Каталог: fmi fmi -> Софтуерни технологии fmi -> Лекции и семинарни занятия по аналитична геометрия fmi -> 3d-алгоритъм на Chaikin fmi -> Лекции по увод в програмирането fmi -> Лекции и семинарни занятия по линейна алгебра fmi -> Конкурентно Програмиране fmi -> Лекции по компютърни мрежи и комуникации fmi -> Ще предпочетеш да наблюдаваш света отстрани или ще се присъединиш към най-голяма студентска организация? fmi -> Лекции по обектно-ориентирано програмиране Изтегляне 2.18 Mb. Сподели с приятели:
|
=