Термове и атомарни формули на предикатното смятане

ТЕРМОВЕ И АТОМАРНИ ФОРМУЛИ НА ПРЕДИКАТНОТО СМЯТАНЕ

За всяка сигнатура Σ някои думи над допълнената основна азбука на Пролог ще бъдат наречени термове на предикатното смятане при сигнатура Σ или по-кратко термове при сигнатура Σ, а други ще бъдат наречени атомарни формули на предикатното смятане при сигнатура Σ или по-кратко атомарни формули при сигнатура Σ (когато сигнатурата Σ се подразбира, обикновено няма да я споменаваме и ще говорим просто за термове и за атомарни формули; така ще постъпваме и при другите понятия, зависещи от сигнатурата, които ще въведем по-нататък). Атомарните формули ще наричаме още атоми.

Понятието терм при дадена сигнатура Σ се дефинира индуктивно по следния начин: термове са променливите, константите на Σ и всички думи от вида ω(τ₁,τ₂,…,τ_n), където n е положително цяло число, ω e n-местен функционален символ на Σ и τ₁, τ₂, …, τ_n са термове. След като разполагаме с понятието терм, уславяме се да наричаме атомарни формули на предикатното смятане при сигнатура Σ нулместните предикатни символи на Σ и всички думи от вида π(τ₁,τ₂,…,τ_n), където n е положително цяло число, π e n-местен предикатен символ на Σ и τ₁, τ₂, …, τ_n са термове.

Пример 1. Ako Σ е сигнатурата от пример 1 от въпроса за сигнатури и структури, то думите b(s(a(a(e)))) и a(s(b(X))) са термове, а думите p(e,e), d(a(a(b(b(e))))) и p(X,a(Y)) са атомарни формули.

Пример 2. Ako Σ е сигнатурата от пример 2 от въпроса за сигнатури и структури, то думата union(singleton(a),singleton(b)) е терм, а думата belongs(X,union(A,B)) е атомарна формула.

Пример 3. Ako Σ е сигнатурата от пример 5 от въпроса за сигнатури и структури, то думите

the_oldest, the_next_after(the_oldest), the_next_after(the_next_after(X)) са термове, а думите is_male(the_oldest), is_male(the_next_after(the_oldest)), is_parent_of(the_oldest,the_next_after(the_next_after(X))) са атомарни формули.

Забележка 1. Очевидно е, че ако сигнатурата Σ е с празно множество на функционалните символи, то единствените термове са променливите, а ако Σ е с празно множество на предикатните символи, то не съществуват атомарни формули.

Като се използват свойствата на допустимите и на силно допустимите думи, с индукция, съобразена с дефиницията за терм, се показва, че всички термове са силно допустими думи, а оттам се получава същото и за атомарните формули. Това, че термовете при дадена сигнатура са силно допустими думи, заедно с лемата за еднозначния прочит и с обстоятелството, че никоя дума не е едновременно константа и променлива, осигурява еднозначното прочитане на термовете и на атомарните формули в следния смисъл: трите случая в дефиницията за терм се изключват взаимно, като в третия от тях числото n, функционалният символ ω и термовете τ₁, τ₂, …, τ_n се определят еднозначно по дадения терм, а също двата случая в дефиницията за атомарна формула се изключват взаимно и във втория от тях числото n, предикатният символ π и термовете τ₁, τ₂, …, τ_n се определят еднозначно по дадената атомарна формула (тези термове ще наричаме аргументи на въпросната атомарна формула). Освен това никоя атомарна формула не е терм, тъй като никой предикатен символ не е същевременно функционален символ или променлива.

Ако са дадени две сигнатури Σ и Σ′, където Σ′ съдържа Σ, една проста индукция показва, че всеки терм при сигнатура Σ е терм и при сигнатура Σ′, а оттук пък следва, че всяка атомарна формула при сигнатура Σ е атомарна формула и при сигнатура Σ′.

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

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