Пример 1. За всеки три атомарни формули φ, ψ и χ, където φ е различна и от ψ, и от χ, дизюнктът {ψ,¬χ} е непосредствена резолвента на дизюнктите {φ,ψ} и  {¬φ,¬χ} (в специалния случай, когато ψ=χ, споменатата непосредствена резолвента на {φ,ψ} и  {¬φ,¬χ} е всъщност дизюнктът {ψ,¬ψ}, а една друга тяхна непосредствена резолвента в този случай ще бъде дизюнктът {φ,¬φ}).

    Лема 1 (коректност на непосредствената резолюция). Всеки път, когато един дизюнкт е непосредствена резолвента на два дизюнкта, валидни в дадена структура, той също е валиден в нея.

    Доказателство. Нека δ₁ и δ₂ са дизюнкти, валидни в дадена структура S, а δ е дизюнкт, който е тяхна непосредствена резолвента, т.е. δ е обединение на δ₁\{λ₁} и δ₂\{λ₂} за някои два противоположни литерала λ₁ и λ₂, принадлежащи съответно на δ₁ и δ₂. Ще покажем, че и δ е валиден в структурата S. За целта да разгледаме произволна оценка v в S. Поради валидността на δ₁ в S някой литерал от δ₁ е верен в S при оценката v. Разглеждаме такъв литерал. Ако той е различен от λ₁, то той ще бъде литерал от δ, който е верен в S при оценката v. Ако пък въпросният литерал е λ₁, то не е възможно и противоположният му литерал λ₂ да е верен в S при оценката v. В този случай, използвайки валидността на δ₂ в S, разглеждаме литерал от δ₂, който е верен в S при оценката v и следователно е различен от λ₂. Значи и в този случай сред дизюнктите на δ ще има такъв, който е верен в S при оценката v.  _□

    Един дизюнкт ще наричаме резолвента на два дадени дизюнкта δ₁ и δ₂, ако той е непосредствена резолвента на някой частен случай на δ₁ и някой частен случай на δ₂. Тъй като всеки дизюнкт е свой частен случай (тъждествената субституция го преобразува в самия него), ясно е, че ако един дизюнкт е непосредствена резолвента на два дадени дизюнкта, той е и тяхна резолвента. Лесно се вижда, че обратното не е вярно.

    Пример 2. Нека  δ₁ = {p(a,Y)},  δ₂ = {¬p(X,b)},  където a и b са константи, а p е двуместен предикатен символ,. Тогава празният дизюнкт е резолвента на δ₁ и δ₂, защото е непосредствена резолвента на дизюнктите {p(a,b)} и {¬p(a,b)}, а те са частни случаи съответно на δ₁ и δ₂. От друга страна δ₁ и δ₂ очевидно нямат непосредствена резолвента.

    Лема 2 (коректност на резолюцията). Всеки път, когато един дизюнкт е резолвента на два дизюнкта, валидни в дадена структура, той също е валиден в нея.

    Доказателство. Използваме лема 1 и запазването на валидността при преминаване към частен случай на дизюнкт.  _□

    На лема 2 се основава тъй нареченият метод на резолюцията, предложен през 1965 г. от Джон Алън Робинсън (John Alan Robinson). Това е един метод за изследване дали дадено множество от дизюнкти притежава модел. Ще опишем накратко идеята на този метод, без да се впускаме в подробностите на неговото прилагане (например няма да се спираме на използването на техниката на унификацията при прилагането му).

    Образуването на резолвента на два дизюнкта ще наричаме извършване на резолюция. Да се условим да наричаме един дизюнкт резолвентно изводим от дадено множество от дизюнкти, ако той може да се получи от дизюнкти, принадлежащи на това множество чрез някакъв (евентуално нулев) брой извършвания на резолюция (допускането на нулев брой извършвания на резолюция осигурява, че дизюнктите от даденото множество също се считат резолвентно изводими от него). Благодарение на лема 2 можем да сме сигурни, че ако е дадено едно множество от дизюнкти, валидни в дадена структура S, то всеки дизюнкт, който е резолвентно изводим от това множество, също е валиден в S.

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

    С това, което сме направили дотук, лесно можем да докажем едната половина на горното твърдение – ако от едно множество от дизюнкти е резолвентно изводим празният дизюнкт, то това множество е неизпълнимо. И наистина, да допуснем, че от дадено множество от дизюнкти е резолвентно изводим празният дизюнкт и въпреки това множеството има модел. Този модел ще бъде структура, в която са валидни всички дизюнкти от даденото множество, а значи и всички дизюнкти, резолвентно изводими от него. Това обаче е невъзможно, защото празният дизюнкт, за който допуснахме, че е резолвентно изводим от даденото множество, не е валиден в никоя структура.

    Доста по-трудно се доказвa другата половина на твърдението – това, че от всяко множество от дизюнкти, което не притежава модел, е резолвентно изводим празният дизюнкт. Това твърдение, което ще наричаме теорема за пълнота на метода на резолюцията, ще бъде доказано по-нататък. То допуска разни усилвания. Най-важното от тях се състои в това, че при образуването на резолвенти частните случаи, на които се образуват непосредствени резолвенти, могат да се търсят чрез техниката на унификацията .

    Ще дадем някои примери, в които по метода на резолюцията се доказва несъществуването на модел за дадено множество от дизюнкти.

    Пример 3. Нека се интересуваме дали има модел множеството от два дизюнкта, разгледано в пример 2. Там показахме, че празният дизюнкт е резолвента на въпросните два дизюнкта. Следователно той е резолвентно изводим от въпросното множество и значи то не притежава модел.

    Пример 4. В пример 2 от въпроса „Прилагане на субституция към литерал и към дизюнкт“ разгледахме множеството Δ от двата дизюнкта  {p(X,Y), p(Y,X)}  и  {¬p(X,Y), ¬p(Y,X)},  където p е двуместен предикатен символ, и използвахме техните частни случаи {p(X,X)}  и  {¬p(X,X)},  за да заключим, че това множество няма модел. Същото заключение можем да направим и посредством метода на резолюцията, защото празният дизюнкт, бидейки непосредствена резолвента на въпросните частни случаи, е резолвента на двата дизюнкта от Δ (да отбележим, че двата дизюнкта от Δ имат и непосредствени резолвенти, но те не са подходящи за използване при прилагане на метода на резолюцията, защото са тавтологични дизюнкти).

    Пример 5. Да разгледаме множеството, състоящо се от четирите дизюнкта

    Пример 6. Заключението, което направихме в горния пример, може да се получи и чрез други начини на установяване на резолвентната изводимост на празния дизюнкт от разглежданото множество. Някои от тях имат предимството, че новите дизюнкти, получени преди да се стигне до празния, съдържат само по един литерал. Например бихме могли да работим така: първо образуваме резолвентата  {p(a)}  на дизюнктите  {p(X), q(X)}  и  {¬q(a)},  както и резолвентата  {¬p(a)}  на дизюнктите  {¬p(X), ¬r(X)}  и  {r(a)},  а след това от дизюнктите  {p(a)}  и  {¬p(a)}  получаваме празния дизюнкт.

    Забележка. В днешно време са свободно достъпни някои компютърни програми, позволяващи решаване на сложни логически задачи с помощта на метода на резолюцията. Такава е например програмата Prover 9, създадена от Уилям Мъкюн (William McCune).

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