Нека P е една хорнова програма. Някои затворени атомарни формули ще наречем изводими чрез P. Дефиницията е индуктивна и се състои от следните две точки:
        а) за всяка клауза от P, която е с празна предпоставка, всички затворени частни случаи на заключението на тази клауза са изводими чрез P;
        б) винаги, когато една клауза C° е затворен частен случай на клауза от P, имаща непразна предпоставка, и всички атомарни формули от предпоставката на C° са изводими чрез P, заключението на C° също е изводимо чрез P.

    Пример 1. Да предположим, че работим в сигнатура, чиито единствени функционални символи са константи a и b. Нека p е неин единствен предикатен символ и той е двуместен. Да разгледаме програма P, състояща се от следните три клаузи:

p(a,b).

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

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

Всевъзможните затворени атомарни формули при дадената сигнатура са следните четири:  p(a,a),  p(a,b),  p(b,a),  p(b,b). Ще покажем, че те всички са изводими чрез P. За формулата  p(a,b) това е ясно от обстоятелството, че тя е заключение на първата клауза от P, а предпоставката на тази клауза е празна. От изводимостта на формулата  p(a,b) получаваме, че е изводима и формулата  p(b,a)  –  за целта използваме, че втората клауза от P има затворения частен случай

    Пример 2. Да изменим пример 1, като от програмата P махнем втората клауза. Тогава измежду четирите възможни затворени атомарни формули изводимите чрез P ще бъдат две, а именно  p(a,a) и  p(a,b),

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

    Пример 3. Нека единствените функционални символи от сигнатурата са константата a и едноместният функционален символ f, а единственият предикатен символ  –  едноместният предикатен символ p. Нека P е следната хорнова програма:

p(a).

p(f(f(X))) :- p(X).

Тогава изводими чрез P са точно онези атомарни формули, които са от вида  p(f(…f(a)…)) с четен (евентуално нулев) брой участия на символа f.

    Пример 4. Нека пак единствените функционални символи от сигнатурата са константата  a и едноместният функционален символ f, но единствен предикатен символ да бъде двуместният предикатен символ p. Нека P е следната хорнова програма:

p(X,a).

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

Да се условим за произволно естествено число m да означаваме с τ_m онзи терм от вида f(…f(a)…),  който е с m участия на символа f. Тогава затворените атомарни формули, изводими чрез P, могат да бъдат охарактеризирани по следния начин: те са атомарните формули от вида p(τ_m,τ_n), където m и n са неотрицателни цели числа, удовлетворяващи неравенството  m ≥ n.

    Пример 5. При същата сигнатура както в пример 3 нека P е програмата

p(a).

p(f(f(X))) :- p(X).

p(f(f(f(X)))) :- p(X).

Описание на изводимите чрез P затворени атомарни формули можем да получим, като използваме лесно доказуемото твърдение, че всяко цяло число, по-голямо от 1, допуска представяне във вида 2k+3l, където k и l са неотрицателни цели числа. С помощта на това твърдение можем да се убедим, че въпросните атомарни формули са точно онези, които са от вида  p(f(…f(a)…)) с различен от 1 (евентуално нулев) брой участия на символа f (това са всъщност всички затворени атомарни формули при дадената сигнатура с изключение на формулата  p(f(a))).

    Да се върнем отново към общия случай, когато P е произволна хорнова програма. От втората основна лема за ербрановите структури (вж. въпроса „Ербранови структури“) следва съществуване на точно една ербранова структура със свойството, че в нея са верни онези и само онези затворени атомарни формули, които са изводими от P. Ербрановата структура с това свойство ще наричаме ербранова структура, породена от P, и ще я означаваме с S_P. Ще докажем едно много съществено твърдение за тази структура.

    Теорема за минималния ербранов модел. Структурата S_P е модел за програмата P и при всеки избор на затворена атомарна формула θ следните три условия са равносилни помежду си: 1) θ е вярна в S_P; 2) θ е изводима чрез P; 3) θ е вярна във всеки модел за P.

    Доказателство. Да означим за краткост структурата S_P с S. За да докажем, че тя е модел за P, да разгледаме произволна клауза C от P. Ще покажем, че C е валидна в структурата S. Да означим с φ заключението на C. Ще разгледаме първо случая, когато предпоставката на C е празна. Нека v е произволна оценка в S на променливите. Разглеждаме такава субституция σ, че  σ(ξ) = v(ξ) за всяка променлива ξ от множеството VAR(φ) (субституция с това свойство съществува, понеже въпросното множество е крайно). По лемата за свеждане на вярност при оценка към вярност на затворен частен случай (вж. въпроса „Ербранови структури“) може да се твърди, че атомарната формула φσ е затворена и е в сила равенството φ^S,v = (φσ)^S. По точка а) от дефиницията за изводимост чрез P затворената формула φσ е изводима чрез P и следователно е вярна в структурата S. Но тогава, по отбелязаното по-горе равенство, формулата φ е вярна в структурата S при оценката v. С това показахме валидността в S на клаузата C в случая, когато тя е с празна предпоставка. Сега ще се занимаем със случая, когато предпоставката на C не е празна. Нека въпросната предпоставка да има за членове атомарните формули ψ₁, …, ψ_m и нека v е оценка в S на променливите, при която в S е вярна всяка от тези формули. Разглеждаме такава субституция σ, че да имаме равенството  σ(ξ) = v(ξ) за всяка променлива ξ от множеството VAR(C) (субституция с това свойство съществува, понеже VAR(C) е крайно). По лемата за свеждане на вярност при оценка към вярност на затворен частен случай може да се твърди, че атомарните формули ψ₁σ, …, ψ_mσ и φσ са затворени и са в сила равенствата

   Остана да покажем, че за всяка затворена атомарна формула θ условията 1), 2) и 3) са равносилни помежду си. Равносилността на първите две от тези условия произтича от дефиницията на структурата S_P. След като сме доказали, че тя е модел за P, ясно е също, че от условието 3) следва условието 1). При това положение е достатъчно да покажем, че от условието 2) следва условието 3), т.е. да покажем, че затворените атомарни формули, изводими чрез P, са верни във всеки модел за P. Това можем да направим чрез индукция, съобразена с дефиницията за изводимост чрез P, като вземем пред вид. че когато една структура е модел за P, всички клаузи на P са валидни в тази структура и следователно техните затворени частни случаи също са валидни в нея (използваме твърдението за запазване на валидността на клаузите при преминаване към техни частни случаи, отбелязано във въпроса „Хорнови програми“).  _□

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

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