Логическо програмиране 2004/05 - упражнения

Език на предикатното смятане от първи ред (сигнатура) наричаме $$\Sigma$$=(Func;Pred;$$\rho$$) - множества от функционални и предикатни символи и тяхната местност (броя на аргументите им). Нека са дадени и други специални символи x₁,x₂,... които са изброимо безкрайно много и ще наричаме индивидни променливи.

Терм наричаме:

1. Всеки константен символ (0-местен функционален символ);
2. Всяка индивидна променлива
3. f(T₁,...,T_n), където f е n-местен функ. символ, а T₁,...,T_n са термове.

Атомарна формула (атом) наричаме:

1. Всеки 0-местен предикатен символ
2. p(T₁,...,T_n), където p е n-местен функ. символ, а T₁,...,T_n са термове.

Формула наричаме:

1. Всеки атом
2. F₁ & F₂, F₁ v F₂, not(F₁), F₁ -> F₂, F₁ <-> F₂, където F₁ и F₂ са формули
3. $$\exists x F_1$$, $$\forall x F_1$$, където F₁ е формула.

Структура наричаме S = ($$\Sigma$$, D, I), където $$\Sigma$$ е сигнатура, D е множество, което наричаме носител, а I - интерпретация на функционалните и предикатните символи до конкретни функции и предикати в D. Така структурата дава семантика на езика (сигнатурата). Оценка в S наричаме изображение v:VAR -> D, което дава стойност на индивидните променливи.

Стойност на терм в структура S при оценка v:

1. c^S,v = I(c) $$\in$$ D.
2. x^S,v = v(x).
3. f(T₁,...,T_n)^S,v = I(f)(T₁^S,v,...,T_n^S,v).

Стойност на формула в структура S при оценка v:

1. p(T₁,...,T_n)^S,v = I(p)(T₁^S,v,...,T_n^S,v).
2. (F₁ & F₂)^S,v = min(F₁^S,v,F₂^S,v).
   (F₁ v F₂)^S,v = max(F₁^S,v,F₂^S,v).
   (not(F₁))^S,v = 1-F₁^S,v.
   (F₁ -> F₂)^S,v = max(F₁^S,v,1-F₂^S,v).
   (F₁ <-> F₂)^S,v = 1 <=> F₁^S,v = F₂^S,v.
3. $$(\exists x F1)^{S,v} = max_{d\in D}(F_1^{S,v[x\rightarrow d]})$$.
   $$(\forall x F1)^{S,v} = min_{d\in D}(F_1^{S,v[x\rightarrow d]})$$.

Казваме, че F е тъждествено вярна в S (F^S = 1), ако за всяка оценка v в S, F^S,v = 1. Казваме, че F е предикатна тавтология, ако F^S = 1 за всяка структура S, т.е. формулата F е логически вярна независимо то обектите, за които се отнася.