Обосновка на твърденията в забележка 1
Първо да докажем изказаното в скобите общо твърдение.
И така, нека P е хорнова програма, G е хорнова цел, s
и m са субституции, s(G)
има проста резолвента Gў
с някоя клауза от P и целта m(Gў)
е тъждествено изпълнена при P. Като използваме инвариантността на простата резолюция относно субституции, заключаваме, че m(Gў) е проста резолвента на ms(Gў) с клауза от P. Оттук, от факта, че m(Gў)
е тъждествено изпълнена при P, и от коректността на простата резолюция следва, че 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)]).
Последно изменение: 21.05.2001 г.