За да опишем стъпките, чрез които се осъществява методът, първо ще се условим да наричаме допустима замяна на едно множество Γ от безкванторни формули, съответна на дадена формула θ от него, такава замяна на Γ с 0, 1 или 2 множества от безкванторни формули, че да бъде изпълнено някое от условията:
      а)  формулата ¬θ също принадлежи на множеството Γ и то се заменя с 0 на брой множества;
      б)  Γ се заменя с множеството (Γ\{θ})∪{θ'}, където θ' е формула, за която θ е ¬¬θ', или пък за някои формули φ и ψ имаме, че θ е ¬(φ&ψ), а θ' е ¬φ∨¬ψ, или че θ е ¬(φ∨ψ), а θ' е ¬φ&¬ψ;
      в)  Γ се заменя с множеството (Γ\{θ})∪{φ,ψ}, където φ и ψ са такива формули, че θ е φ&ψ;
      г)  Γ се заменя с двете (евентуално съвпадащи) множества (Γ\{θ})∪{φ} и (Γ\{θ})∪{ψ}, където φ и ψ са такива формули, че θ е φ∨ψ.

    Лесно се забелязва, че при допустима замяна на едно множество Γ от безкванторни формули, съответна на дадена негова формула, тази формула не принадлежи на никое от заменящите множества, но те (в случай, че броят им е ненулев) също се състоят от безкванторни формули и не са празни, а ако Γ е крайно, те също са крайни. Може да се случи в Γ да съществува повече от една формула, за която има съответна на нея допустима замяна на Γ, а би могло също за някоя формула от Γ да има повече от една допустима замяна на Γ, съответна на нея (това положение ще бъде налице, когато формулата не е литерал, а отрицанието й също принадлежи на Γ). Допустими замени на едно множество от безкванторни формули ще наричаме всички допустими негови замени, съответни на формули от него. Веднага се вижда, че при коя да е допустима замяна на едно множество Γ от безкванторни формули конфигурациите, удовлетворяващи Γ, са точно онези, които удовлетворяват поне едно от множествата, заменящи Γ. Ясно е също, че за едно множество от безкванторни формули не съществува допустима замяна тогава и само тогава, когато всички формули от множеството са литерали и никой от тях не е отрицание на атомарна формула, принадлежаща на множеството. Такова множество ще наричаме просто.

    Приемаме, че споменатият по-горе итеративен процес завършва, когато стигнем до множество от прости множества. Когато пък {Γ₁,…,Γ_n} е крайно множество, чиито елементи са непразни крайни множества от безкванторни формули, и поне едно от тези множества не е просто, разрешена стъпка на итеративния процес за това множество е заменянето в него на всяко множество Γ_i, което не е просто, с множествата, получени при някоя допустима замяна на това Γ_i (ако някои множества Γ_i са прости, те се запазват без изменение). От казаното в предходния абзац следва, че след извършването на такава стъпка получаваме пак крайно множество, чиито елементи са непразни крайни множества от безкванторни формули. При това една конфигурация ще удовлетворява някое от тези множества точно тогава, когато тя удовлетворява някое от множествата Γ₁, …, Γ_n. Това доказва коректността на описания метод за привеждане на безкванторна формула в дизюнктивен нормален вид – в смисъл, че всеки резултат, получен по този метод, наистина е формула в дизюнктивен нормален вид, еквивалентна на онази, към която сме приложили метода.

    Пример 1. Нека θ е формулата α↔β, където α и β са две различни атомарни формули. Като вземем пред вид дефинициите за еквиваленция и импликация, виждаме, че описаният по-горе итеративен процес ще трябва да започне с множеството, имащо за единствен елемент едноелементното множество

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

    За произволно крайно множество Γ от безкванторни формули да наречем сложност на Γ споменатия по-горе сбор, т.е. сбора от сложностите на формулите от Γ, които не са литерали. Разбира се, ако Γ е просто множество (т.е. всички формули от Γ са литерали), за този сбор ще приемем, че е равен на 0, а очевидно във всички останали случаи той е положително цяло число. Ако Γ₁, …, Γ_n, където n е положително, са крайни множества от безкванторни формули, то най-голямата измежду сложностите на тези множества ще наричаме височина на множеството {Γ₁,…,Γ_n}. Допълнително се уславяме, че височината на празното множество е 0. Ясно е, че когато поне едно от множествата Γ₁, …, Γ_n не е просто, височината на множеството {Γ₁,…,Γ_n} е положителна, и не е трудно да се съобрази, че при извършване на разрешена стъпка на итеративния процес тази височина ще намалее (това е така, защото при такава стъпка всяко от множествата с положителна сложност измежду Γ₁, …, Γ_n се заменя с множества, имащи по-малка сложност, а останалите Γ_i се запазват без промяна). Това обстоятелство показва, че итеративният процес непременно ще завърши след краен брой стъпки, ненадминаващ височината на множеството в началото на процеса (тази височина всъщност е равна на сложността на формулата, към която прилагаме метода).

    Забележка 1. С леко усложняване на разсъжденията може да се покаже, че коректността на метода и завършването на итеративния процес се запазват и при разрешаване още на стъпки, изразяващи се в премахване на такова измежду множествата Γ₁, …, Γ_n, на което някое същинско подмножество е също измежду тях.

    Забележка 2. Когато прилагаме описания метод към дадена безкванторна формула θ, формулите в множествата, появяващи се в хода на итеративния процес, имат само такива атомарни компоненти, които са атомарни компоненти на θ. Благодарение на това може да се твърди, че всяка безкванторна формула е еквивалентна на някоя формула в дизюнктивен нормален вид, на която атомарните компоненти са измежду атомарните компоненти на дадената формула (така е дори и в случаите, когато итеративният процес завършва с празно множество – тогава дадената формула е еквивалентна на конюнкция от своя атомарна компонента и нейното отрицание). В случаите, когато итеративният процес завършва с непразно множество от прости множества (а това със сигурност става, ако формулата θ е изпълнима), в никоя от елементарните конюнкции, от които е съставена получената формула в дизюнктивен нормален вид, не ще участват едновременно атомарна формула и нейното отрицание.

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

    Пример 2. Да разгледаме формулата (α&β)∨(β&γ)∨(γ&α), където α, β и γ са три различни атомарни формули. Като вземем пред вид дефиницията за тричленна дизюнкция, виждаме, че за привеждане на тази формула в конюнктивен нормален вид трябва да започнем итеративния процес с множеството, имащо за единствен елемент едноелементното множество