Алгоритм абдуктивного вывода, использующий ATMS

Существуют различные методы решения задачи абдукции. Мы рассматриваем метод решения задачи абдукции с помощью ATMS. Назовем алгоритм абдуктивного вывода, использующий ATMS, как AAA (ATMS-based Abduction Algorithm) [Hwee Tou Ng et al., 1991]. Достоинством алгоритма AAA является тот факт, что вся выводимая информация сохраняется в дереве вывода, и для вывода новых вершин не нужно тратить время на конструирование дизъюнктов. На вход алгоритма поступает исходное множество дизъюнктов и наблюдаемое событие, которое необходимо объяснить. На выходе получается множество абдуктивных объяснений этого события. Сначала создается вершина GOAL (операция создания вершины ATMS), а наблюдаемое событие добавляется в ATMS как обоснование GOAL (операция добавления обоснования в ATMS). Процедура Assume добавляет для вершины, помеченной некоторой литерой, вершину-предположение, содержащую эту же литеру (операция добавления предположения в ATMS). Таким образом, реализуется допущение об истинности литеры для вершины. Далее, начиная с GOAL, в ход вступают процедуры ProcessNode и ProcessJustification, рекурсивно вызывающие друг друга. В процедуре ProcessNode для каждого обоснования текущего узла запускается механизм ProcessJustification. В процедуре ProcessJustification происходит собственно добавление новых вершин в ATMS: для каждой вершины n текущего обоснования, помеченной литерой N, ищется дизъюнкт, и к вершине n добавляется обоснование, где — это вершины, помеченные литерами соответственно (операция добавления обоснования в ATMS). Если в процессе унификации аргументы текущего обоснования изменяются, то обоснование копируется, и унификация и добавление новых узлов происходят с копией обоснования. Это необходимо для того, чтобы не потерять текущее обоснование как часть решения. После того, как дерево построено, вычисляется метка на узле GOAL, которая представляет собой множество минимальных абдуктивных объяснений.

В алгоритме AAA используется понятие фактора дизъюнкта. Если две или более одинаковые литеры одного и того же знака дизъюнкта C имеют НОУ, то дизъюнкт C называется фактором дизъюнкта C [Вагин и др., 2008].

Алгоритм AAA.

Исходные данные:

clauses — исходное множество дизъюнктов,.

observed — наблюдаемый конъюнкт.

Выходные данные:

result — множество абдуктивных объяснений для observed (результирующее множество конъюнктов).

Начало.

Шаг 1.

Если все дизъюнкты из clauses — хорновские дизъюнкты, то переход к шагу 2. Иначе ОШИБКА, Сообщение «Все дизъюнкты должны быть хорновскими!», Конец.

Шаг 2.

Вычислить множество, где — множество всевозможных факторов дизъюнктов из clauses.

Шаг 3.

Пусть O₁, O₂… — это литеры observed. Создать вершину GOAL (операция добавления вершины в ATMS) и добавить к ней обоснование. nO₁, nO₂… — добавленные таким образом новые вершины (операция добавления обоснования в ATMS).

Шаг 4.

Выполнить процедуру Assume с параметрами nO_i, O_i для i=1,2. (операция добавления предположения в ATMS).

Шаг 5.

Выполнить процедуру ProcessNode с параметрами GOAL, extendedClauses, GOAL, .

Шаг 6.

Вычислить метку на вершине GOAL. Найденная метка содержит результирующее множество конъюнктов. Запишем его в result.

Конец.

Процедура Assume.

Исходные данные:

node — вершина,.

litera — литера, по которой делается предположение.

Требуется:

создать предположение для текущей вершины.

Начало.

Шаг 1.

Создать вершину-предположение nLitera с литерой litera и добавить обоснование (операция добавления предположения в ATMS).

Конец.

Процедура ProcessNode.

Исходные данные:

node — текущая вершина,.

clauses — множество дизъюнктов,.

mainNode — целевая вершина,.

unassumed — список литер, к вершинам которых запрещено добавлять обоснование-предположение.

Требуется:

добавить новые вершины через механизм обратной дедукции.

Начало.

Шаг 1.

Обозначим — номер обоснования; justificationCount — число обоснований.

Шаг 2.

Если, то Конец. Иначе рассмотрим justification — i-е обоснование вершины node. Вызвать процедуру ProcessJustification с параметрами justification, clauses, mainNode, unassumed.

Шаг 3.

Присваиваем и переход к шагу 2.

Конец.

Процедура ProcessJustification.

Исходные данные:

justification — текущее обоснование,.

clauses — множество дизъюнктов,.

mainNode — целевая вершина,.

unassumed — список литер, к вершинам которых запрещено добавлять обоснование-предположение.

Требуется:

добавить новые вершины через механизм обратной дедукции.

Начало.

Шаг 1.

Пусть nodeCount — число вершин в justification; - номер вершины в justification.

Шаг 2.

Если, то Конец. Иначе рассмотрим node — i-я вершина в justification.

Шаг 3.

Найти список пар дизъюнкт-подстановка вида, в которых литера из clause унифицируется с литерой на вершине node. Обозначим этот список пар как substitutions, количество элементов в substitutions — как substitutionCount; - номер текущего элемента в substitutions.

Шаг 4.

Если, то и переход к шагу 2. Иначе рассмотрим пару дизъюнкт-подстановку substitution — substNumber-й элемент в substitutions. Пусть substitution представляет пару clause — дизъюнкт и subst — подстановка.

Шаг 5.

Определить, меняет ли литера хотя бы на одном узле ветви от mainNode до justification свои аргументы при подстановке subst. Если есть такой узел, то переход к шагу 6. Иначе переход к шагу 7.

Шаг 6.

«Устранение многозначности». Пусть lastStableNode — это последний узел текущей ветви C, начиная от вершины mainNode, литера на котором не меняет свои аргументы при подстановке subst. Пусть notStableJustification — обоснование вершины lastStableNode, причем одна или несколько литер вершин notStableJustification меняют свои аргументы при подстановке subst. Тогда stableJustification — скопированное обоснование notStableJustification, к которому применена подстановка subst и которое добавлено в дерево вывода как обоснование lastStableNode (операции создания вершины и добавления обоснования в ATMS). Определим newUnassumed — последовательность литер, которыми помечены вершины начиная от lastStableNode и заканчивая node; причём ко всем литерам этой последовательности применена подстановка subst. Вызвать процедуру ProcessJustification с параметрами stableJustification, clauses, mainNode, newUnassumed. Переход к шагу 8.

Шаг 7.

Резолюция по node с дизъюнктом clause с добавлением нового обоснования newJustification к node. … — узлы обоснования newJustification, … — литеры, соответствующие этим узлам (операции создания вершины и добавления обоснования в ATMS). Пусть firstUnassumedLitera — первая литера в unassumed. Среди литер … найти firstUnassumedLitera. Пусть это. Если литера не найдена, то unassumedNumber = -1. Выполнить процедуру Assume с параметрами, , (операция добавления предположения в ATMS). Если unassumedNumber -1, то удалить из unassumed первую литеру. Выполнить процедуру ProcessNode с параметрами node, clauses, mainNode, unassumed.

Шаг 8.

Присвоить и переход к шагу 4.

Конец.