Метод на резолюцията за множество от дизюнкти

Метод на резолюцията за множество от дизюнкти

под дизюнкт разбираме крайно множество от литерали; празното множество наричаме празен дизюнкт;

това съпоставяне не е взаимноеднозначно – на различни елементарни дизюнкции може да отговаря един и същи дизюнкт;

нека S е структура, v е оценка на променливите, D е дизюнкт;

казваме, че D е верен в S при оценката v, ако съществува L  D, така че L ^{S, v} = 1; така празният дизюнкт не е верен в никоя структура при никоя оценка;

ако S е структура, D е дизюнкт, казваме че D е тъждествено верен в S, ако D е верен в S при всяка оценка на променливите;

също една елементарна дизюнкция е тъждествено вярна в S  нейният съответен дизюнкт е тъждествено верен в S;

ясно е, че D е дизюнкт, тъй като D също е крайно множество от литерали;

D е верен в S при оценката v;

Доказателство: имаме D = (D₁\{ L₁})  (D₂\{ L₂}), където L₁  D₁ и

L₂  D₂ са противоположни литерали; нека D₁ и D₂ са вярни в S при оценката v; тогава някой литерал L  D₁ е верен в S при оценката v и някой литерал L  D₁ е верен в S при оценката v;

ако допуснем, че L = L₁ и L = L₂ ще получим, че противоположните литерали L₁ и L₂ са вярни в S при оценката v – противоречие;

така L  L₁ или L  L₂  L  D или L  D; така в D има литерал, който е верен в S при оценката v  D е верен в S при оценката v;

вярни в S, то непосредствената резолвента D също е тъждествено вярна в S;

ясно е, че D също е дизюнкт, тъй като ако L е литерал, то L също е литерал; при това, ако F е елементарна дизюнкция и D е нейният съответен дизюнкт, то е ясно, че съответният дизюнкт на F е D;

дизюнктът D наричаме частен случай на дизюнкта D; ще отбележим, че е възможно D да има по-малко членове от D – например, ако  е унификатор на някои два литерала от D;
Твърдение: нека D е дизюнкт, S е структура; ако D е тъждествено верен в S, то всеки частен случай на D е тъждествено верен в S;

Доказателство: нека D е тъждествено верен в S; тогава D  ,

D = { L₁, L₂, …, L_n}, n  1; образуваме елементарната дизюнкция

F = L₁  L₂  …  L_n; от по-горе F е тъждествено вярна в S;

нека  е субституция; имаме D = { L₁, L₂, …, L_n };

от друга страна F = L₁  L₂  …  L_n; тъй като F е тъждествено вярна в S, то F е тъждествено вярна в S и от по-горе D също е тъждествено верен в S;

D₁ и D₂, ако D е непосредствена резолвента на някой частен случай на D₁ и някой частен случай на D₂;

верен в S;

Доказателство: непосредствено от предните две твърдения;
нека M е множество от дизюнкти; модел на M наричаме структура, в която всички дизюнкти от M са тъждествено вярни;

разглеждаме въпроса дали съществува модел на M;

База: всички дизюнкти от M са резолвентно изводими от M;

Предположение: нека D₁ и D₂ са дизюнкти, които са резолвентно изводими от M;

Стъпка: ако D₁ и D₂ притежават резолвента D, то дизюнктът D е резолвентно изводим от M;

Заключение: няма други дизюнкти, които са резолвентно изводими от M;
нека S е модел на M;

с индукция по дефиницията се вижда, че ако един дизюнкт D е резолвентно изводим от M, то D е тъждествено верен в S;

при това положение, ако празният дизюнкт е резолвентно изводим от M, то M няма модел : ако допуснем, че M има модел S, ще получим, че празният дизюнкт е тъждествено верен в S, което е противоречие;
вярно е обратното твърдение – ако M няма модел, то празният дизюнкт е резолвентно изводим от M; това твърдение съвсем не е тривиално и е известно като теорема за пълнота на метода на резолюцията;
така методът на резолюцията се основава на следния критерий за неизпълнимост : едно множество от дизюнкти M е неизпълнимо  празният дизюнкт е резолвентно изводим от M;

нека M е множество от безкванторни формули; въпросът дали M има модел свеждаме до горните разглеждания по следния начин:

всяка формула от M привеждаме в конюнктивна нормална форма;

всички елементарни дизюнкции от получените формули заменяме със съответните им дизюнкти;

нека M е полученото множество от дизюнкти;

ясно е, че ако S е структура, то S е модел на M  S е модел на M;

питаме се дали M има модел; привеждаме формулите от M в конюнктивна нормална форма по алгоритъма;

{ s (b, X)  s (X, X) } -> { s (b, X)  s (X, X) }

{ s (X, X)  s (b, X) } -> { s (X, X)  s (b, X) } -> { s (X, X)  s (b, X) }

дизюнктите на множеството M са:

{ s (b, X), s (X, X) } и { s (X, X), s (b, X) };

частният случай на първия дизюнкт

{ s (b, X), s (X, X) }[X/b] = { s (b, b) } и частният случай на втория дизюнкт { s (X, X), s (b, X) }[X/b] = { s (b, b) } имат непосредствена резолвента празният дизюнкт; така празният дизюнкт е резолвентно изводим от множеството от M  M няма модел 

M няма модел;