Дуальная структура обоснований, предложенная дойлом, может быть использована для разделения допущений на три группы.

(1) Посылки (premises), т.е. высказывания, которые полагаются истинными без всякого обоснования (по определению). Пользуясь обозначениями из теории множеств, можно следующим образом представить определение посылки:

{Р В | IN _p = OUT _p = не существует }.

(2) Дедукции (deductions), т.е. высказывания, которые являются заключениями нормальной монотонной дедукции. В обозначениях теории множеств дедукции представляются выражением

(2) Проверить консеквенсы данного узла. Если таковых не существует, то изменить статус узла с исключено на включено, сформировать связанные с ним списки IN и OUT и на этом закончить. В противном случае сформировать список L, в который включить узел и его множество последствий, зафиксировать статус включено-исключено каждого из этих узлов, временно присвоить им статус nil и перейти к шагу (3).

(3) Для каждого узла N из списка L попытаться отыскать действительное и убедительное обоснование, которое позволяет изменить статус этого узла на включено. Если таковое найдено не будет, присвоить узлу статус исключено. В любом варианте изменения статуса узла распространить это изменение на его консеквенсы. (Примечание. Обоснование является действительным, если каждый узел, перечисленный в его списке IN, имеет статус включено, а каждый узел, перечисленный в списке OUT, — статус исключено. Обоснование является убедительным в том случае, когда в его логической цепочке отсутствует зацикливание. Например, обоснования ({-Р},{}) и ({},{Р}) являются зацикленными по отношению к Р. Из первого следует, что Р имеет статус включено только в случае, если —P также имеет статус включено, а из второго следует, что Р имеет статус включено только в случае, если Р имеет статус исключено. Таким образом, каждое обоснование, если применить его в отношении высказывания Р, приводит к противоречию.)

(4) Если некоторый узел в списке L имеет состояние включено и отмечен как противоречивый, то запустить процедуру обратного прослеживания, ведомого зависимостями (dependency-directed backtracking). Если в процессе выполнения этой процедуры вновь возникнут условия для запуска процесса отслеживания истинности предположений (шаги (1)-(3)), повторять эти шаги до тех пор, пока не будут разрешены все противоречия.

(5) Сравнить текущий статус поддержки каждого узла из списка L с его прежним статусом, зафиксированным ранее, и известить пользователя обо всех произведенных изменениях статуса.

Обе системы — и Мак-Аллестера, и Доила — демонстрируют более "интеллектуальный" подход к решению проблемы адекватного и непротиворечивого описания мира, чем тот, который был использован в рассмотренной ранее системе STRIPS (см. главу 7). В обоих случаях системы отслеживания истинности предположений берут на себя заботы об обновлении модели мира посредством распространения аналогов операций ADD и DELETE по сети зависимостей. Если при этом обнаруживается, что в модели возникли противоречия, пользователю предлагается отказаться от какой-либо из посылок, которые послужили причиной такого противоречия, и восстановить тем самым целостность модели.

Пара конфликтующих выражений

Приведенная ниже программа на языке CLIPS реализует простой алгоритм отслеживания истинности предположений по отношению к простым атомарным выражениям. Литералы являются атомарными высказываниями, имеющими статус либо включено, либо исключено. Список inlist некоторого выражения включает те выражения, которые должны иметь статус включено для того, чтобы и данное выражение имело статус включено. Список outlist некоторого выражения включает те выражения, которые должны иметь статус исключено, для того, чтобы данное выражение имело статус включено. Как и ранее, пустые списки поддержки по умолчанию имеют значение -1.

;; ШАБЛОНЫ

;; Литерал - атомарное высказывание.

(deftemplate literal (field id (type INTEGER})

(field atom (type SYMBOL))

(field status (type SYMBOL) (default unk))

(multifield inlist (type INTEGER) (default -1))

(multifield outlist (type INTEGER) (default -1))

)

;; Исходная модель мира.

(deffacts model

(literal (id 0) (atom P) (status in) (outlist 1))

(literal (id 1) (atom Q) (status in) (outlist 0))

)

;; ПРАВИЛА

;; Если выражение в списке outlist

;; выражения S имеет статус out

;; и выражение S имеет пустой список inlist,

;; то присвоить выражению S статус in.

(defrule in

(literal (id?A) (status out))?F <-

(literal (status out) (inlist -1) (outlist?A))

=> (modify?F (status in))

)

Если выражение в списке outlist выражения S имеет статус in, то присвоить выражению S статус out. Обратите внимание на то, что в этом правиле наличие списка inlist для выражения S не имеет значения,

(defrule out

(literal (id?A) (status in))?F <-

(literal (status in) (outlist?A)) =>

(modify?F (status out)))

;; Это правило предлагает пользователю удалить

;; выражение и таким образом уладить конфликт,

(defrule deny

(declare (salience -10))

?L <- (literal (atom?X) (status in) (inlist -1)) =>

(printout t crlf "Deny "?X "? ")

(bind?ans (read)) (if (eq Pans yes)

Then (modify PL (status out)))

;; Что произойдет после того, как вы

;;запустите эту программу на выполнение?

;;Как! будет вести себя программа, если

;;в ответ на запрос, сформированный правилом

;; deny, ввести yes? Как будет

;;вести себя программа, получив ответ по?