Обосновка на твърденията в забележка 1
Първо да докажем изказаното в скобите общо твърдение.
И така, нека P е хорнова програма, G е хорнова цел, s
и m са субституции, s(G)
има непосредствена резолвента Gў
с частен случай на някоя клауза от P и целта m(Gў)
е тъждествено изпълнена при P. Тогава за някоя атомарна формула
A и някои цели R и B имаме равенствата
G=[A|R], Gў=Bs(R),
като клаузата
s(A) :- B.
е частен случай на клауза от P. От написаните равенства следват
равенствата
ms(G)=[ms(A)|ms(R)],
m(Gў)=m(B)ms(R),
а клаузата
ms(A) :- m(B).
също е частен случай на клауза от P, следователно е тъждествено
вярна във всеки модел за P. Тъй като m(Gў)
е тъждествено изпълнена при P, такива са също m(B)
и ms(R). Но щом целта m(B)
е тъждествено изпълнена при P, атомарната формула ms(A)
ще бъде тъждествено вярна във всеки модел за P благодарение на казаното
преди малко за клаузата с тяло m(B)
и глава ms(A). По този начин
виждаме, че всички атомарни формули, които са членове на ms(G),
са тъждествено верни в кой да е модел за P.
Сега ще покажем с помощта на доказаното твърдение,
че наистина субституцията [f(f(f(X)))=:U] преобразува
целта [p(U,U)] в такава, която е тъждествено изпълнена
при програмата P от пример 4. Имахме основаната на
P резолвентна верига
[p(U,U)], [p(f(Y),f(Z)),p(Y,Z)], [p(f(Z),Z)],
[],
при това за всеки неин член без последния можем да посочим субституция,
която, приложена към него, дава цел, от която следващият член на веригата
се получава като непосредствена резолвента с частен случай на някоя програмна
клауза. Споменатите субституции са следните: [f(Y),f(Y)=:U,X],
[f(Z)=:Y] и [f(X)=:Z].
При първото прилагане на общото твърдение вземаме
G=[p(f(Z),Z)], Gў=[],
s=[f(X)=:Z], m=[=:].
Заключението, което получаваме, е, че целта [f(X)=:Z]([p(f(Z),Z)])
е тъждествено изпълнена при P (разбира се верността на това заключение
е и непосредствено очевидна). При следващото прилагане на общото твърдение
вземаме
G=[p(f(Y),f(Z)),p(Y,Z)], Gў=[p(f(Z),Z)],
s=[f(Z)=:Y], m=[f(X)=:Z].
Получаваме заключението, че целта [f(X)=:Z][f(Z)=:Y]([p(Y,Z),p(f(Y),f(Z))])
е тъждествено изпълнена при P. Още веднаж прилагаме общото твърдение
- сега при
G=[p(U,U)], Gў=[p(f(Y),f(Z)),p(Y,Z)],
s=[f(Y),f(Y)=:U,X],
m=[f(X)=:Z][f(Z)=:Y].
Заключението е, че целта [f(X)=:Z][f(Z)=:Y][f(Y),f(Y)=:U,X]([p(U,U)])
е тъждествено изпълнена при P. Разбира се, за нас е важно как действа
субституцията [f(X)=:Z][f(Z)=:Y][f(Y),f(Y)=:U,X]
върху единствената променлива U на целта [p(U,U)].
Имаме
[f(X)=:Z][f(Z)=:Y][f(Y),f(Y)=:U,X](U)
= [f(X)=:Z][f(Z)=:Y](f(Y)) = [f(X)=:Z](f(f(Z)))
= f(f(f(X))).
Значи тъждествено вярната при P цел [f(X)=:Z][f(Z)=:Y][f(Y),f(Y)=:U,X]([p(U,U)])
съвпада с целта [f(f(f(X)))=:U]([p(U,U)]).
Последно изменение: 16.05.2000 г.