Да предположим, че е дадена една конфигурация (S,v), където S=(Σ,D,I). Стойността на произволен терм τ в тази конфигурация ще бъде подходящо определен елемент на множеството D, който ще означаваме с τ^S,v. Дефиницията на този елемент е индуктивна и има следния вид, като коректността й се обосновава с еднозначния прочит на термовете: ако термът τ е константа на Σ, полагаме τ^S,v = τ^S  (т.е. τ^S,v = I(τ) ), ако τ е променлива, полагаме τ^S,v = v(τ), а ако τ = ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ на Σ и τ₁, …, τ_n са термове, приемаме, че τ^S,v = ω^S(τ₁^S,v,…,τ_n^S,v)  (т.е. че τ^S,v = I(ω)(τ₁^S,v,…,τ_n^S,v) ). Елемента τ^S,v ще наричаме още стойност на τ в структурата S при оценката v.

      Стойността на произволна атомарна формула φ в конфигурацията (S,v) ще бъде пък някой елемент на множеството {0,1}, който ще означаваме с φ^S,v. А именно, ако φ = π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ на Σ и τ₁, …, τ_n са термове, то полагаме φ^S,v = π^S(τ₁^S,v,…,τ_n^S,v)  (т.е. φ^S,v = I(π)(τ₁^S,v,…,τ_n^S,v) ), a ako φ е нулместен предикатен символ на Σ, полагаме φ^S,v = φ^S  (т.е. φ^S,v = I(φ) ). Елемента φ^S,v ще наричаме още стойност на φ в структурата S при оценката v.

      За една атомарна формула φ ще казваме, че е вярна (или изпълнена) в дадена конфигурация (S,v), ако е в сила равенството φ^S,v = 1. Вместо да казваме, че атомарната формула φ е вярна в конфигурацията (S,v), ще казваме още, че φ е вярна в структурата S при оценката v, или че v удовлетворява φ в S. За да изразим, че φ е вярна в конфигурацията (S,v), ще си служим и с означението S,v ⊨ φ. Чрез означението S,v ⊭ φ ще изразяваме пък това, че φ не е вярна в конфигурацията (S,v), т.е. че имаме равенството φ^S,v = 0.

      За една атомарна формула φ ще казваме, че е тъждествено вярна в дадена структура S, ако φ е вярна в S при всяка оценка на променливите, а ще казваме, че φ е изпълнима в S, ако φ е вярна в S при поне една оценка на променливите. За едно множество Γ от атомарни формули ще казваме, че е изпълнимо в дадена структура S, ако съществува такава оценка v на променливите в S, че всички формули от Γ да бъдат верни в S при оценката v. За всяка такава оценка ще казваме, че удовлетворява Γ в S. Разбира се, една оценка удовлетворява дадена атомарна формула φ в дадена структура S точно тогава, когато тази оценка удовлетворява в S множеството с единствен елемент φ.

      Пример 1. Атомарните формули   p(s(X),a(b(X)))  и   p(s(X),a(s(b(X))))  са тъждествено верни в структурата, разгледана в пример 3 от въпроса за сигнатури и структури, атомарната формула   p(X,X)  не е изпълнима в тази структура, а множеството от двете атомарни формули   d(X)  и   d(a(b(X)))  е изпълнимо в нея, защото се удовлетворява в нея от коя да е оценка, съпоставяща на променливата X празната дума.

      За една атомарна формула φ ще казваме, че следва в дадена структура S от дадено множество Γ от атомарни формули, и ще пишем φ <=_S Γ, ако φ е вярна в S при всяка оценка на променливите в S, която удовлетворява Γ в S. Когато множеството Γ се състои от един единствен атом ψ, вместо да казваме, че φ следва в S от Γ, ще казваме още, че φ следва в S от ψ, и ще пишем φ <=_Sψ.

      Пример 2. Нека S е структурата, за която става дума в предходния пример. Тогава атомарната формула   d(Y)  следва в S от множеството от двете атомарни формули   p(X,Y)  и   d(X),  а всяка от атомарните формули   p(a(X),a(Y)),  p(b(X),b(Y))  и   p(s(X),s(Y))  следва в S от атомарната формула   p(X,Y).

      Забележка 1. Следното очевидно свойство играе съществена роля за обосноваването на метода, по който в Пролог се изпълняват логически програми: ако една формула φ следва в дадена структура S от дадено множество Γ от атомарни формули, а Δ е произволно множество от атомарни формули, то всяка оценка в S, която удовлетворява в S обединението на множествата Γ и Δ, удовлетворява в S също и множеството {φ}∪Δ. Казано другояче, ако φ следва в S от Γ, то за да удовлетворява в S една оценка множеството {φ}∪Δ, достатъчно е тя да удовлетворява в S множеството Γ∪Δ.

      Забележка 2. Нека S е дадена структура. Ако Γ е празното множество, то по тривиални причини за всяка оценка в S е в сила твърдението, че тя удовлетворява Γ в S. Поради това една атомарна формула следва в S от празното множество точно тогава, когато тя е тъждествено вярна в S.

      Забележка 3. Нека S е дадена структура. Ако Γ е множество от атомарни формули, което е неизпълнимо в S, то по тривиални причини всяка атомарна формула следва в S от множеството Γ.

      Дотук се занимавахме със стойности на термове и атомарни формули в една фиксирана структура. Да предположим сега, че са дадени структура S със сигнатура Σ и нейно обогатяване S′, което е със сигнатура Σ′. Понеже Σ′ съдържа Σ, термовете и атомарните формули при сигнатура Σ същевременно са съответно термове и атомарни формули при сигнатура Σ′. Освен това, тъй като S и S′ имат един и същ носител, всяка оценка на променливите в S е тяхна оценка в S′ и обратно. С индукция се доказва, че за всеки терм τ в сигнатура Σ и всяка оценка v на променливите в S имаме равенството τ^S,v = τ^S′,v, а след това се установява, че φ^S,v = φ^S′,v за всяка атомарна формула φ в сигнатура Σ и всяка оценка v на променливите в S.

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