Главная arrow Знания и рассуждения arrow Полнота резолюции
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

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

Чтобы завершить обсуждение правила резолюции в этом разделе, покажем, почему алгоритм 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) является замкнутым согласно правилу резолюции и не содержит пустого выражения. Доказательство этого утверждения оставляем читателю в качестве упражнения.