Процедура ProcessJustification.

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

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

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

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

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

Требуется:

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

Начало.

Шаг 1.

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

Шаг 2.

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

Шаг 3.

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

Шаг 4.

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

Шаг 5.

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

Шаг 6.

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

Конец.

НЕ нашли? Не то? Что вы ищете?

В четвёртой главе рассматривается применение абдуктивного вывода к задаче составления расписаний.

Составление расписаний – это область, в которой в последнее время абдуктивный вывод находит успешное применение. Классическая задача составления расписаний заключается в следующем. Пусть необходимо обслужить множество N = {1, 2, …, n} требований. Требование k, k Î {1,…, n} поступает на обслуживание в момент времени dk ³ 0 и для обслуживания требует tk > 0 единиц времени. Процесс обслуживания может быть описан заданием кусочно-постоянной, непрерывной слева функции S = S (t), принимающей при 0 < t < ∞ одно из значений 0, 1, 2,..., n. Если S (t) = k ¹ 0, то в момент времени t прибор обслуживает требование k; если S (t) = 0, то в момент времени t ни одно из требований не обслуживается. Эта функция называется расписанием и её требуется найти.

Рассматривается модификация задачи составления расписаний, известная как задача Job Shop Scheduling:

•  задано множество работ ;

•  задано множество машин ;

•  на множестве J определена функция , такая что , если работа j выполняется на машине m;

•  для каждой работы задано время её выполнения, определена функция , такая что , если выполнение работы j длится t единиц времени;

Расписание есть функция , которая для каждой работы j определяет начальное время S(j).

Длиной расписания S будем называть .

Требуется найти расписание S, такое что len(S) ® min. Так же, расписание должно удовлетворять определённым условиям, вытекающим из самой постановки задачи. Вывод по абдукции позволяет формализовать трудно формализуемые ограничения предметной области для задачи составления расписания.

Идея применения вывода по абдукции в решении задачи составления расписания состоит в следующем. Рассмотрим соотношение . Пусть Th – это логическая теория первого порядка, представляющая условия и ограничения предметной области, j – формула логики первого порядка, содержащая константы TS и TE. Пусть , где , что означает, что [TS, TE] – период выполнения работы j. Теперь пусть наблюдается . Здесь tS, tE – переменные. Задача состоит в нахождении объяснений для f1, в процессе получения которых переменные tS, tE означиваются.

Абдуктивный вывод позволяет строить различные расписания, которые далее могут быть обработаны методами оптимизации в целях нахождения расписания наименьшей длины.

Преимущество решения задачи составления расписания при помощи абдуктивного вывода по сравнению с комбинаторными аналогами состоит в уменьшении вычислений за счёт учёта логических связей между объектами. Также, при необходимости, оператор может изменить логические связи через удобный ему интерфейс без перекомпиляции решателя.

Разработана модификация алгоритма ABAA для решения задачи составления расписания – ABAA\M. В данной модификации используются следующие понятия.

Под обратной резолюцией будем понимать набор инструкций/шагов алгоритма абдуктивного вывода, т. е. вывод посылки, когда известны заключение и правило.

Например, для алгоритма ABAA обратная резолюция выражается в добавлении обоснования для вершины.

Будем говорить, что обратная резолюция литеры l с дизъюнктом d непротиворечива, если полученные в её результате формулы непротиворечивы.

Перефразируем это определение для алгоритма ABAA. Пусть вершина n помечена литерой l. Обратная резолюция литеры l с дизъюнктом d непротиворечива, если добавленные к вершине n обосновывающие вершины не обосновываются вершиной-противоречием.

Литеру, для которой должна быть выполнена хотя бы одна непротиворечивая обратная резолюция, будем называть !-литерой и в конце её названия приписывать символ '!'.

Литеру, для которой должны быть выполнены все возможные обратные резолюции, причём все полученные в её результате формулы не противоречивы, будем называть *-литерой и в конце её названия приписывать символ '*'.

Для алгоритма ABAA это определение сформулируем следующим образом. Литеру, для которой должны быть выполнены все возможные обратные резолюции, причём ни одна из вершин, которая обосновывает вершину, помеченную этой литерой, не должна обосновываться вершиной-противоречием, будем называть *-литерой и в конце её названия приписывать символ '*'.

Процесс нахождения литеры для непротиворечивого обратного резольвирования с вершиной, помеченной !-литерой, будем называть подтверждением, а найденную литеру – подтверждающей. Процесс нахождения литеры для противоречивого обратного резольвирования с вершиной, помеченной *-литерой, будем называть опровержением, а найденную литеру – опровергающей.

Первая особенность модифицированного алгоритма ABAA (ABAA\M) состоит в разрешении абдуктивно недопустимых унификаций, в отличие от алгоритма ABAA. Вторая заключается в возможности оперирования!-литерами и *-литерами, а также во введении условий останова процессов подтверждения и опровержения, которые формулируются как:

·  Если для вершины, помеченной !-литерой, найдена подтверждающая литера, то оставшиеся пары дизъюнкт-подстановка для этой вершины не рассматривать и перейти к рассмотрению следующей вершины, находящейся в том же обосновании, что и рассматриваемая вершина.

·  Если для вершины, помеченной *-литерой, найдена опровергающая литера, то оставшиеся пары дизъюнкт-подстановка для этой вершины не рассматривать, добавить в качестве обоснования этой вершины противоречие, а также добавить противоречие как обоснование всех вершин, находящихся во всех обоснованиях на пути от рассматриваемой вершины к вершине, непосредственно обосновывающей вершину верхнего уровня GOAL.

Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5