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

      Коректност на последователните резолюции. Нека  Q₀, Q₁, …, Q_k  е резолвентна редица, основана на редицата от положителни хорнови клаузи  C₁, …, C_k.  Ако всички клаузи  C_i ,  i = 1, …, k,  са тъждествено верни в дадена структура  S,  а формулата  Q_k  е изпълнима в  S,  то формулата  Q₀  също е изпълнима в  S.

      Доказателство. Да предположим, че всички клаузи  C_i ,  i = 1, …, k,  са тъждествено верни в дадена структура  S.  Тогава споменатото преди малко твърдение от предходния въпрос показва, че при  i = 1, …, k,  ако  Q_i  е изпълнима в  S,  то  Q_i−1  също  е изпълнима в  S.  Значи ако формулата  Q_k  е изпълнима в  S,  то всички членове на разглежданата резолвентна редица, в това число и формулата  Q₀,  ще бъдат изпълними в  S.  _□

      Следствие. Нека  Γ  е множество от положителни хорнови клаузи. Ако една резолвентна редица относно  Γ  има за последен член празната конюнкция, то началният член на тази редица е изпълним във всеки модел за  Γ.

      Доказателство. Прилагаме твърдението за коректност на последователните резолюции, като в качеството на  S  вземаме произволен модел за  Γ  и използваме, че празната конюнкция е вярна във всяка структура.  _□

      Горното следствие дава един често пъти удобен метод за установяване на изпълнимост на дадена положителна елементарна конюнкция във всеки модел за дадено множество от положителни хорнови клаузи.

      Пример. Нека  Γ  се състои от атомарната формула  p(f(f(X)),f(X))  и от по-сложната хорнова клауза  p(X,f(Y)) :- p(X,f(Z)), p(Y,Z),  където  f  е едноместен функционален символ, а  p  е двуместен предикатен символ. Ще покажем, че във всеки модел за  Γ  е изпълнима формулата  p(U,U).  Това ще направим, като намерим резолвентна редица относно  Γ  с начален член  p(U,U)  и последен член  true. При търсенето на такава редица сме улеснени от обстоятелството, че  p(U,U)  няма резолвента с атомарната формула от  Γ  (защото не съществува атомарна формула, която да е частен случай едновременно на двете атомарни формули). От друга страна частният случай  p(f(Y),f(Y))  на  p(U,U)  съвпада със заключението на частния случай на другата клауза от  Γ,  получен чрез субституцията  [X/f(Y)].  Това показва, че  p(U,U)  има с въпросната клауза резолвента  p(f(Y),f(Z)) & p(Y,Z).  От своя страна тази конюнкция има резолвента  p(f(Z),Z)  с атомарната формула от  Γ,  защото субституцията  [Y/f(Z)]  преобразува първия член на конюнкцията във вариант на споменатата атомарна формула. Тъй като атомарната формула от  Γ  е частен случай на току-що получената резолвента, тези две формули пък имат празна резолвента. И така, намерихме резолвентната редица относно  Γ  с последователни членове

      Забележка. С помощта на Пролог изпълнимостта от горния пример може да се установи, като се изпълни програмата
        p(f(f(X)),f(X)).
        p(X,f(Y)) :- p(X,f(Z)), p(Y,Z).
върху запитването
        ?- p(U,U).
 

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

Previous  Next  Contents