Полнота резолюции

Чтобы завершить обсуждение правила резолюции в этом разделе, покажем, почему алгоритм PL-Resolution является полным. Для этого целесообразно ввести понятие резолюционного замыкания RC(S) множества выражений, представляющего собой множество всех выражений, которые могут быть получены путем повторного применения правила резолюции к выражениям из множества S или к их производным.

Резолюционным замыканием является множество выражений, которое вычисляется алгоритмом PL-Resolution в качестве окончательного значения переменной clauses. Можно легко показать, что множество RC(S) должно быть конечным, поскольку количество различных выражений, которые могут быть сформированы из символов P1, …Pk, присутствующих в S, является конечным. (Следует отметить, что это утверждение не было бы истинным, если бы не применялся этап факторизации, в котором уничтожаются дополнительные копии литералов.) Поэтому алгоритм PL-Resolution всегда оканчивает свою работу.

Блок-схема

Часть блок-схемы, показывающей процесс применения функции PL-Resolution для формирования простого логического вывода в мире вампуса. Здесь показано, что из первых четырех выражений, приведенных в верхнем ряду, следует выражение ¬P1,2

Теорема полноты для правила резолюции в пропозициональной логике называется основной теоремой резолюции. Если множество выражений является невыполнимым, то резолюционное замыкание этих выражений содержит пустое выражение. Докажем эту теорему, показав, что справедливо противоположное ей утверждение: если замыкание RC(S) не содержит пустое выражение, то множество S выполнимо. В действительности для множества S можно создать модель с подходящими истинностными значениями для P1,…,Pk. Процедура создания такой модели описана ниже. Для i от 1 до k:

  • если в множестве RC(S) имеется выражение, содержащее литерал ¬Pi, такое, что все другие его литералы являются ложными при данном присваивании, выбранном для P1,…Pi-1, то присвоить литералу Pi значение false; в противном случае присвоить литералу Pi значение true.
  • Остается показать, что это присваивание значений литералам Рг,..., Рк 
представляет собой модель множества выражений 5, при условии, что множество RC(S) является замкнутым согласно правилу резолюции и не содержит пустого выражения. Доказательство этого утверждения оставляем читателю в качестве упражнения.