Резолюция әдісі Бұл G формуласының логикалық нәтижесі F1,F2,...,Fk формуласы болатынын дәлелдеу әдісіне берілген. Бұл әдіс Резолюция әдісі деп аталады. Логикалық құралдар туралы есеп есептің орындалуына әкеледі. Расындада, G формуласының логикалық құралы F1,F2,...,Fk формуласы болады және {F1,F2,...,Fk, G}жиын формуласы орындалмайды. Резолюция әдісі нақты айтқанда орындалмауын көрсетеді. Бұл әдістің бірінші ерекшелігі. Екінші ерекшелігіол туынды формуланы көрсетпей, дизъюнктарды (немесе элементар дизъюнкцияны) көрсетеді.
Логикалық құралдар.Литерал деп атомарлы формуланы немесе оның терісін, дизъюнкт – литералдар дизъюнкциясы айтылады. Дизъюнкт бір литералдан тұруы мүмкін. Дизъюнктті біз литералдар жиыны деп алсақ болады немесе дизъюнктті айырмасақ та болады, себебі, коммутативті және ассоциативті дизъюнкциядан бір-бірінің көмегімен шығады, және де идемпотенттілік шығады. Мысалы X YX и X Y дизъюнкттері тең. Бізге ерекше бос (ішінде литералы жоқ) дизъюнкт керек. Оны "квадратпен" белгілейміз □. Бос дизъюнкт кез келген интерпретацияда жалған деп есептейміз. Бұдан F&□ формуласы □ тең , ал F□ формуласы F-ке тең. Бос дизъюнкт те тура солай, себебі атомарлы формула 0, контекстті резолюция әдісінде □-ті қолдану керек. .
Анықтама. L және L литералы қарама-қарсы деп аталады.
Логикалық құралдарда резолюция әдісі резолюция ережесіне негізделген.
Анықтама. Резолюция ережесі логикалық құралдардан келесі ереже шығады: резолюция ережесінен ХF и XGдизъюнктінен FGдизъюнкті шығады.
Мысалы, XYZ и X Y дизъюнкттерден YZ Y дизъюнкттері шығады. Назар аударар болсақ, бірінші екі дизъюнкттерде тағы бір жұп қарама-қарсы литералдар шығады. Резолюция ережесі тек сол литералдарда қолданады деген тұжырым алсақ. Онда Y және Y-ке қолданылған резолюция ережесінен XZX шығады. Условимся еще о следующем: в дизъюнктке қайталанатын литералдарды және □ жазбасақ, онда басқа литералдар бар болады.
