Забележка 1. Често използван подход при теоретичните разглеждания в областта на логическото програмиране е вместо положителни елементарни конюнкции да се използват еквивалентните на техните отрицания отрицателни хорнови клаузи. При такъв подход дефиницията за непосредствена резолвента би изглеждала по следния начин: ако A₁, A₂, …, A_m и B₁, …, B_n  (където m > 0, n ≥ 0)  са атомарни формули, то непосредствена резолвента на отрицателната клауза  :- A₁, A₂, …, A_m  с положителната клауза  A₁ :- B₁, …, B_n  ще наричаме отрицателната клауза  :- B₁, …, B_n, A₂, …, A_m.  На горния пример тогава би отговаряло следното: ако  F₀, F₁, F₂, F₃, F₄  са атомарни формули, то отрицателната клауза  :- F₀, F₁, F₂  има с двете положителни клаузи  F₀ :– F₃, F₂, F₄  и  F₀  непосредствени резолвенти съответно  :- F₃, F₂, F₄, F₁, F₂  и  :- F₁, F₂,  а отрицателната клауза  :- F₀  има със същите две положителни клаузи непосредствени резолвенти съответно  :- F₃, F₂, F₄  и  fail  (празната дизюнкция).

      В сила са следните две свойства на непосредствената резолюция.

      Инвариантност на непосредствената резолюция относно субституции. Нека една положителна елементарна конюнкция  Q  има с дадена положителна хорнова клауза  C  непосредствена резолвента  Q ′  и нека  σ  е произволна субституция. Тогава формулата  Qσ  има с клаузата  Cσ  непосредствена резолвента  Q ′σ.

      Доказателство. Нека  Q  има вида  A₁ & A₂ & … & A_m ,  а  C   -  вида  A₁ :- B₁, …, B_n ,  където  A₁, A₂, …, A_m  и  B₁, …, B_n  са атомарни формули. Тогава  Q ′  е конюнкцията  B₁ & … & B_n & A₂ & … & A_m ,  а  Qσ  и  Cσ  са съответно конюнкцията  A₁σ & A₂σ & … & A_mσ,  и клаузата  A₁σ :- B₁σ, …, B_nσ.  Оттук е ясно, че  Qσ  има с  Cσ  непосредствена резолвента  B₁σ & … & B_nσ & A₂σ & … & A_mσ,  a това е точно формулата  Q ′σ.  _□

      Коректност на непосредствената резолюция. Нека една положителна елементарна конюнкция  Q  има с дадена положителна хорнова клауза  C  непосредствена резолвента  Q ′.  Тогава от множеството от двете формули  C  и  Q ′  следва формулата  Q.

      Доказателство. Да предположим, че формулите  C  и Q ′  са верни в дадена конфигурация. Тъй като всички предпоставки на клаузата  C  и всички членове на конюнкцията  Q  след първия са членове и на Q ′,  те поради верността на  Q ′  във въпросната конфигурация също са верни в нея. Първият член на  Q  пък е верен в тази конфигурация благодарение на верността в нея на клаузата  C  и на нейните предпоставки. И така, всички членове на конюнкцията  Q  са верни в разглежданата конфигурация, следователно и  Q  е вярна в нея.  _□

      Забележка 2. Коректността, която току-що доказахме, се отличава по своя характер от обикновено разглежданата в логиката. Когато в логиката се обсъжда някакъв начин, чрез който от известен брой дадени формули в определени случаи се получава нова, коректността на този начин най-често означава, че новата формула следва от множеството на онези, от които тя е получена (понякога въпросната коректност означава нещо малко по-слабо, но пак в такъв дух, а именно, че винаги, когато формулите, от които е получена новата формула, са тъждествено верни в дадена структура, новата формула също е тъждествено вярна в тази структура). Подобно разбиране на коректността съответства на тъй наречения синтетичен начин на разсъждение, при който от твърдения, чиято вярност е установена, се получават нови верни твърдения. При непосредствената резолюция на положителни елементарни конюнкции с положителни хорнови клаузи следването е до известна степен в обратната посока, а именно от новата формула и втората от онези, от които тя е получена, следва първата. Това донякъде съответства на тъй наречения аналитичен начин на разсъждение - при него се придвижваме от твърдения, чиято вярност искаме да установим, към твърдения, които биха я гарантирали, ако се окажат верни. Добре е да споменем обаче, че ако вместо с положителни елементарни конюнкции бихме работили с отрицателни хорнови клаузи (вж. забележка 1), то коректността на непосредствената резолюция би била от същия характер както обикновено разглежданата в логиката, при това в силния й вид (може би това е една от причините често да се предпочита споменатият в забележка 1 друг подход).

      Случаите, когато една положителна елементарна конюнкция и една положителна хорнова клауза имат непосредствена резолвента, са сравнително редки. Затова ще въведем едно доста по-общо понятие за резолвента (то ще може да е от полза дори и понякога, когато съществува непосредствена резолвента). Дефиницията му е следната: резолвента на дадена положителна елементарна конюнкция с дадена положителна хорнова клауза ще наричаме всяка формула, която е непосредствена резолвента на някой частен случай на дадената конюнкция с някой частен случай на дадената клауза (всяка такава формула е пак положителна елементарна конюнкция). Разбира се образуването на резолвента ще наричаме резолюция.

      Пример 2. Нека p и q са двуместни предикатни символи, r е едноместен предикатен символ, a и b са константи. Конюнкцията  p(X,b) & q(X,Z)  и клаузата  p(a,X) :– q(X,Z), r(Z)  очевидно нямат непосредствена резолвента. Въпреки това те имат резолвента (имат даже безбройно много резолвенти). И наистина, частните случаи на дадената конюнкция са конюнкциите от вида  p(T,b) & q(T,U),  където  T  и  U  са термове. Частните случаи пък на дадената клауза  -  това са клаузите от вида  p(a,V) :– q(V,W), r(W),  където  V  и  W  са термове. Ясно е, че един частен случай на конюнкцията и един частен случай на клаузата допускат непосредствена резолюция точно тогава, когато имат съответно вида  p(a,b) & q(a,U)  и вида  p(a,b) :– q(b,W), r(W)  за някой терм  U  и някой терм  W.  Оттук виждаме, че резолвенти на дадената конюнкция с дадената клауза са точно конюнкцияите, които имат вида  q(b,W) & r(W) & q(a,U)  за някой терм  W  и някой терм  U.  Измежду така описаните резолвенти има най-обща, т.е. такава, на която всички те са частни случаи. А именно, в качеството на най-обща резолвента бихме могли да вземем коя да е конюнкция от горния вид, в която термовете  W  и  U  са различни помежду си променливи.

      Разбира се съвсем лесно може да се даде и пример на положителна елементарна конюнкция и положителна хорнова клауза, които нямат резолвента и в разглеждания по-общ смисъл. По-интересно е да дадем пример за положителна елементарна конюнкция и положителна хорнова клауза, които имат непосредствена резолвента, но тя не е най-обща измежду техните резолвенти.

      Пример 3. Да разгледаме частния случай  p(a,b) & q(a,Z)  на конюнкцията от предходния пример и частния случай  p(a,b) :– q(b,Z), r(Z)  на клаузата от същия пример. Тяхна непосредствена резолвента е конюнкцията  q(b,Z) & r(Z) & q(a,Z),  но съществуват други техни резолвенти, които не са нейни частни случаи. За да се убедим в това, достатъчно е да забележим, че общият вид на резолвентите в настоящия пример е същият както в предходния.

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

      От семантична гледна точка общото понятие за резолвента е полезно благодарение на следващото твърдение.

      Коректност на резолюцията. Нека една положителна елементарна конюнкция  Q  има с дадена положителна хорнова клауза  C  резолвента  Q ′.  Ако  C  е тъждествено вярна в дадена структура  S,  а  Q ′  е изпълнима в  S,  то  Q  също е изпълнима в  S.

      Доказателство. Формулата  Q ′  е непосредствена резолвента на някой частен случай  Q^o  на  Q  с някой частен случай  C^o  на  C.  Да предположим, че  C  е тъждествено вярна в дадена структура  S,  а  Q ′  е изпълнима в  S.  Тогава клаузата  C^o  също е тъждествено вярна в  S,  а формулата  Q ′  е вярна в  S  при някоя оценка на променливите. Благодарение на коректността на непосредствената резолюция можем да твърдим, че и формулата   Q^o  е вярна в  S  при тази оценка на променливите. Това показва, че частният случай  Q^o  на  Q  е изпълним в  S  и следователно  Q  също е изпълнима в  S.  _□

      Забележка 3. Ако вместо с положителни елементарни конюнкции бихме работили с отрицателни хорнови клаузи, то коректността на резолюцията би била от характера на обикновено разглежданата в логиката коректност, макар и в нейния по-слаб вид, споменат в забележка 2.
 

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

Previous  Next  Contents