За един дизюнкт ще казваме, че е верен в дадена структура S при дадена оценка v на променливите в тази структура, ако някой от принадлежащите на дизюнкта литерали е верен в S при оценката v. Ще казваме за един дизюнкт, че е тъждествено верен в дадена структура, ако той е верен в нея при всяка оценка на променливите в нея. Под модел за едно множество от дизюнкти ще разбираме структура, в която всички дизюнкти от въпросното множество са тъждествено верни.

    За един затворен дизюнкт ще казваме, че е верен в дадена структура, ако някой от принадлежащите му литерали е верен в нея. Очевидно е, че един затворен дизюнкт е тъждествено верен в дадена структура точно тогава, когато е верен в нея; поради това една структура е модел за дадено множество от затворени дизюнкти точно тогава, когато те всички са верни в нея.

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

    За два литерала ще казваме, че са противоположни, ако единият от тях е атомарна формула, а другият е нейното отрицание. За един дизюнкт ще казваме, че е тавтологичен, ако има два противоположни литерала, които му принадлежат. Очевидно е, че тавтологичните дизюнкти са тъждествено верни във всяка структура.

    За всяка елементарна дизюнкция множеството на нейните членове е един дизюнкт. Ще го наричаме съответен на нея (понеже всяка елементарна дизюнкция има поне един член, съответният дизюнкт не е никога празен). Ако φ е една елементарна дизюнкция и δ е съответният й дизюнкт, то верността на φ в дадена структура S при дадена оценка v на променливите и тъждествената вярност на φ в S очевидно са равносилни съответно с верността на δ в S при оценката v и тъждествената вярност на δ в S. Добре е да отбележим обаче, че различни елементарни дизюнкции могат да имат един и същ съответен дизюнкт, защото съответният дизюнкт на една елементарна дизюнкция не се променя, ако повторим някой от нейните членове или извършим разместване на членовете й.

    От представимостта на безкванторните формули в конюнктивен нормален вид следва, че за всяка безкванторна формула φ може да се намери крайно множество Δ от дизюнкти, което я представя в следния смисъл: формулата φ е вярна в дадена структура S при дадена оценка v на променливите точно тогава, когато всеки дизюнкт от Δ е верен в S при оценката v (следователно φ е тъждествено вярна в дадена структура S точно тогава, когато S е модел за Δ). При това множеството Δ може да се избере така, че променливите на всеки дизюнкт от Δ да бъдат измежду променливите на формулата φ. За да намерим такова множество Δ, достатъчно е да намерим краен брой елементарни дизюнкции, на които конюнкцията е еквивалентна на φ и има същото множество на променливите, след което да образуваме множеството на дизюнктите, съответни на тези елементарни дизюнкции.

    Пример 1. Нека a и p са съответно константа и двуместен предикатен символ на сигнатурата Σ, а φ е формулата

    Въпросите, разгледани в предходните текстове, позволяват за всяко множество от формули Γ да се намери такова множество от дизюнкти Δ (които в общия случай са при някое разширение на първоначалната сигнатура), че съществуването на модел за Γ да бъде равносилно със съществуването на модел за Δ. Намирането на такова Δ може да стане, като най-напред всяка от формулите от Γ заменим с еквивалентна на нея пренексна формула, след това скулемизираме универсалните затваряния на така получените формули, използвайки за различните измежду тях различни скулемови функционални символи, представяме безкванторните части на получените скулемови нормални форми чрез крайни множества от дизюнкти и накрая образуваме обединението на тези множества.

    Пример 2. Нека p е двуместен предикатен символ на сигнатурата Σ, а функционални символи в нея да няма. Нека Γ е множеството от двете формули

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

    Нека са дадени два дизюнкта δ₁ и δ₂. Един дизюнкт δ ще наричаме тяхна непосредствена резолвента, ако съществуват литерал λ₁ от δ₁ и литерал λ₂ от δ₂, такива, че λ₁ и λ₂ са противоположни и е в сила равенството

    Пример 3. Всеки от двата тавтологични дизюнкта  {¬p(x,x), p(x,x)}  и  {¬p(a,x), p(a,x)}  е непосредствена резолвента на двата дизюнкта от пример 1.

    Пример 4. При всеки избор на атомарна формула φ празният дизюнкт е непосредствена резолвента на дизюнктитте {φ} и {¬φ}.

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

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

    Разбира се, ако се случи (както е в пример 3) един тавтологичен дизюнкт да бъде непосредствена резолвента на два дизюнкта, той ще бъде верен във всяка структура при всяка оценка на променливите без да е нужно да предполагаме нищо за въпросните два дизюнкта. Образуването на тавтологични непосредствени резолвенти всъщност се оказва излишно при прилагането на метода на резолюцията. От друга страна, случва се (както е да речем в примерите 1 и 2) разглежданите дизюнкти да нямат непосредствени резолвенти освен евентуално тавтологични. Затова ще разгледаме по-общ вид резолвента от непосредствената. За тази цел първо ще дефинираме какво ще разбираме под частен случай на даден дизюнкт.

    Нека е даден един дизюнкт δ. За всяка субституция σ дефинираме множество σδ чрез уславянето, че то се състои от формулите σλ, където λ принадлежи на δ. Очевидно σδ е пак един дизюнкт (с брой на елементите, ненадминаващ броя на елементите на δ). Ще го наричаме резултат от прилагането на σ към δ.

    Пример 5. Резултатите от прилагането на субституцията [x/a] към двата дизюнкта от пример 1 са съответно {¬p(a,a)} и {p(a,a)}.

    Лесно е да се убедим, че за произволен дизюнкт δ и произволна субституция σ дизюнктът σδ е верен в дадена структура S при дадена оценка v на променливите точно тогава, когато δ е верен в S при оценката σ^S(v). И наистина, ако дизюнктът δ не е празен, то той е съответен на някоя елементарна дизюнкция φ, а дизюнктът σδ е съответен на елементарната дизюнкция σφ, тъй че можем да се възползваме от аналогичното свойство на резултат от прилагане на субституция към формула. Ако пък δ е празният дизюнкт, то и σδ ще бъде празен, тъй че и двата ще бъдат неверни в S при всяка оценка на променливите.

    За един дизюнкт ще казваме, че е частен случай на даден дизюнкт δ, ако е резултат от прилагане към δ на някоя субституция. Отбелязаното преди малко условие за вярност на такъв резултат позволява да заключим, че ако един дизюнкт е тъждествено верен в дадена структура, то и всички частни случаи на този дизюнкт са тъждествено верни в нея,

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

    Пример 6. От пример 5 е ясно, че празният дизюнкт е резолвента на двата дизюнкта от пример 1. Очевидно обаче празният дизюнкт не е тяхна непосредствена резолвента.

    Забележка 1. Ако един дизюнкт е резолвента на два затворени дизюнкта, то той е тяхна непосредствена резолвента. Това е така, защото, както знаем, прилагането на субституция към затворена формула дава същата формула и поради това единственият частен случай на един затворен дизюнкт е той самият. Разбира се, дизюнкт, който е непосредствена резолвента на два затворени дизюнкта, също е затворен.

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

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

    Методът на резолюцията се основава именно на лема 2. Ще опишем накратко идеята на този метод, без да се впускаме в подробностите на неговото прилагане.

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

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

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

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

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

    Пример 7. Пример 6 показва, че празният дизюнкт е резолвентно изводим от множеството от двата дизюнкта в пример 1. Следователно не съществува модел за това множество. Значи не съществува и структура, в която да е тъждествено вярна формулата φ от споменатия пример.

    Пример 8. Нека Δ е множеството от четирите дизюнкта в пример 2. Прилагайки субституцията [x/a] към първия от тях и субституцията [y/f(a)] към третия, получаваме дизюнкти, които имат за непосредствена резолвента дизюнкта {p(f(a),a)}, следователно той е резолвентно изводим от Δ. От другите два от четирите дизюнкта чрез субституциите [x/a,z/a] и [y/f(a)] пък получаваме дизюнкти, на които е непосредствена резолвента дизюнктът {¬p(f(a),a)}, значи и той е резолвентно изводим от Δ. И така, намерихме два дизюнкта, резолвентно изводими от Δ, на които празният дизюнкт е непосредствена резолвента, следователно той също е резолвентно изводим от Δ. С това показахме, че не съществува модел за Δ, а значи не съществува модел и за множеството Γ от пример 2.

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

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