Алгоритм абдуктивного вывода с использованием систем поддержки истинности на основе предположений

Размещено на http://www.allbest.ru/

АЛГОРИТМ АБДУКТИВНОГО ВЫВОДА С ИСПОЛЬЗОВАНИЕМ СИСТЕМ ПОДДЕРЖКИ ИСТИННОСТИ НА ОСНОВЕ ПРЕДПОЛОЖЕНИЙ

В.Н. Вагин

К.Ю. Хотимчук

Московский Энергетический Институт (Технический Университет), Москва



В последнее время в интеллектуальных системах очень важную роль стал играть абдуктивный вывод, цель которого заключается в выводе причины для наблюдаемого события. Разработан алгоритм абдуктивного вывода AAA (Assumption-based Truth Maintenance System-based Abduction Algorithm). Результаты экспериментов, проведенных на примере задачи составления расписаний для энергохранилищ, подтвердили эффективность алгоритма AAA.

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

Индуктивный вывод - это вывод от частного к общему. Абдуктивный вывод заключается в выводе причины из наблюдаемого события и является выводом от частного к частному. Схематично абдуктивный вывод можно представить следующим образом. Пусть имеется правило и известно, что имеет место событие . Тогда, по абдукции, делаем заключение о том, что, быть может, имеет место и . Точнее, при заданной теории и наблюдении, предложенном для объяснения, абдуктивный вывод должен определить одно или более наилучших объяснений наблюдения на основе заданной теории. Термин “абдукция” впервые ввел американский философ Пирс [Peirce, 1955]. На сегодняшний день вывод по абдукции успешно применяется для решения задач диагностики [Cox et al., 1987], понимания естественного языка[Hobbs et al., 1993], распознавания, накопления знаний, составления расписаний и, несомненно, является очень важной частью интеллектуальных систем.

В настоящей работе мы рассматриваем понятие минимального абдуктивного объяснения, после чего приведём алгоритм абдуктивного вывода с использованием систем поддержки истинности, основанных на предположениях (Assumption-based Truth Maintenance Systems, ATMS). Показано применение алгоритма AAA для решения задачи составления расписаний для энергохранилищ.

1. Абдукция

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

Определение 1 [Marquis, 2000]. Пусть Ф - конъюнкция формул логики предикатов первого порядка (ЛП1П). H - конечное множество фактов, называемых предположениями (гипотезами). Упорядоченная пара T = <Ф, Н> - теория, построенная на предположениях.

Определение 2 (абдуктивного вывода). Пусть T = <Ф, Н> - теория, построенная на предположениях. Абдуктивный вывод заключается в выводе объяснения для наблюдаемого события д как подмножества г H, такое, что Ф & г ? д.

Заметим, что на г в определении 2 накладывается синтаксическое ограничение - г представляет собой конъюнкцию фактов.

Определение 3 [Marquis, 2000]. Пусть Т = <Ф, Н> - теория, основанная на предположениях, и д - формула логики предикатов первого порядка. Конъюнктивно интерпретируемое подмножество гH назовем абдуктивным объяснением д относительно Т, если:

Ф г ? д;

Ф г выполнимо.

Пример 1. Пусть Т = <Ф, Н>, где Ф = x (Студент(x) Юн(x)), д = Юн(Петров). Пусть H = {Студент(x₁), Рабочий(x₂)}. Тогда Студент(Петров), Студент(Петров) & Рабочий (Иванов) являются абдуктивными объяснениями д относительно T.

Заметим, что абдуктивное объяснение должно быть непротиворечиво. В примере 1 Студент(Петров) & Юн(Петров) не является абдуктивным объяснением д относительно T в силу противоречивости.

Определение 4 [Marquis, 2000]. Пусть Т = <Ф, Н> - теория, основанная на предположениях, д - формула логики предикатов первого порядка. Конъюнктивно интерпретируемое подмножество гH назовем минимальным абдуктивным объяснением д относительно Т, если:

г - абдуктивное объяснение для д относительно Т;

для любого абдуктивного объяснения г' для д относительно Т выполняется (гг') ( г'г).

Пример 2. Пусть Т = <Ф, Н>, где Ф = x (Студент(x) Юн(x)), д = Юн(Петров). Пусть H = {Студент(x₁), Рабочий(x₂)}. Тогда Студент(Петров) является минимальным абдуктивным объяснением д относительно T. Студент(Петров) & Рабочий (Иванов) не является минимальным абдуктивным объяснением д относительно T.

Задачу абдукции будем рассматривать как задачу нахождения множества минимальных абдуктивных объяснений наблюдаемого события.

2. Алгоритм абдуктивного вывода, использующий 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, subst>, в которых литера из 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.

Конец.

3. Пример работы алгоритма AAA

Пусть исходное множество дизъюнктов имеет вид

Наблюдается конъюнкт . Требуется найти множество его абдуктивных объяснений.

программный задача алгоритм энергохранилище

Рис. 1. Пример дерева вывода для алгоритма AAA



Алгоритм AAA строит дерево, изображённое на Рис. 3.1. В построенном дереве после удаления включаемых окружений и после замены переменной y1 на y получаем

Label(GOAL) =

Ответ:

4. Результаты экспериментов

Нами был разработан программный комплекс, реализующий алгоритм AAA. Для тестирования разработанного программного комплекса используется усеченная версия задачи о составлении расписаний для энергохранилищ [Denecker et al., 2002]. Число энергохранилищ изменялось от 1 до 50. В зависимости от этого количество правил изменялось от 7 до 1145. Требовалось найти все минимальные абдуктивные объяснения вводимых запросов, а означенные переменные в полученных минимальных абдуктивных объяснениях являлись искомыми параметрами задачи составления расписаний энергохранилищ. Так, например, для 50 энергохранилищ было получено 11350 минимальных абдуктивных объяснений, содержащих 7528 вариантов планирования. Алгоритм AAA эффективно решил поставленную задачу, что подтвердило его применимость в решении задачи абдукции, и в частности, в решении задачи планирования работы сложных технических объектов.

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

Благодарности. Работа выполнена при финансовой поддержке РФФИ (проект № 08-07-00212).



Список литературы

1. Вагин В.Н., Головина Е.Ю., Загорянская А.А. и др. Достоверный и правдоподобный вывод в интеллектуальных системах. - 2е изд., испр. и доп. / Под ред. Вагина В.Н. и Поспелова Д.А. - М.: ФИЗМАТЛИТ, 2008.

2. Cox P.T. and Pietrzykowski T. General diagnosis by abductive inference // Proc. IEEE Sympos. Logic Programming. San Francisco. 1987.

3. Denecker M., Kakas A. Abduction in Logic Programming // Computational Logic: Logic Programming and Beyond, Essays in Honour of Kowalski R.A., P. I, London, UK: Springer-Verlag. 2002. V. 2407.

4. Hobbs J., Stickel M.E., Appelt D. et al. Interpretation as abductior // Artificial Intelligence. 1993. 63(1 - 2).

5. Hwee Tou Ng, Mooney R.J. An Efficient First-Order Horn-Clause Abduction System Based on the ATMS // Proc. AAAI-91. Anaheim, CA. 1991.

6. Marquis P. Consequence finding algorithms // Handbook for Defeasible Reasoning and Uncertain Management Systems, eds. D.M. Gabbay and P. Smets. 2000. V. 5.

7. Peirce C.S., Philosophical writings. N.Y.: Dover Publications, Inc, 1955.

Размещено на Allbest.ru

...