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

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

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

Теорема полноты для правила резолюции в пропозициональной логике называется основной теоремой резолюции.

Если множество выражений является невыполнимым, то резолюционное замыкание этих выражений содержит пустое выражение.

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

•    если в множестве RC(S) имеется выражение, содержащее литералтакое, что все другие его литералы являются ложными при данном присваивании, выбранном для

то присвоить литералу Pi значение false;

•    в противном случае присвоить литералу Pi значение true.

Остается показать, что это присваивание значений литералампредставляет собой модель множества выражений S, при условии, что множество RC{S) является замкнутым согласно правилу резолюции и не содержит пустого выражения. Доказательство этого утверждения оставляем читателю в качестве упражнения.