Нека е дадена една сигнатура Σ. Положителни литерали при сигнатура Σ ще наричаме атомарните формули при тази сигнатура. Отрицателни литерали при сигнатура Σ ще наричаме думите от вида not(φ), където φ е атомарна формула при тази сигнатура. Положителните и отрицателните литерали при сигнатура Σ ще наричаме с общото наименование литерали при сигнатура Σ (както досега, обикновено няма да споменаваме сигнатурата Σ, когато тя се подразбира).

    За всяка атомарна формула φ съответния отрицателен литерал not(φ) ще наричаме отрицание на φ и ще го означаваме по-кратко с ¬φ (знакът  ¬  се чете „не“ и се нарича знак за отрицание). Благодарение на обстоятелството, че (по дефиницията за сигнатура) думата not не е нито предикатен, нито функционален символ, думата not(φ) не е нито атомарна формула, нито терм. Очевидно е, че по тази дума атомарната формула φ се възстановява еднозначно.

    Забележка 1. Отрицателният литерал not(φ) понякога бива означаван също и с −φ.

    За всяка атомарна формула φ променливи на отрицателния литерал ¬φ ще наричаме променливите на φ. Ще казваме, че този литерал е затворен, тогава, когато атомарната формула φ е затворена. Очевидно един литерал е затворен точно тогава, когато е празно множеството на неговите променливи.

    Ще казваме, че литералът ¬φ е верен в дадена структура S при дадена оценка v на променливите, тогава, когато атомарната формула φ не е вярна в S при оценката v. Ако φ е затворена атомарна формула, ще казваме, че литералът ¬φ е верен в дадена структура S, когато атомарната формула φ не е вярна в S.

    Под дизюнкт при сигнатура Σ ще разбираме произволно крайно множество от литерали при тази сигнатура (не изключваме и празното множество  –  ще го наричаме празен дизюнкт). Променлива на един дизюнкт ще наричаме такава променлива, която е променлива на поне един от принадлежащите му литерали. Един дизюнкт ще наричаме затворен, ако всеки от принадлежащите му литерали е затворен.

    За един дизюнкт ще казваме, че е валиден в дадена структура S, ако при всяка оценка v на променливите в тази структура някой от принадлежащите на дизюнкта литерали е верен в S при оценката v.

    Пример 1. Нека сигнатурата Σ и структурата S са онези, които бяха описани в пример 1 от въпроса „Хорнови програми“. Тогава следният дизюнкт е валиден в S (поради това, че ако произведението на две естествени числа е 0, то някое от тези числа също е 0):

    Пример 2. Нека S е структура, чийто носител е някое множество D от хора. Нека p е двуместен предикатен символ и p се интерпретира в S чрез двуместния предикат, приемащ стойност 1 точно за онези елементи на D², в които първият член е родител на втория (като употребяваме думата „родител“, тук подразбираме същински родител и изключваме например родителство по силата на осиновяване или по силата на втори брак на някой от същинските родители). Оказва се, че следните дизюнкти са валидни в S:

    Пример 3. Нека n е положително цяло число, а ξ₁, ξ₂, …, ξ_n са променливи. Лесно се вижда, че дизюнктът

    Пример 4. Нека a, b, x, y са такива четири души, че a е родител на x и на y, а b е родител на x, но не е родител на y (тази ситуация се среща в живота!). Нека S е структура от вида, разглеждан в пример 2, но с D={a,b,x,y}. Тогава дизюнктът

    За два литерала казваме, че са противоположни, ако единият от тях е атомарна формула, а другият е нейното отрицание. За един дизюнкт се казва, че е тавтологичен, ако има два противоположни литерала, които му принадлежат. Очевидно е, че тавтологичните дизюнкти при дадена сигнатура са валидни във всяка структура с тази сигнатура.

    Ясно е, че ако един дизюнкт е затворен, то неговата валидност в дадена структура е равносилна с това някой от принадлежащите му литерали да е верен в тази структура. Сред затворените дизюнкти има един, който не е валиден в никоя структура  –  това е празният дизюнкт.

    Модел за едно множество от дизюнкти се нарича такава структура, в която са валидни всички дизюнкти от това множество. Една основна задача във връзка с дизюнкти е изследването дали за дадено множество от дизюнкти съществува модел. Ще покажем как може да се сведе към нея въпросът дали на дадено хорново запитване съществува отговор при дадена хорнова програма. Нека P е дадена хорнова програма и Q е дадено хорново запитване. Знаем, че отговор на Q при P съществува точно тогава, когато множеството на атомарните формули, съставляващи редицата Q, е изпълнимо във всеки модел за P. Нека на всяка клауза на P съпоставим дизюнкта, състоящ се от заключението на клаузата и отрицанията на атомарните формули от нейната предпоставка. Не е трудно да се съобрази, че този дизюнкт е валиден в дадена структура точно тогава, когато клаузата е валидна в нея. Поради това структурите, които са модели за така полученото множество от дизюнкти, и структурите, които са модели за програмата P, са едни и същи. Да означим въпросното множество с Δ_P. Нека Q⁻ е дизюнктът, състоящ се от отрицанията на атомарните формули, съставляващи Q. Очевидно този дизюнкт е валиден в една структура точно тогава, когато в нея не е изпълнимо множеството на атомарните формули, съставляващи Q. Като вземем пред вид отбелязаните дотук свойства на множеството Δ_P и на дизюнкта Q⁻, виждаме, че отговор на Q при P съществува точно тогава, когато за множеството от дизюнкти Δ_P∪{Q⁻} не съществува модел.

    Пример 5. Нека хорновата програма P и хорновото запитване Q са такива както в примера към края на въпроса „Теорема за пълнота на SLD-резолюцията“, т.е. P се състои от клаузите

p(a,b).

p(X,Y) :- p(Y,X).

p(X,Y) :- p(X,Z), p(Y,Z).

(евентуално не в същата последователност), а Q е запитването

?- p(b,b).

Тогава Δ_P∪{Q⁻} се състои от следните четири дизюнкта:

    Забележка 2. Дизюнктите от множеството Δ_P∪{Q⁻}, съответстващо на произволна хорнова програма P и произволно хорново запитване Q, имат свойството, че във всеки от тях фигурира най-много един положителен литерал. За дизюнкт с това свойство е прието да се казва, че е хорнов. Дизюнктите, разгледани в примери 3 и 4 по-горе, са хорнови, а онези, за които става дума в примери 1 и 2, не са хорнови.

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