Для доказательства того, что формула G является логическим следствием множества формул F1,...,Fk метод резолюций применяется следующим образом. Сначала составляется множество формул {F1,...,Fk, ¬G}. Затем каждая из этих формул приводится к конъюнктивной нормальной форме (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F1,...,Fk. Если из S нельзя вывести #, то G не является логическим следствием формул F1,...,Fk.

Множество формул {F1,F2,...,Fk} называется выполнимым, если существует интерпретация j такая, что j(F1)=j(F2)=...=j(Fk)=1.
...
то, что формула X в интерпретации j истинна, можно записать в виде j(X)=1.
...
Интерпретацию будем обозначать в виде малой латинской буквы j, за которой в скобках указывается обозначение интерпретируемой формулы. Например, j(F1).
...
Чтобы судить об истинности формул, необходимо связать их с содержанием, т.е. выполнить интерпретацию формулы.
...
Интерпретацию можно рассматривать как некоторую функцию, отображающую множество формул на множество высказываний.
...
Т.е. если j(X v F)=1 и j(¬X v G)=1 для некоторой интерпретации j, то j(F v G)=1.

Правило резолюции. Из дизъюнктов (X v F) и (¬X v G) выводим дизъюнкт (F v G). Или другими словами, дизъюнкт (F v G) является логическим следствием дизъюнктов (X v F) и (¬X v G).