НАМИРАНЕ НА УДОВЛЕТВОРЯВАЩИ СУБСТИТУЦИИ
Ще предполагаме, че е дадено едно множество Γ от положителни хорнови клаузи. Знаем. че ако една положителна елементарна конюнкция е изпълнима във всеки модел за Γ и в сигнатурата, с която работим, има поне една константа, то съществува такъв затворен частен случай на конюнкцията, който е верен, а значи и тъждествено верен, във всеки модел за Γ. В много случаи могат да бъдат налице също и незатворени частни случаи на конюнкцията, които да са тъждествено верни във всеки модел за Γ (разбира се затворените частни случаи на кой да е такъв частен случай ще бъдат верни във всеки модел за Γ).
Пример 1. Нека p е двуместен предикатен символ, f и g са едноместни функционални символи и Γ се състои от атомарните формули p(X,f(X)) и
p(Y,g(Z)). Нека Q е конюнкцията
p(U,V) & p(V,U). Ако приложим към нея субституцията [U/g(Z),V/f(g(Z))], ще получим формулата
p(g(Z),f(g(Z))) & p(f(g(Z)),g(Z)).
Този частен случай на Q е тъждествено верен във всеки модел за Γ, защото е конюнкция на частен случай на първата клауза от Γ с частен случай на втората.
Когато е дадена една положителна елементарна конюнкция Q, удовлетворяваща субституция за Q при Γ ще наричаме такава субституция σ, че конюнкцията Qσ да бъде тъждествено вярна във всеки модел за Γ (следователно субституцията [U/g(Z),V/f(g(Z))] е една удовлетворяваща субституция за конюнкцията Q от горния пример при множеството Γ от същия пример). Поне при наличие на константа в сигнатурата е ясно, че за да съществува удовлетворяваща субституция за Q при Γ, необходимо и достатъчно е Q да е изпълнима във всеки модел за Γ. Ние знаем как с помощта на резолюция може да се установява такава изпълнимост. Сега ще покажем как резолюцията може да се използва и за намиране на удовлетворяваща субституция в този случай.
Нека една крайна редица Q0, Q1, …, Qk от положителни елементарни конюнкции е резолвентна редица относно Γ. Нейна асоциирана редица от субституции ще наричаме такава редица σ1, …, σk от събституции, че Qi е непосредствена резолвента на Qi −1σi с частен случай на някоя клауза от Γ при i = 1, …, k (ясно е, че такава редица σ1, …, σk съществува).
Пример 2. При условията на пример 1, тричленната редица Q, p(f(X),X), true е резолвентна редица относно Γ с асоциирана редица от субституции [U/X,V/f(X)], [X/g(Z)]. Очевидно произведението [U/X,V/f(X)][X/g(Z)] на членовете на тази асоциирана редица е равно на удовлетворяващата субституция [U/g(Z),V/f(g(Z))], за която стана дума преди малко. Това, че въпросното произведение е удовлетворяваща субституция за Q при Γ, не е случайно, а произтича от следното общо твърдение.
Теорема за удовлетворяващата субституция. Нека Q е положителна елементарна конюнкция и една резолвентна редица относно Γ, започваща с Q и завършваща с празната конюнкция, има асоциирана редица от субституции σ1, …, σk. Тогава произведението σ1…σk е удовлетворяваща субституция за Q при Γ.
Доказателство. Трябва да докажем, че формулата Q(σ1…σk) е тъждествено вярна във всеки модел за множеството Γ. Нека Q0, Q1, …, Qk е резолвентната редица, за която става дума в предположението на теоремата, и нека C1, …, Ck са такива частни случаи на клаузи от Γ, че Qi да е непосредствена резолвента на Qi −1σi с Ci при i = 1, …, k. Да положим
Qi = Qi σi +1…σk , i = 0, 1, …, k,
Ci = Ci σi +1…σk , i = 1, …, k.
Ако i е кое да е от числата 1, …, k, то, като вземем пред вид горните равенства заедно с равенството
Qi−1 = Qi−1σi σi +1…σk
и използваме инвариантността на непосредствената резолюция относно субституции, виждаме, че Qi е непосредствена резолвента на Qi−1 с Ci . Коректността на непосредствената резолюция позволява да заключим, че при i = 1, …, k формулата Qi −1 следва от множеството на формулите Ci и Qi . Да предположим сега, че S е някой модел за Γ. Понеже тъждествената вярност на една безкванторна формула се запазва при преход към неин частен случай, клаузите Ci са тъждествено верни в S. Поради това ако за дадено i от множеството {1,…,k} формулата Qi е тъждествено вярна в S, такава е и формулата Qi−1. Понеже Qk е празната конюнкция, а тя е вярна, а значи и тъждествено вярна, във всяка структура, ясно е, че всички формули Qi , където i∈{0,1,…,k}, са тъждествено верни в S. В частност такава е Q0 , а тя е всъщност формулата Q(σ1…σk ). □
Последно изменение: 11.06.2004 г.