Пример 1. Нека Γ се състои от четирите дизюнкта {A,B}, {¬A,B}, {A,¬B} и {¬A,¬B}, където A и B са две различни затворени атомарни формули. Тогава има точно 11 затворени дизюнкта, изводими от Γ, а именно четирите дизюнкта, съставящи Γ, и още дизюнктите {B}, {A}, {B,¬B}, {¬A,A}, {¬A}, {¬B}, ∅ (разбира се изводимостта на празния дизюнкт позволява да заключим, че множеството Γ не е изпълнимо).

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

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

    За един затворен дизюнкт D ще казваме, че той е почти изводим от дадено множество Γ от затворени дизюнкти, ако D съдържа като подмножество някой дизюнкт, изводим от Γ, или сред елементите на D има два взаимно противоположни литерала. Очевидно всеки такъв дизюнкт следва от Γ. Оказва се обаче, че е вярно и обратното. В лема 3 по-долу ще докажем въпросното обратно твърдение при предположение, че множеството Γ е крайно, но с помощта на теоремата за компактност бихме могли лесно да се освободим от това предположение.

    Лема 1. Ако един затворен дизюнкт D е почти изводим от дадено множество Γ от затворени дизюнкти, то всеки затворен дизюнкт, който съдържа D, също е почти изводим от Γ.

    Доказателство. Твърдението следва директно от дефиницията за почти изводимост.  _□

    Лема 2. Нека Γ е множество от затворени дизюнкти, D₁ и D₂ са затворени дизюнкти, почти изводими от Γ, и D е непосредствена резолвента на D₁ и D₂. Тогава дизюнктът D също е почти изводими от Γ.

    Доказателство. Всеки един от двата дизюнкта D₁ и D₂ съдържа като подмножество някой дизюнкт, изводим от Γ, или съдържа сред елементите си два взаимно противоположни литерала. Освен това D е обединение на D₁\{L₁} и D₂\{L₂}), където L₁ и L₂ са противоположни литерали, принадлежащи съответно на D₁ и на D₂. Да разгледаме най-напред случая, когато съществуват изводими от Γ затворени дизюнкти D₁ и D₂, съдържащи се съответно в D₁ и в D₂. Ако L₁ принадлежи на D₁ и L₂ принадлежи на D₂, то обединението на D₁\{L₁} и D₂\{L₂} е дизюнкт, който е изводим от Γ и се съдържа в D. Ако L₁ не принадлежи на D₁, то изводимият от Γ дизюнкт D₁ се съдържа в D₁\{L₁}, а следователно и в D. Аналогично се вижда, че ако L₂ не принадлежи на D₂, то D₂ се съдържа в D. И така, във всички подслучаи на разглеждания дотук случай се оказва, че D съдържа като подмножество някой дизюнкт, изводим от Γ, и следователно D е почти изводим от Γ. Да предположим сега, че в D₁ има два взаимно противоположни литерала. Ако те и двата са различни от L₁, то те принадлежат на D₁\{L₁}, а значи и на D, тъй че сред елементите на D има два взаимно противоположни литерала и значи D е почти изводим от Γ. Ако пък единият от въпросните два взаимно противоположни литерала е L₁, то другият е L₂, поради което L₂ принадлежи на D₁\{L₁} и значи всички елементи на почти изводимия от Γ дизюнкт D₂ принадлежат на D, тъй че D е почти изводим от Γ съгласно лема 1. Аналогично се разглежда и случаят, когато в D₂ има два взаимно противоположни литерала.  _□

    Лема 3. Нека Γ е крайно множество от затворени дизюнкти. Тогава всеки затворен дизюнкт, който следва от Γ, е почти изводим от Γ.

    Доказателство. Ще си послужим с индукция относно броя на дизюнктите в Γ. Ако този брой е 0, то затворените дизюнкти, които следват от Γ, са верни във всяка структура. Лесно се вижда обаче, че когато един затворен дизюнкт е верен във всяка структура, сред елементите на този дизюнкт има непременно два взаимно противоположни литерала и значи дизюнктът е почти изводим от Γ. И наистина, ако никои два литерала, принадлежащи на даден затворен дизюнкт D не са взаимно противоположни, то същото важи и за литералите, противоположни на тези от D, и поради това (по критерия за изпълнимост на множество от затворени литерали) съществува структура, в която литералите, противоположни на тези от D, са верни и следователно литералите от D са неверни, т.е. съществува структура, в която D не е верен. Да предположим сега, че заключението на лемата е вярно за дадено крайно множество Γ от затворени дизюнкти, и да разгледаме множество Γ′, получено от Γ чрез добавяне на още един затворен дизюнкт D′. Нека D е произволен затворен дизюнкт, който следва от Γ′. За произволен литерал L да се условим да означаваме неговия противоположен с −L. Лесно се съобразява, че за всеки литерал L, принадлежащ на D′, дизюнктът {−L}∪D следва от множеството Γ, поради което е почти изводим от Γ, а значи и от Γ′. Оттук се вижда, че ако за някой литерал от D′ неговият противоположен принадлежи на D, то дизюнктът D е почти изводим от Γ′ (даже и от Γ). Оттук нататък ще предполагаме, че D не съдържа противоположния литерал на никой литерал от D′. Ако D съдържа  D′, то разбира се D е почти изводим от Γ′ (защото D′ е изводим от Γ′). Ще се занимаем сега със случая, когато D не съдържа  D′. Нека разликата  D′\D има k елемента L₁, …, L_k. Да разгледаме (k+1)-членната редица от дизюнкти

    Следствие. Ако едно множество от затворени дизюнкти е неизпълнимо, то празният дизюнкт е изводим от това множество.

    Доказателство. Нека е дадено едно неизпълнимо множество от затворени дизюнкти. По теоремата за компактност някое крайно подмножество Γ на това множество също е неизпълнимо. Според току-що доказаната лема празният дизюнкт е почти изводим от Γ, но това е възможно само в случай че той е изводим от Γ, а значи и от първоначално даденото множество от дизюнкти.  _□

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

    Модел за едно множество от дизюнкти се нарича такава структура, в която всички дизюнкти от множеството са тъждествено верни.

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

    Доказателство. Нека Γ е множество от дизюнкти, за което не съществува модел. На първо време ще предположим, че в сигнатурата, с която работим, има поне една константа. Да означим с Γ^o множеството на всички затворени частни случаи на дизюнктите от Γ. Множеството Γ^o е неизпълнимо и значи по доказаното по-горе следствие празният дизюнкт е изводим от Γ^o. Оттук получаваме, че той е изводим и от множеството Γ. За целта можем да използваме лесно доказуемото твърдение, че всеки дизюнкт, изводим от Γ^o, е частен случай на дизюнкт от Γ или е изводим от Γ (използваме още, че празният дизюнкт не е частен случай на никой друг дизюнкт). Ако пък се случи сигнатурата да е без константи, можем да я разширим чрез добавяне на някоя константа α. Множеството Γ няма да притежава модел и при работа с така разширената сигнатура, следователно при работа с нея празният дизюнкт ще бъде изводим от множеството Γ^o на затворените частни случаи на дизюнктите от Γ. Да си изберем някоя променлива ξ. Доказва се, че субституцията [ξ/α] установява взаимно еднозначно съответствие между множеството на всички дизюнкти в първоначалната сигнатура, които нямат променливи, различни от ξ, и множеството на всички затворени дизюнкти в разширената. Доказва се още, че при въпросното съответствие първообразът на всеки затворен дизюнкт, изводим от Γ^o, е частен случай на дизюнкт от Γ или е изводим от Γ при работа с първоначалната сигнатура. Накрая това се прилага към първообраза на празния дизюнкт.  _□

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

    Пример 2. Нека, работейки в сигнатура с константа a, едноместен функционален символ f и двуместен предикатен символ p, искаме да изследваме дали има модел множеството Γ, което се състои от двата едноелементни дизюнкта {p(f(X),Y)} и {¬p(Z,f(Z))}. Ако следваме изложените по-горе доказателства, би трябвало да търсим затворени термове X, Y и Z, за които частните случаи {p(f(X),Y)} и {¬p(Z,f(Z))} на двата дизюнкта имат непосредствена резолвента, т.е. затворени термове X, Y и Z, за които са в сила равенствата f(X)=Z и Y=f(Z) (ако намерим такива термове, това ще докаже несъществуването на модел за Γ, тъй като в качеството на резолвента ще се получи празният дизюнкт). Тъй като обаче при тази сигнатура съществуват безбройно много затворени термове, едва ли можем да извлечем някаква изгода от възможността да се ограничим при търсенето само със затворените термове. Всъщност достатъчно е да търсим какви да е термове X, Y и Z, за които са изпълнени горните равенства. Очевидно системата от тези две равенства е равносилна със системата

    Пример 3. Да усложним малко предходния пример, като в описанието на Γ заменим втория от двата дизюнкта с {¬p(Z,f(U)), ¬p(U,f(Z))}. Тогава бихме могли да работим както в предния пример, ако при образуването на резолвента използваме за втория дизюнкт частен случай на неговия частен случай, получен чрез субституцията [U/Z] (той всъщност е вторият дизюнкт от пример 2). При прилагане на метода на унификацията се достига до субституцията [U/Z] чрез опит да се извърши в посочения по-горе втори дизюнкт на сегашното Γ тъй нареченото слепване - т.е. да се намери на дизюнкта частен случай с по-малък брой елементи. Този опит води до търсене на термове Z и U, удовлетворяващи условията Z=U и f(U)=f(Z), а очевидно системата от тези две условия е равносилна с условието U=Z.

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

    Пример 4. Нека в описанието на множеството Γ от пример 1 да заменим първия дизюнкт с неговия частен случай {p(f(X),X)}. След това изменение вече в Γ няма дизюнкти, които да притежават резолвента, защото ако би имало, то за някои термове X, Y и Z биха били в сила равенствата f(X)=Z и X=f(Z), а от тях следва невъзможното равенство X=f(f(X)) (то е невъзможно, защото при всеки избор на терм X дясната страна на равенството има по-голяма дължина от лявата). При това положение е ясно, че празният дизюнкт не е изводим от Γ, и теоремата за пълнота на резолюцията позволява да твърдим, че Γ има модел.