Полнота и компактность метода

Правило резолюции обладает свойством полноты в том смысле, что с помощью него всегда можно вывести из пустой дизъюнкт #, если исходное множество дизъюнктов является противоречивым.

Отношение выводимости (из-за конечности вывода) является компактным: если , то существует такое конечное подмножество , что . Поэтому предварительно нужно доказать, что отношение невыполнимости является компактным.

Лемма. Если каждое конечное подмножество имеет выполняющую оценку, то имеется выполняющая оценка для всего множества дизъюнктов .

Доказательство. Предположим, что в встречаются дизъюнкты, использующие счетное множество пропозициональных переменных . Построим бесконечное двоичное дерево, где из каждой вершины на высоте выходят два ребра, помеченное литералами и соответственно. Удалим из этого дерева те вершины, литералы по пути в которые образуют оценку, противоречащую хотя бы одному дизъюнкту .

Для каждого рассмотрим конечное подмножество , состоящее из дизъюнктов, не содержащих переменных . По условию леммы найдется такая оценка переменных (или путь до вершины на уровне обрезанном дереве), что она выполняет все дизъюнкты из . Значит, обрезанное дерево бесконечно (то есть содержит бесконечное множество вершин). По лемме Д.Кёнига обрезанное дерево содержит бесконечную ветвь. Этой ветви соответствует оценка всех переменных , которая делает истинными все дизъюнкты из . Что и требовалось.