Нека е дадена една сигнатура Σ. Атомарните формули, термовете и субституциите, за които ще става дума нататък, ще бъдат всъщност атомарни формули при сигнатура Σ и понятията, които ще въведем, фактически ще зависят от избора на тази сигнатура, макар че за краткост няма да я споменаваме. Структурите, които ще разглеждаме, също ще бъдат със сигнатура Σ. Ще наричаме положителни хорнови клаузи, а за по-кратко клаузи наредените двойки, на които първият член е атомарна формула, а вторият  –  крайна (евентуално празна) редица от атомарни формули. Под хорнова програма ще разбираме крайна редица от положителни хорнови клаузи. Членовете на една хорнова програма ще наричаме нейни клаузи. Ако (φ,Γ) е положителна хорнова клауза, то атомарната формула φ ще наричаме заключение (или глава) на тази клауза, а редицата Γ  –  нейна предпоставка (или тяло). Ще записваме въпросната клауза във вида

    Забележка 1. Oпределението „хорнов“ произлиза от името на математика Алфред Хорн (Alfred Horn).

    Да се условим да казваме, че една атомарна формула φ следва в дадена структура S от дадена крайна редица от атомарни формули, ако φ следва в S от множеството на членовете на тази редица. За една положителна хорнова клауза (φ,Γ) ще казваме, че е в сила (или че е валидна) в дадена структура S, ако заключението φ на тази клауза следва в S от предпоставката Γ на клаузата. Казваме, че една структура S е модел за дадена хорнова програма, ако всички клаузи на тази програма са в сила в структурата S.

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

    За всяка хорнова програма съществуват безбройно много модели. Такива са поне онези структури, в които всички атомарни формули са тъждествено верни (очевидно всяко непразно множество е носител на поне една такава структура). Ако сред клаузите на дадена хорнова програма няма такава, която е с празна предпоставка, модели за тази програма ще бъдат и онези структури, в които никоя атомарна формула не е изпълнима. Интерес обикновено представляват такива модели за една хорнова програма, които не са от никой от тези два вида, а по-точно  –  модели, в които някои атомарни формули са тъждествено верни, а други не са.

    Пример 1. Нека сигнатурата Σ има функционални символи o и s, съответно нулместен и едноместен, и предикатни символи a и m  –  и двата триместни. Нека S° е структурата със сигнатура Σ и с носител множеството N на естествените числа, за която o^S° = 0,  s^S°(i) = i+1 при всеки избор на i в N,  a^S°(i,j,k) = 1 точно тогава, когато k е сборът на естествените числа i и j,  m^S°(i,j,k) = 1 точно тогава, когато k е произведението на естествените числа i и j. Като използваме, че всяко естествено число е стойност в S° на някой затворен терм, виждаме, че има безбройно много затворени атомарни формули, които са верни в S°, и безбройно много, които са неверни в S°. Лесно се проверява, че структурата S° е модел за следната хорнова програма:

a(o,Y,Y).

a(s(X),Y,s(Z)) :- a(X,Y,Z).

m(o,Y,o).

m(s(X),Y,Z) :- m(X,Y,U), a(U,Y,Z).

(при проверката се използва, че при всеки избор на естествените числа i и j са в сила равенствата  0+j = j,  (i+1)+j = (i+j)+1,  0j = 0,  (i+1)j = ij+j ). Разбира се, както за всяка хорнова програма и за тази съществуват безбройно много модели, включително и такива, в които всички затворени атомарни формули са верни.

    За всяка крайна редица Γ от атомарни формули и всяка субституция σ ще означаваме с Γσ редицата, получена чрез прилагането на σ към всеки от членовете на Γ, т.е. ако членовете на Γ са ψ₁, …, ψ_m, то членовете на Γσ ще бъдат ψ₁σ, …, ψ_mσ (в частност, ако редицата Γ е празна, то Γσ ще бъде също празна). Тази редица ще наричаме резултат от прилагането на σ към дадената редица. Като използваме обстоятелството, че за всяка атомарна формула ψ и всеки две субституции σ₁ и σ₂ е в сила равенството ψ(σ₁σ₂) = (ψσ₁)σ₂, виждаме, че е в сила аналогично твърдение и за прилагането на субституции към крайни редици от атомарни формули, а именно: за всяка крайна редица от атомарни формули Γ и всеки две субституции σ₁ и σ₂ е в сила равенството Γ(σ₁σ₂) = (Γσ₁)σ₂.

    Когато са дадени една положителна хорнова клауза (φ,Γ) и една субституция σ, резултат от прилагането на σ към дадената клауза ще наричаме клаузата (φσ,Γσ), която ще означаваме и с (φ,Γ)σ. Отбелязаното преди малко твърдение, отнасящо се до прилагане на произведение на две субституции към крайна редица от атомарни формули, се пренася и за положителни хорнови клаузи: за всяка положителна хорнова клауза C и всеки две субституции σ₁ и σ₂ е в сила равенството C(σ₁σ₂) = (Cσ₁)σ₂.

    Резултатите от прилагане на субституции към дадена крайна редица от атомарни формули или към дадена положителна хорнова клауза ще наричаме частни случаи съответно на редицата или на клаузата (един от тях е самата редица или клауза  –  получава се чрез прилагане на тъждествената субституция). Благодарение на изказаните по-горе твърдения за резултата от прилагане на произведение на две субституции към крайна редица от атомарни формули и към положителна хорнова клауза може да се твърди, че частните случаи на кой да е частен случай на такава редица или клауза са частни случаи и на самата нея. С помощта на точка А от следствие 2 във въпроса „Оператори за присвояване, съответни на субституция“ пък се вижда, че когато една положителна хорнова клауза е в сила в дадена структура S, всички частни случаи на тази клауза също са в сила в S. Това обстоятелство може в много случаи да се използва за намиране на атомарни формули, които са тъждествено верни във всички модели на дадена хорнова програма и са различни от заключенията на нейните клаузи с празна предпоставка.

    Пример 2. Нека S е произволен модел за хорновата програма от пример 1, а τ е произволен терм. Като приложим субституцията [Y/τ] към първата и към третата клауза на програмата, виждаме, че атомарните формули  а(о,τ,τ) и  m(о,τ,o) са тъждествено верни в S. Прилагайки към втората и към четвъртата клауза на програмата съответно субституцията [X/o, Y/τ, Z/τ] и субституцията [U/o, X/o, Y/τ, Z/τ], получаваме клаузите

a(s(o),τ,s(τ)) :- а(о,τ,τ).

m(s(o),τ,τ) :- m(o,τ,o), a(o,τ,τ).

Тези клаузи ще бъдат в сила в структурата S и, понеже за атомарните формули, които са членове на техните предпоставки, вече установихме, че са тъждествено верни в S, можем да заключим, че и заключенията им a(s(o),τ,s(τ)) и  m(s(o),τ,τ) също са тъждествено верни в S.

    Забележка 3. При сигнатурата от пример 1 могат да се посочат атомарни формули, които са тъждествено верни в структурата S°, но не са тъждествено верни в някой друг модел за програмата от същия пример. Такива са например атомарните формули a(X,o,X) и  m(X,o,o). Един модел за споменатата програма, в който никоя от тези две атомарни формули не е тъждествено вярна, е структурата S, определена по следния начин: носител на S е множеството от числата 0 и 1,  o^S е 0, функцията s^S има стойност 0 за всяко от числата 0 и 1, а  a^S и  m^S са един и същ предикат, чието множество на истинност се състои от тройките (0,0,0), (0,1,0) и (0,1,1). Все пак да отбележим, че при затворените атомарни формули положението в случая е друго  –  ако една затворена атомарна формула е вярна в структурата S°, то тази формула е вярна във всеки модел на разглежданата програма (това може да се докаже чрез индукция относно построението на терма, който е първи аргумент на въпросната атомарна формула).

    Обектите, към които биха могли да се прилагат хорновите програми, са крайните редици от атомарни формули. Ще наричаме тези редици хорнови запитвания (хорнови заявки) или за краткост просто запитвания (заявки). Хорново запитване с членове φ₁, …, φ_n ще записваме във вида

    Пример 3. От пример 2 се вижда, че всяка от субституциите [X/o] и [X/s(o)] е отговор на запитването

    Забележка 4. От забележка 1 във въпроса „Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура“ е ясно, че ако едно хорново запитване има отговор при дадена хорнова програма, то множеството на членовете на това запитване е изпълнимо във всеки модел за програмата. Обратното твърдение не е ни най-малко очевидно, но по-нататък в настоящия курс ще видим, че и то е вярно.

    Забележка 5. По дефиницията за хорново запитване празната редица е хорново запитване. Това запитване се удовлетворява от всяка субституция във всяка структура, следователно всяка субституция е негов отговор при всяка хорнова програма.

    Забележка 6. Ако сред клаузите на една хорнова програма няма нито една с празна предпоставка, то само празното запитване има отговор при тази програма. Това е ясно от обстоятелството, че в този случай съществува модел за програмата, в който никоя атомарна формула не е изпълнима.

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

    Прилагането на една хорнова програма към дадено хорново запитване представлява търсене на отговори на запитването при тази програма. Методът на търсенето се основава на една операция, наречена SLD-резолюция, с която предстои да се занимаем.

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