Хорнова цел (за краткост цел) ще наричаме всяка крайна редица от атомарни формули (вкл. едночленните редици и празната редица). Една цел ще наричаме затворена, ако всички нейни членове са затворени атомарни формули (тази дефиниция, приложена към празната цел, дава, че тя е затворена по тривиални съображения) . За една затворена цел ще казваме, че е изпълнена в дадена структура S, ако всички членове на тази цел са верни в S (пак по тривиални съображения празната цел е изпълнена във всяка структура). За една каква да е (не непременно затворена) цел ще казваме, че е изпълнена в дадена структура S при дадена оценка v в S на променливите, ако всички членове на тази цел са верни в S при оценката v. За една цел ще казваме, че е изпълнима в дадена структура S, ако тази цел е изпълнена в S при някоя оценка на променливите. От предходния въпрос знаем, че ако A e затворена атомарна формула, то условието A да е вярна в дадена структура S при дадена оценка на променливите е равносилно с условието A да е вярна в S. По тази причина една затворена цел е изпълнима в дадена структура S точно тогава, когато тази цел е изпълнена в S.

    Една непразна цел често ще я означаваме, като на самостоятелен ред напишем въпросителен знак, следван от тире, и след това последователните членове на целта със запетаи между тях и с точка на края. Празната цел ще означаваме със знака [].

    Пример 1. При условията на пример 2 от предходния въпрос, ако S е дефинираната в споменатия пример структура, то целта
        ?- d(a(X)), d(a(a(b(X)))).
е изпълнима в S (защото е изпълнена в S при оценка, която съпоставя на променливата X еднобуквената дума b), а затворената цел
        ?- d(s(e)), p(e,e).
не е изпълнима в S (защото нейният втори член не е верен в S и значи тя не е изпълнена в S).

    Всяка наредена двойка, на която първият член е атомарна формула, а вторият е хорнова цел, ще наричаме хорнова клауза (за краткост клауза). Първия член на такава наредена двойка ще наричаме глава на клаузата (или нейно заключение), а втория - нейно тяло (или нейна предпоставка). Прието е още клауза с празно тяло да се нарича факт, а клауза с непразно тяло - правило. Интуитивно можем да тълкуваме една клауза като твърдение, че ако са верни всички членове на нейното тяло, то е вярна и нейната глава, като в случай на клауза с празно тяло това всъщност е твърдение, че е вярна главата на клаузата. Точната дефиниция в подобен дух, с която ще си служим, е следната: ако S е дадена структура, то за една клауза ще казваме, че е тъждествено вярна в S, ако главата на тази клауза е вярна в S при всяка оценка на променливите, при която в S е изпълнено тялото на клаузата. За клауза с празно тяло разбира се това е равносилно с изискването атомарната формула, която е глава на клаузата, да бъде тъждествено вярна в S. Да отбележим още, че клауза, на която тялото не е изпълнимо в дадена структура S, по тривиални съображения трябва да се счита тъждествено вярна в S.

    Една клауза се нарича затворена, ако са затворени както нейното тяло, така и нейната глава. За такава клауза често ще пропускаме думата "тъждествено" в термина "тъждествено вярна в S"; изискването за тъждествена вярност на клаузата в S в този случай е равносилно с това, че ако тялото на клаузата е изпълнено в S, то главата на клаузата е вярна в S (разбира се, в специалния случай, когато тялото на въпросната клауза е празно, горното изискване от своя страна е равносилно с това главата на клаузата да е вярна в S, а пък в случая, когато тялото на клаузата не е изпълнено в S,  изискването е удовлетворено по тривиални съображения).

    Една клауза обикновено ще я означаваме, като на самостоятелен ред напишем главата на клаузата, следвана от точка в случай, че клаузата е факт, и следвана от знака  :-  и след това последователните членове на тялото на клаузата със запетаи между тях и с точка на края в случай, че клаузата е правило.

    Пример 2. При условията на пример 2 от предходния въпрос, ако S е дефинираната в споменатия пример структура, то например следните клаузи са тъждествено верни в S (ср. с пример 3 от встъпителните бележки):
        p(s(X),a(s(b(X)))).
        p(s(X),a(b(X))).
        p(a(X),a(Y)) :- p(X,Y).
        p(b(X),b(Y)) :- p(X,Y).
        p(s(X),s(Y)) :- p(X,Y).
        d(s(e)).
        d(Y) :- p(X,Y), d(X).
Разбира се за предпоследната от тези клаузи можем да кажем просто, че е вярна в S.

    Множество на променливите на една цел G ще наричаме обединението на множествата на променливите на нейните членове; ще го означаваме с VAR(G). Множество на променливите на една клауза C с глава H и тяло B ще наричаме обединението на множествата VAR(H) и VAR(B); ще го означаваме с VAR(C). Веднага се съобразява, че множеството на променливите на всяка цел и на всяка клауза е крайно. Очевидно една цел е затворена точно тогава, когато множеството на нейните променливи е празно, и аналогично твърдение е в сила за клаузите.

    Всяка крайна редица от хорнови клаузи (вкл. едночленните редици и празната редица) ще наричаме хорнова програма (за краткост програма). Например редицата, съставена от седемте клаузи в горния пример, представлява една хорнова програма. Една непразна хорнова програма обикновено ще я записваме като напишем на последователни отделни редове клаузите, които са нейните последователни членове (така както да речем са записани седемте клаузи в горния пример).

    Модел за дадена хорнова програма P ще наричаме такава структура S, че всички клаузи, които са членове на редицата P, са тъждествено верни в S. Лесно се съобразява, че за всяка хорнова програма P и всяко непразно множество C съществува структура с носител C, която е модел за P. Една такава структура можем да получим, ако за интерпретация в C на всеки функционален символ (ако има такива) изберем произволна операция в C със съответния брой аргументи, за интерпретация на всеки нулместен предикатен символ (ако има такива) вземем числото 1, а за интерпретация на всеки друг предикатен символ - предикат в C, който има съответния брой аргументи и е тъждествено равен на 1. Пример 2 по-горе показва,  че за някои хорнови програми съществуват и значително по-интересни модели (структурата S, за която се говори в примера, е модел за програмата, съставена от изброените там клаузи). Все пак има и случаи, когато една хорнова програма няма други модели освен тривиалните, които описахме преди малко. Например ако сигнатурата е такава, че липсват функционални символи, множеството на едноместните предикатни символи се състои само от еднобуквената дума p, а при n, различно от 1, липсват n-местни предикатни символи, то за едночленната програма
        p(X).
единствените модели са такива структури, в които предикатният символ p се интерпретира чрез едноместен предикат, тъждествено равен на 1.

    Когато искаме с методите на логическото програмиране да изследваме дали дадена цел е изпълнима в дадена конкретна структура S₀, обикновено записваме подходящи краен брой свойства на S₀ посредством хорнови клаузи и след това се опитваме да решим въпроса въз основа на информацията, съдържаща се в тези клаузи. Споменатите краен брой клаузи, взети в някаква последователност, съставляват хорнова програма, за която структурата S₀ е модел. За тази програма обаче ще съществуват и други модели освен S₀ и може да се случи в някои от тях дадената цел да е изпълнима, а в други да не е. За една цел ще казваме, че е изпълнима при дадена програма P, ако тази цел е изпълнима във всеки модел за P. Когато програмата P е получена от дадена структура S₀ по описания преди малко начин (тъй че S₀ да е модел за P), ясно е че изпълнимостта на една цел при програмата P ще гарантира изпълнимост на тази цел и в структурата S₀ (разбира се би могло някой път да се случи една цел да е изпълнима в S₀ и без да е изпълнима при програмата P).

    Пример 3. Имайки пред вид пример 1 от встъпителните бележки, да приемем, че са налице двуместен предикатен символ q и константи a26, a26v, a46, a47, a50, a64, a65a, a78, a79, a81. Да означим с P  програмата
        q(a26,a50).
        q(a26v,a26).
        q(a46,a78).
        q(a47,a46).
        q(a65a,a64).
        q(a78,a47).
        q(a78,a81).
        q(a79,a47).
Пак по повод на споменатия пример да разгледаме и целта
        ?- q(X,Y), q(Y,Z), q(Z,X).
Припомняйки си направеното там, трябва да очакваме, че тя е изпълнима при P и то благодарение на наличието в P на фактите с глави атомарните формули q(a46,a78),  q(a78,a47) и q(a47,a46). За да установим споменатата изпълнимост въз основа на дадените дефиниции, нека означим с S произволна структура, която е модел за P. Благодарение на това, че S е модел за P, току-що споменатите три атомарни формули са верни в S.Това означава, че са в сила равенствата

    Разсъжденията, с които в горния пример установихме изпълнимост на разглежданата цел при разглежданата програма, имат семантичен характер и изискват прилагане на няколко от дадените дефиниции. След като докажем някои неща по-нататък, ще можем да установяваме изпълнимост на цел при дадена програма значително по-просто, като при това ще можем да работим само с  формални синтактични средства и то в духа на примерите от встъпителните бележки.
 

Последно изменение: 21.06.2000 г.
 

Previous  Next  Contents