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

 
Алгоритм резолюции Печать

Процедуры логического вывода, основанные на правиле резолюции, действуют с использованием принципа доказательства путем установления противоречия, который описывался в конце раздела. Таким образом, чтобы показать, что KB ≠ α, мы покажем, что высказывание (KB ^ ¬α) является невыполнимым. Это можно сделать, доказав, что имеет место противоречие.

Алгоритм резолюции приведен в листинге. Вначале высказывание (KB ^ ¬α) преобразуется в форму CNF.

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

  • перестают вырабатываться какие-либо новые выражения, которые могли быть добавлены к существующим, и в этом случае из базы знаний KB не следует высказывание α;
  • два противоположных друг другу выражения устраняются, в результате чего создается пустое выражение; в этом случае из базы знаний KB следует высказывание α.

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

 

function PL-Resolution(KB, се) returns значение true или false

  inputs: KB, база знаний - высказывание в пропозициональной логике

  а, запрос - высказывание в пропозициональной логике

  clauses <— множество выражений, полученное после преобразования

  высказывания KB л —i(X в форму CNF

  new <— {}

  loop do

  for each d, Cj in clauses do

  resolvents <— PL-Resolve (Cl, Cj)

  if множество resolvents содержит пустое выражение

  then return true

  new <— new u resolvents

  if new с clauses then return false

  clauses <— clauses u new

 

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

Эту процедуру резолюции можно применить для формирования очень простого логического вывода в мире вампуса. Когда агент находится в квадрате [ 1,1 ], он не чувствует ветерка, поэтому в соседних квадратах не может быть ям. Соответствующая база знаний является следующей:

KB = R2 ^ R4 = (B1,1 <=> (P1,2 v P2,1)) ^ ¬B1,1

и требуется доказать высказывание α, которое, скажем, имеет вид ¬P1,2. После преобразования высказывания (KB ^ ¬α) в форму CNF получим выражения. В нижнем ряду на этом рисунке показаны все выражения, полученные путем устранения противоположных друг другу литералов из всех пар выражений, приведенных в верхнем ряду. Затем после устранения литерала P1,2, противоположного литералу ¬P1,2, будет получено пустое выражение, показанное в виде небольшого квадрата.

Анализ результатов, позволяет обнаружить, что многие этапы резолюции были бессмысленными. Например, выражение B1,1 v ¬B1,1 v P1,2 эквивалентно выражению True v P1,2, которое эквивалентно True. Логический вывод, согласно которому выражение True является истинным, не очень полезен. Поэтому любое выражение, в котором присутствуют два взаимно дополнительных литерала, может быть отброшено.