Анықтама. S – дизъюнкттар жиыны болсын. S-ң нәтижесі деп, дизъюнкттар тізімін айтады.
D1,D2,...,Dn дегеніміз S-ға қатысты әрбір дизъюнкт тізімі немесе бұдан резолюцияның соңғы ережесі шығады. D дизъюнкті S-ң нәтижесі, егер S-ң соңғы дизъюнкті D болса.
Мысалы, егер S={ XYZ, YU, X}, онда D1= XYZ, D2= YU, D3= XZU, D4=X, D5=ZU – S-дан шыққан нәтижесі. ZU дизъюнкті S-дан шығады.
Резолюция әдісін қолдану келесі тұжырымнан шығады және ол толық резолюция әдісінің теоремасыдеп аталады.
Теорема1.Логикалық құралдар дизъюнкттар S жиыны орындалмайды сонда тек сонда ғана S – дан бос дизъюнкт шықса.
Дәлелдеу үшін, G формуласы логикалық жиыны F1,…,Fkформуласына резолюция әдісі келесі түрде қолданылады. Алдымен T={F1,…,Fk, G} формулалар жиыны құрылады. Одан кейін бұл формулалардың әр қайсысы КНФ-ке келтіріледі және шыққан формулалардан конъюнкция сызылады. S дизъюнкттар жиыны шығады. Және , нәтижесінде S-дан бос дизъюнктті іздейді. Егер S-дан бос дизъюнкт алсақ, онда G формуласы үшін F1,…,Fk логикалық формула болады. Егер S-дан алынбаса, онда G формуласы F1,…,Fk логикалық формуласы шықпайды.
Бұл мысалды кері алсақ, G=Z формула. G=Z формуласы логикалық болады, нәтижесінде F1= X Y X&Z, F2= Y Z. T={F1,F2, G}жиындар формуласы. F1 және F2 формуласын КНФ-қа келтіреміз ( G формуласында осы форма болады). Нәтижесінде
F1 эквивалентті X&( YZ),
F2 эквивалентті (YZ).
Онда S дизъюнкттар жиыны тең:
{X, YZ, YZ, Z}.
S жиынынан бос дизъюнкт оңай алынады:
YZ, Z, Y, YZ, У, □.
