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

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

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

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

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

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