Забележка 1. Когато искаме конкретните променливи от нашите разглеждания да могат да се използват без проблеми в Strawberry Prolog, трябва да избягваме еднобуквената променлива  _  и онези променливи, които започват с думата  G_.  Такова самоограничаване се налага поради особената роля в Strawberry Prolog на току-що споменатите променливи (знакът  _  е тъй наречената анонимна променлива, а променливите, започващи с  G_,  са тъй наречените глобални променливи).

      Понятието терм на предикатното смятане при дадена сигнатура Σ се дефинира индуктивно по следния начин: термове са константите на Σ, променливите и всички думи от вида φ(T₁,Т₂,…,Т_n), където n е положително цяло число, φ e n-местен функционален символ на Σ и T₁, Т₂, …, Т_n са термове. След като разполагаме с понятието терм, уславяме се да наричаме атомарни формули на предикатното смятане при сигнатура Σ нулместните предикатни символи на Σ и всички думи от вида π(T₁,Т₂,…,Т_n), където n е положително цяло число, π e n-местен предикатен символ на Σ и T₁, Т₂, …, Т_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)) е атомарна формула.

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

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

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

      Общото понятие за формула при сигнатура Σ ще въведем чрез следната индуктивна дефиниция: 
          0. Атомарните формули при сигнатура Σ и думите true и fail са формули при сигнатура Σ.
          1. За всяка формула F при сигнатура Σ думата not(F) също е формула при сигнатура Σ (нарича се отрицание на F).
          2. При всеки избор на цяло число n, по-голямо от 1, и на формули F₁, F₂, …, F_n при сигнатура Σ думите (F₁,F₂,…,F_n) и (F₁;F₂;…;F_n) също са формули при сигнатура Σ (наричат се съответно конюнкция на F₁, F₂, …, F_n и дизюнкция на F₁, F₂, …, F_n, а споменатите n формули се наричат членове на конюнкцията и на дизюнкцията).
          3. За всяка променлива ξ и всяка формула F при сигнатура Σ думите (ξ,F) и (ξ;F) също са формули при сигнатура Σ (наричат се съответно генерализация на F по ξ и екзистенциализация на F по ξ).

      Пример 3. Ako Σ е сигнатурата от пример 2 от предходния въпрос, то думите not(belongs(X,A)), (not(belongs(X,A));belongs(X,union(A,B))) и (X,belongs(X,singleton(X))) са формули.

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

      С дефиницията, която приехме, ние всъщност определихме какво да разбираме под конюнкция и под дизюнкция на произволна крайна редица от формули, имаща поне два члена. Удобно е да определим какво да разбираме под конюнкция и под дизюнкция още и на едночленна и на празна редица от формули, като при това да останат в сила изказаните преди малко условия за вярност на конюнкцията и на дизюнкцията. Това ще направим по следния начин: под конюнкция и под дизюнкция на едночленна редица от формули ще разбираме нейния единствен член, а под конюнкция и под дизюнкция на празна редица от формули ще разбираме съответно формулата true и формулата fail (ще ги наричаме празна конюнкция и празна дизюнкция).

      Ще използваме и следните означения за формули:
          1. Формулата not(F) ще означаваме с  ¬ F  (знакът  ¬  се чете "не" и се нарича знак за отрицание).
          2. При n>1 формулите (F₁,F₂,…,F_n) и (F₁;F₂;…;F_n) ще означаваме съответно с F₁ & F₂ & … & F_n и с F₁ ∨ F₂ ∨ … ∨ F_n  (знаците  &  и  ∨  се четат съответно като "и" и "или", като вместо първия от тях понякога се използва още и знакът  ∧ ; наричат се съответно знак за конюнкция и знак за дизюнкция).
          3. Формулите (ξ,F) и (ξ;F) ще означаваме съответно с  ∀ξ F  и с  ∃ξ F  (знаците  ∀  и  ∃  се четат съответно като "за всяко" и "за някое"; наричат се съответно квантор за общност и квантор за съществуване).

      Забележка 2. Означенията  F₁ & F₂ & … & F_n  и  F₁ ∨ F₂ ∨ … ∨ F_n  за конюнкция и дизюнкция биха могли да се използват и при n=1 благодарение на уславянето, което приехме относно конюнкция и дизюнкция на едночленна редица от формули. В някои общи разглеждания, при които n не е фиксирано и може да бъде и 0, ние ще използваме тези означения и без да изключваме нулата.

      Очевидно всички формули са стандартни изрази. Лесно се вижда, че не може да се случи една формула да бъде същевременно и терм  -  за атомарните формули това вече го проверихме, а за останалите то следва от еднозначния анализ на стандартните изрази и обстоятелството, че празната дума и думите true, fail, not не са нито функционални символи, нито променливи. Като използваме още веднъж еднозначния анализ на стандартните изрази, но този път в съчетание с обстоятелството, че изброените в предното изречение четири думи не са и предикатни символи, виждаме, че за формулите е налице еднозначно прочитане в смисъл аналогичен на онзи, който имахме при термовете.

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

      Забележка 3. Понятието за логическа формула, което въведохме, представлява само един от многото приемливи варианти на това понятие, различаващи се в едно или друго отношение, но свеждащи се по същество един към друг. Всъщност един по-обичаен подход е в дефиницията за логическа формула конюнкциите и дизюнкциите да са само с по два члена, а след това с помощта на такива конюнкции и дизюнкции да се определят конюнкции и дизюнкции и с друг брой членове - например F₁ & F₂ & F₃ да се определи като (F₁ & F₂) & F₃. Освен това невинаги се въвеждат формули от рода на true и fail, което обаче създава някои малки затруднения във връзка с празната конюнкция и празната дизюнкция.

      В много от нашите разглеждания ще имаме работа с един по-тесен клас от формули, които ще наричаме безкванторни. Казано накратко, това са формулите, които могат да се получат, без да се използва последната точка от индуkтивната дефиниция за формула. Точната дефиниция и на този клас от формули също е индуктивна и тя може да се изкаже така: атомарните формули при сигнатура Σ и формулите true и fail са безкванторни формули при сигнатура Σ, отрицанието на безкванторна формула при сигнатура Σ е пак безкванторна формула при сигнатура Σ, конюнкцията и дизюнкцията на безкванторни формули при сигнатура Σ са пак безкванторни формули при сигнатура Σ.

      Пример 4. От трите формули, споменати в пример 3, първите две са безкванторни, а последната не е.

      Накрая ще отбележим, че по естествен начин се дефинира индуктивно кои са функционалните символи от дадената сигнатура, участващи в даден терм, и кои са функционалните и предикатните символи от нея, участващи в дадена формула. След като се дадат тези дефиниции, лесно се доказва, че за всеки терм T съществува такава сигнатура, при която думата T е терм, че всяка сигнатура с това свойство е обогатяване на въпросната сигнатура. А именно, достатъчно е да разгледаме сигнатура с празно множество на предикатните символи, на която множеството от функционалните символи се състои точно от онези функционални символи, които участват в T, а указателят за брой на аргументите е рестрикция на указателя на дадената сигнатура за брой на аргументите. По подобен начин се доказва и аналогично твърдение за произволна формула.
 

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

Previous  Next  Contents