Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F₁,F₂,...,F_k, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F₁,F₂,...,F_k тогда и только тогда, когда множество формул {F₁,F₂,...,F_k,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).