автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Разработка и реализация методов и алгоритмов абдуктивного вывода с использованием систем поддержки истинности на основе предположений

На правах рукописи

лал ыми и

Хотимчук Кирилл Юрьевич ^Т2^

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

Специальность 05.13.17 - Теоретические основы информатики

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

2 С!ЮН 2011

Москва-2011

4848607

Работа выполнена на кафедре Прикладной математики Московского энергетического института (Технического университета)

Научный руководитель:

доктор технических наук, профессор Вагин Вадим Николаевич

Официальные оппоненты:

доктор физико-математических наук, профессор

Осипов Геннадий Семёнович; кандидат физико-математических наук, ведущий научный сотрудник Аверкин Алексей Николаевич

Ведущая организация:

ГУ "Российский НИИ информационных технологий и систем автоматизированного проектирования", г. Москва

Защита состоится «23» июня 2011 г. в 18 час. 00 мин. на заседании диссертационного совета Д 212.157.01 при Московском энергетическом институте (Техническом университете) по адресу: 111250, Москва, Красноказарменная ул., 17 (ауд. М 704).

С диссертацией можно ознакомиться в библиотеке Московского энергетического института (Технического университета).

Отзывы в двух экземплярах, заверенные печатью, просьба направлять по адресу: 111250, г. Москва, Красноказарменная улица, д.14, Ученый Совет МЭИ (ТУ).

Автореферат разослан «20» мая 2011 г.

Ученый секретарь

диссертационного совета Д 212.157.01 кандидат технических наук, доцент

М.В. Фомина

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

Одним из вариантов организации абдуктивного вывода, определяющим высокую скорость поиска решений, мощные средства для пересмотра решений и обеспечения непротиворечивости выводимых решений, является сохранение выводимых данных в системе поддержки истинности, основанной на предположениях (Assumption-based Truth-Maintenance System, ATMS).

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

В теорию и практику организации абдуктивного вывода большой вклад внесли отечественные учёные Финн В.К., Кузнецов С.О., Аншаков О.М., Виноградов Д.В., Рузавин Г.И., Васюков B.JI. и другие, а так же учёные Пирс Ч.С., Пол Г., Флэч П., Какас А., Габбай М., Бергадано Ф., Дюбуа Д., Прейд X., МакИлрайт ILL, Аллемань Д., Джозефсон Дж., Конолиге К., Ковальски Р., Тони Ф., Иноу К., Сакама Ч., Левек X., Кокс Ф., Пиетржиковски Т., Аппелт Д., Поллак М., Консоле Л., Дюпре Д., Пул Д. и другие.

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

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

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

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

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

Объектом исследования являются системы поддержки истинности, основанные на предположениях. Предметом исследования являются методы и алгоритмы систем поддержки истинности на основе предположений для реализации абдуктивного вывода.

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

Для достижения указанной цели требовалось решение следующих задач:

1) Исследование существующих методов и алгоритмов абдуктивного вывода.

2) Разработка алгоритма абдуктивного вывода с применением первичных импликат.

3) Разработка эвристического метода для алгоритма абдуктивного вывода с применением первичных импликат.

4) Исследование возможностей систем поддержки истинности на основе предположений для организации абдуктивного вывода.

5) Разработка на основе системы поддержки истинности, основанной на предположениях, алгоритма абдуктивного вывода.

6) Разработка модификации алгоритма абдуктивного вывода на основе системы поддержки истинности для решения задачи составления расписаний.

7) Разработка на основе системы поддержки истинности, основанной на предположениях, эвристического метода выбора начального порядка литер в исходных дизъюнктах.

8) Разработка и программная реализация на базе системы поддержки истинности алгоритма абдуктивного вывода.

9) Проверка работы алгоритма и его программной реализации на задаче составления расписания работ в сложных технических объектах.

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

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

Научная новизна. Новыми являются:

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

2. Эвристический метод выбора начального порядка в исходных литерах для алгоритмов абдуктивного вывода с использованием первичных импликат.

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

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

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

Практическая значимость работы подтверждена использованием полученных результатов в интеллектуальной системе поддержки принятия решений "СПРИНТ-РВ" и в учебном процессе в МЭИ (ТУ) при изучении дисциплины "Математическая логика", о чём имеются акты о внедрении.

Реализация результатов. Результаты диссертационной работы Хотимчука К.Ю. вошли в отчёты по НИР, выполняемым кафедрой ПМ по грантам РФФИ № 09-01-00076а "Исследование и разработка методов анализа данных и обнаружения знаний в «зашумленных» базах данных", № 08-07-00212 "Исследование и разработка методов и инструментальных средств индуктивного формирования понятий в интеллектуальных системах поддержки принятия решений", в отчёты по НИР, выполняемым Хотимчуком К.Ю. по гранту "У.М.Н.И.К.", а также были использованы в учебном процессе в курсе

"Математическая логика". На разработанный в диссертационной работе программный комплекс выдано свидетельство о государственной регистрации программы для ЭВМ №2010614887 (27 июня 2010 г.).

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 13-й, 16-й и 17-й научно-технических конференциях аспирантов и студентов "Радиоэлектроника, электротехника и энергетика" в МЭИ (ТУ) (г. Москва, 2007, 2010, 2011 г.), 11-й и 12-й национальных конференциях по искусственному интеллекту с международным участием КИИ-2008 (г. Дубна, 2008 г.) и КИИ-2010 (г. Тверь, 2010 г.), "Информационные технологии в науке, социологии, экономике и бизнесе" ГГ+в&Е'И (Украина, г. Гурзуф, 2011 г.), МНТК-2010 (г. Москва, 2010 г.), "Повышение эффективности электрического хозяйства потребителей в условиях ресурсных ограничений. Материалы Всероссийской научно-практической конференции с международным участием".

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 12 печатных работах, из них 3 - в журналах, относящихся к списку ВАКа.

Структура и объём работы. Диссертация состоит из введения, пяти глав, заключения, списка использованной литературы (72 наименования) и приложения. Диссертация содержит 114 страниц машинописного текста (без приложений).

СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

Разработан алгоритм ImpAA. Данный алгоритм позволяет найти множество минимальных абдуктивных объяснений с помощью первичных импликат. В данном алгоритме используются следующие понятия.

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

Пусть 8 - формула ЛП1П. Конъюнкт y=h1Ah2A...Ahk, где hi,h2,...,hk е Н, назовем абдуктивным объяснением 5 относительно Т, если:

• Ф л у f= 5;

• Ф л у выполнимо.

Конъюнкт y-hiAh2A...Ahk, г де hbh2,...,hk е Н, назовем минимальным абдуктивным объяснением 8 относительно Т, если:

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

• для любого абдуктивного объяснения у" для 5 относительно Т выполняется (у' |= у") -»(у" (= у').

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

Пусть L - конечное подмножество литер ЛП1П, £ — некоторая формула ЛП1П, Ф - конъюнкция формул ЛПШ, a Lit(d) - множество литер дизъюнкта d.

Дизъюнкт л является <L, Ф>-импликатой формулы I, если ФлХ [= я, Ф ^ п, и Lit(n) с L.

Дизъюнкт и' является <L, Ф>-первичной импликатой формулы Z, если:

• 7t - <L, Ф>-импликата формулы

• для всех <L, Ф>-импликат тс" формулы S выполняется {л" (=7t'}-»{u' ¡=я"}.

В алгоритме ImpAA используются следующие понятия.

Пусть L - множество литер ЛПШ. Расширенным дизъюнктом называется упорядоченный дизъюнкт, литеры которого берутся из множества Lu{[r], reL}. Множество {[г], reL} - это множество так называемых обрамлённых литер. Обрамление литеры является способом запомнить, что по данной литере мы уже резольвировали. Таким образом, если дизъюнкт содержит обрамлённую литеру [г], то это означает, что один из его родительских дизъюнктов содержит г.

Структурный дизъюнкт - это упорядоченная пара <<5, е>, где «У- дизъюнкт, е- расширенный дизъюнкт.

Далее представлены шаги разработанного алгоритма ImpAA.

Алгоритм 1. Алгоритм ImpAA._

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

clauses - исходное множество дизъюнктов, observed - набдадаемый конъюнкт. Выходные данные:

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

Начало. Шаг 1. Шаг 2.

ШагЗ.

Конец.

Создаем дизъюнкт clause = observed,

Обращаемся к процедуре SOLSoIve с параметрами clause, clauses, Lil(clause) и Lil(clauses), где Lit(clause) / Lit{clauses) - множество литер, встречающихся в дизъюнкте/дизъюнктах. Результат выполнения процедуры -множество implicates.

Для каждого дизъюнкта implicate из implicates создаем конъюнкт explanation = -1 implicate. Добавляем explanation к result.

Алгоритм SOLSoIve.

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

clause - дизъюнкт, для которого требуется найти множество <L, Ф> - первичных импликат,

ruleBase - имеющаяся база правил,

lit - множество литер, которые могут присутствовать в выводимых дизъюнктах. Выходные данные:

result - множество <L, Ф> - первичных импликат. Начало.

Шаг 1. Образование начального центрального структурного дизъюнкта topClause = «0>, <Lit(clause)>>. В качестве базы правил нужно взять имеющуюся базу правил, объединенную с clause. Шаг 2. Найти все первичные импликаты с помощью выполнения шага 4. ШагЗ. Выбрать из полученного на предыдущем шаге множества неповторяющиеся

дизъюнкты и записать их в result. Конец. Шаг 4. Поиск множества первичных импликат для поступающего на вход узла (структурного дизъюнкта). Возвращается множество дизъюнктов, которые являются первичными импликатами дизъюнкта, образованного из необрамленных литер родительского структурного дизъюнкта topClause, и где резольвировать можно только по литерам из второй компоненты topClause. Для узла, в котором произошел вызов данного шага, выполнить шаг 5, получив множество дизъюнктов si, и шаг 6, получив множество дизъюнктов s2. Возвратить si и s2.

Шаг 5. Рассматриваем 1 - первую литеру из второй компоненты topClause. Если 1 е lit, то осуществить перенос (правило Skip) литеры из второй компоненты topClause в первую, иначе Конец. Осуществить редукцию (шаг 7).

Если вторая компонента topClause пуста, то возвратить дизъюнкт, полученный из литер левой компоненты topClause.

Иначе: продолжить рекурсивный поиск для topClause — выполнить шаг 4. Шаг 6. Осуществить резолюцию (правило Resolve) первой литеры из второй компоненты со всевозможными дизъюнктами из базы правил. Пусть входной структурный дизъюнкт на данном этапе имеет вид ...

в*>, <1, h, ... /„», а подходящее правило rule = l'i, ...J't, -J, I'm, l'P, тогда

резольвента примет вид «ста/, аа2,... стар-, < al'i.....а/',, al'i+i, Ы'р, [а/], а//,...

<т/„». При выборе подходящего правила нужно соблюдать условие lit (rule) п fiamed({7, /¡, ... /„}) = 0. Кроме того, унификация а не должна изменить аргументы литеры I.

Осуществить редукцию (шаг 7) всех полученных резольвент и с ними перейти к шагу 4.

Шаг 7. Редукция поступающего на вход структурного дизъюнкта (правило Reduce).

Если в ... 1„ литера I встречается дважды, то удаляется ее самое левое вхождение. Получаем ¡'¡, ¡'г,... l'„i.

Если какая-либо литера из щ, 02, ... аь совпадает с некоторыми литерами из I1 ¡, lJ2, ... l'„i, то удаляем из последнего множества эти литеры. Получаем I2/,

I 2, ... 1 „2-

Удалить все обрамленные литеры из <l21, 122, ..., 12„2>, которым не предшествует обрамленная литера.

Конец.

Разработан эвристический метод для алгоритма 1трАА, который позволяет получить заметное ускорение для решения ряда абдуктивных задач. Данный эвристический метод использует выбор начального порядка литер в исходных дизъюнктах в целях уменьшения числа шагов алгоритма ЗОЬ-резолюции. Метод заключается в упорядочивании литер в дизъюнкте по возрастанию функции Яапк(г, ЯикВазе), действующей на декартовом произведении множества литер и множества множеств дизъюнктов во множество целых чисел и определённой ниже, где г - литера, ЯикВаяе - множество дизъюнктов. Ранг литеры г в ШиЫВазе определяется следующим образом. Находятся дизъюнкты ¿¡, ... с1п, содержащие —¡г, \//е{1,..., и} 4' £ ЯиЬВаэе. Тогда О, если п = О,

Rank(r, RuIeBase) =

1 + £ ]Г Rank(h, RuIeBase \ {dl}),

¡-О Аеламць»-)

в противном случае.

Таким образом, на первых местах (самых левых) в е оказываются литеры, которые, по предложенной функции, приведут к порождению наименьшего числа дизъюнктов. Ранг 0 имеет та литера, по которой резольвирование вообще не происходит. Алгоритмом 1шрАА\Н назовём модифицированный алгоритм 1трАА, который перед своим выполнением производит упорядочение литер в исходных дизъюнктах согласно предложенной эвристике.

Пусть 5 - формула ЛП1П. Будем говорить, что унификация о абдуктивно недопустима для 8 относительно Т, если в результате её применения выводится формула у, такая что:

• у является минимальным абдуктивным объяснением а5 относительно Т и

• у не является минимальным абдуктивным объяснением 5 относительно Т.

Разработаны модификации алгоритмов 1трАА и 1трАА\Н - 1трАА\М и

1трАА\М\Н соответственно. В данных модификациях разрешены абдуктивно недопустимые унификации, которые не разрешены в 1трАА и 1трАА\Н. Данные модификации позволяют использовать разработанные алгоритмы в решении задачи составления расписания.

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

массивах данных, как большой объем, а также неполнота и противоречивость данных.

Основной структурой данных ATMS является вершина (node), которая имеет формат <данное, метка, обоснованиям Возможны следующие типы вершин ATMS:

• предположение - обозначает допущение о некотором факте, принятое за истину, но которое может стать ложным, и отвергнуто из дальнейшего рассмотрения;

• выведенная вершина - некоторое утверждение, выведенное решающей системой;

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

С каждым утверждением связывается обоснование, состоящее из трех частей: обосновываемой вершины, называемой заключением, списка обосновывающих вершин и описания обоснования решающей системой. Обоснования имеют следующий вид: =>п, где xl,x2....,x¡ - родительские

вершины, а га - заключение. Данными вершин обоснования выступают атомы. Таким образом, обоснование представляет импликацию X, AXy..Xt ->N, где

Xl,X1.....Xt,N - это данные вершин д:,,^,...,*,,« соответственно. Таким образом,

обоснования - это хорновские дизъюнкты.

Множество предположений ATMS называется окружением. Также вводится противоречивое окружение, представляющее собой противоречивую конъюнкцию предположений.

Говорят, что вершина п содержится в окружении Е, если п может быть получена из £ и текущего множества обоснований J.

Окружение противоречиво, если из него выводима ложь (1).

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

Есть три основные операции ATMS: создание вершины с информацией решающей системы, создание предположения и добавление обоснования к вершине. Эти операции проиллюстрированы на рис. 1 - 3. На рис. 1 создаются вершины с данными А, В и С, на рис. 2 - предположения D и Е. На рис. 3 к вершине А добавляется обоснование В а С, к вершинам В и С - обоснования D и Е соответственно. Здесь овалом (кругом) обозначается выведенная вершина, а прямоугольником (квадратом) - вершина-предположение.

Е

Рис. 1

Рис.2

Рис.3

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

здесь j,k - метка i-й вершины k-ro обоснования вершины п. Если метки рассматривать как пропозициональные выражения в дизъюнктивной

нормальной форме, то метка вершины п вычисляется как va J¡k .

к i

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

________________¿г_____________________

ujji апгмацпп L-.W< r\ i iliirnji w оошида.

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

Алгоритм 1. Алгоритм АВАА._

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

clauses - исходное множество дизъюнктов, observed- наблюдаемый конъюнкт. Выходные данные:

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

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

Шаг 2. Вычислить множество extendedClauses = clauses U Factor(clauses), где Factor(clauses) - множество всевозможных факторов дизъюнктов из clauses.

ШагЗ. Пусть 01,02... - это литеры observed. Создать вершину GOAL (операция добавления вершины в ATMS) и добавить к ней обоснование 0[,02... —> GOAL . nO¡, пОг-.. - добавленные таким образом новые вершины (операция добавления обоснования в ATMS). Шаг 4. Выполнить процедуру Assume с параметрами пО„ О¿ для i=l,2.. (операция

добавления предположения в ATMS) Шаг 5. Выполнить процедуру Р rocessNode с пар аметрами GOAL , extendedClauses, GOAL, 0.

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

Конец.

Процедура Assume.

Исходные данные: node - вершина,

litera - литера, по которой делается предположение. Требуется:

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

Начало.

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

Конец.

Процедура ProcessNode.

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

node - текущая вершина, clauses - множество дизъюнктов, mainNode - целевая вершина,

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

предположение.

Требуется:

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

Начало.

Шаг 1. Обозначим / = 1 - номер обоснования; justificationCount - число обоснований.

Шяг 9. Если i > hiRtificatinnC.mmt. то Конец. Иначе рассмотрим justification - i-e обоснование вершины node. Вызвать процедуру ProccssJustification с параметрами justification, clauses, mainNode, unassumed.

Шаг 3. Присваиваем í = i +1 и переход к шагу 2.

Конец.

Процедура ProcessJustification.

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

justification - текущее обоснование, clauses - множество дизъюнктов, mainNode - целевая вершина,

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

предположение.

Требуется:

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

Начало.

Шаг 1. Пусть nodeCount - число вершин в justification; i = 1 - номер вершины в justification.

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

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

Шаг 4. Если substNumber > substitutionCount, то i = i +1 и переход к шагу 2. Иначе рассмотрим пару дизъюнкт-подстановку substitution - substNumber-я элемент в substitutions. Пусть substitution представляет пару clause - дизъюнкт и subst -подстановка.

Шаг 5. Резолюция по node с дизъюнктом clause с добавлением нового обоснования newJustification к node. п01,п02,... - узлы обоснования newJustification, 0V02,... - литеры, соответствующие этим узлам (операции создания вершины и добавления обоснования в ATMS). Пусть firstUnassumedLitera - первая литера в unassumed. Среди литер 0,,03,... найти firstUnassumedLitera. Пусть это Злкшшккмлйв- • Если литера не найдена, то unassumedNumber = -1. Выполнить процедуру Assume с параметрами n0jt0j, j = 1.., j ф unassumedNumber (операция добавления предположения в ATMS). Если unassumedNumber ф -1, то удалить из unassumed первую литеру. Выполнить процедуру ProcessNode с параметрами node, clauses, mainNode, unassumed. Шаг 6. Присвоить substNumber - substNumber +1 и переход к шагу 4. Конец.

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

Составление расписаний - это область, в которой в последнее время абдуктивный вывод находит успешное применение. Классическая задача составления расписаний заключается в следующем. Пусть необходимо обслужить множество N= {1, 2, ..., п] требований. Требование к, к е {1,..., и} поступает на обслуживание в момент времени > 0 и для обслуживания требует tk > 0 единиц времени. Процесс обслуживания может быть описан заданием кусочно-постоянной, непрерывной слева функции S = S (/), принимающей при 0 < t < оо одно из значений 0, 1, 2,..., п. Если S (t) = к Ф 0, то в момент времени t прибор обслуживает требование к, если S (f) = 0, то в момент времени t ни одно из требований не обслуживается. Эта функция называется расписанием и её требуется найти.

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

• задано множество работ / = { j\,j2, ■■■]„};

• задано множество значений единиц времени Т;

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

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

Длиной расписания S будем называть len( S ) = maxf S(j) + г (j) ).

jeJ

Требуется найти расписание S, такое что len(S) —» min.

Идея применения вывода по абдукции в решении задачи составления расписания состоит в следующем. Рассмотрим соотношение ^>д77г)= /. Пусть Th - это логическая теория первого порядка, представляющая условия и ограничения предметной области, ср - формула логики первого порядка, содержащая константы Ts (время начала работы j) и ТЕ (время окончания работы j). Пусть <рлТк\=/, где / = sheduled(j,Ts,TE) представляет собой период выполнения [Ts> ТЕ] работы j. Теперь пусть наблюдается

/у з $Иес1и1е<3(у, ^, ^). Здесь Г?, 4- - переменные. Задача состоит в нахождении объяснений для /¡, в процессе получения которых переменные ?£ означиваются.

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

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

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

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

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

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

Перефразируем это определение для алгоритма АВАА. Пусть вершина п помечена литерой /. Обратная резолюция литеры I с дизъюнктом с1 непротиворечива, если добавленные к вершине п обосновывающие вершины не обосновываются вершиной-противоречием.

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

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

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

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

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

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

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

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

На классическом примере задачи о составлении расписаний для технических работ продемонстрировано преимущество использования эвристического метода. Использование эвристического метода в моделирующей подсистеме даёт улучшение во временных показателях и уменьшает число выведенных вершин.

Далее представлены шаги разработанного эвристического алгоритма ReArrangeLiteras.

Алгоритм 3. Алгоритм ReArrangeLiteras._

Алгоритм ReArrangeLiteras

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

ruleBase - база правил.

Требуется:

переставить литеры в дизъюнктах ruleBase для того, чтобы сократить процесс опровержения (т.е., построить как можно меньше вершин).

Начало.

Шаг 1. Найти в ruleBase все дизъюнкты, содержащие хотя бы одну *-литеру.

Обозначим их множество как StarClauses. Пусть N - число таких дизъюнктов. Рассмотрим i - номер текущего дизъюнкта. Присвоим i = 1. Шаг2. Если i>N, то Конец. Иначе рассмотрим clause - i-й дизъюнкт в

StarClauses. Пусть литера lit - *-литера в этом дизъюнкте. Найти все дизъюнкты в ruleBase, в которых lit встречается без отрицания. Обозначим найденное множество как S. Пусть NS - число таких дизъюнктов. Рассмотрим j - номер текущего дизъюнкта. Присвоим 7 = 1.

ШагЗ. Если j>NS, то присваиваем /' = ;'+ 1 и переход к шагу 2. Иначе

рассмотрим clause - j-й дизъюнкт в S. Выполнить процедуру AnalyzeMath с параметрами clause, ruleBase. Выполнить процедуру AnalyzeArgumentCover с параметром clause. Присваиваем j =j + 1 и переход к шагу 3 Конец.

Алгоритм AnalyzeMath

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

clause - дизъюнкт. Требуется:

Переставить математические литеры в дизъюнкте clause в конец вплоть до положительной литеры. Начало.

Шаг 1. Пусть N - число отрицательных литер в дизъюнкте clause. Рассмотрим / -

номер текущей литеры. Присвоим i = 1. Шаг 2. Если i > N, то Конец. Иначе рассмотрим lit - i-ю литеру в clause. Если это

математическая литера, то поменять её местами с N-й литерой в дизъюнкте clause, ирисвишь N — N— 1 и (С uiäiy 2. Иначе присвоить / = i + 1 и к шагу 2.

Конец.

Алгоритм AnalyzeArgumentCover

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

clause - дизъюнкт вида —i/, v—1/2 v...v-п/^ v-i/и, v-,m2 v...v-пт^ vi, где lul2,...,lN¡ -литеры, не являющиеся математическими, - литеры, являющиеся

математическими. Требуется:

Переставить литеры /15/2/v в дизъюнкте clause так, чтобы аргументы, от значений которых зависят значения других аргументов, означивались как можно раньше, и самой левой литерой в дизъюнкте была литера с максимальным пересечением по аргументам с положительной литерой I. Начало.

Шаг 1. Пусть Arguments - множество рассматриваемых аргументов. Присвоим

Arguments = Args(l)\[jArgs(mj). Рассмотрим ; - текущая позиция литеры.

п

Присвоим i = 1. Шаг 2. Если i > N,

-1, то Конец. Иначе найти такую литеру litera среди /,,/2,...,ív , что I Arguments п Args(litera)¡-> max . Присвоить

Arguments = Arguments и ArgsQitera). Поменять местами в дизъюнкте clause литеры litera и /,. Присвоить= i + 1 и к шагу 2. Конец.

На рис. 4 представлен график зависимости времени выполнения программы от числа технических работ для четырёх предложенных в этой работе алгоритмов - ImpAAYM, ImpAAYMYH, АВАА\М, АВАА\М\Н. Эксперимент проводился на машине Core 2 Duo 2,20 GHz. Для 50 технических работ алгоритм АВАА\М по сравнению с алгоритмом ImpAA\M\H даёт выигрыш в 3 раза по времени, по сравнению с алгоритмом ImpAA\M даёт выигрыш в 4 раза по времени. Алгоритм ImpAA\M\H по сравнению с алгоритмом ImpAA\M даёт

выигрыш 1,3 раза по времени. Алгоритм АВАА\М\Н по сравнению с алгоритмом АВАА\М даёт выигрыш в 1,3 раза по времени.

О 5 10 15 20 25 30 35 40 45 50 Число технических работ

Рис.4

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

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

Архитектура разработанного программного комплекса состоит из ' пользовательского интерфейса, транслятора базы знаний, транслятора запросов, I решателя, математического сопроцессора и библиотеки ЛП1П.

Пользовательский интерфейс отвечает за взаимодействие пользователя с ' программным комплексом - ввод информации и получения конечного результата - расписания работ в сложном техническом объекте.

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

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

Решатель выполняет алгоритм абдуктивного вывода. Помимо реализации абдуктивного вывода с использованием систем поддержки истинности на основе предположений (алгоритм АВАА\М\Н), разработана реализация

абдухтивного вывода с использованием первичных импликат (алгоритма 1шрАА\М\Н). В зависимости от предпочтения пользователей, решатель использует тот или иной алгоритм.

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

Ь.^ШиШШДШШШМЦД .1111 ^ Ш1ДЦЕГ ■____

■"Файл "Вид- '■

в1аг1(т, Ь, е) 51аг[СопсМоп(т, Ь, е) рюЫЫ1ес£оп(№оп(т, Ь, е) таюЦт) иеек(1ч) (1ига1юп1т, с1) таЬуог.ипЩт, и) ргоЬЫеф, р$. ре)

s(drtCondKвn(ntb^l & рюЬЫЫСогхвкП^ггЬ«) > «ЬйСпьЬ^Х-

та|'гЛ(т) & иеёк(Ь) Ь йигайопЦсЧ I иеек(е) I асЙ(ЬДа) Ь яЛтейас^аХе) > 4!з:Спгк1&п(т^5.е). пййЦоСипНОп. и) & рпКЫЬасЦи; Ьр. ер) I ю(_сквятд(Ь, е, Ьр, ер) > ргаЬ1Ые(Ср«5йоп(т, Ь, е). таиг1(М1).

таит1(М2).

шатцт^.

■с5ара$оп!«.152)иеек(щ)., -.¡..-¡-г, I • ..

¿ига!!оп(М1,-4). . ■ . ■ '"• .

ёига1юп[М2,31). . : :;Г.

А1га1юп(МЗ,12). - . ■, '

та1п(_Ро1_игв1[М1,и1). та1пНог_ипй[М2, и2). :'...': та1п(_(ог_цпй(МЗ, 1)3).

ргоИЫефЛА?). ргоИЬйеёЕШ, 35.38). ргоЫЬКе^иг. 4.7). prohbiietiUZ.35.38). рго№ВДи3.4.7). рго№йес!(иЗ, 35.38).

Рис. 5

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

2) Выполнено исследование и анализ систем поддержки истинности. Особое внимание уделено системам поддержки истинности, основанньм на предположениях, ключевым достоинством которых является сохранение выводов, что приводит к кэшированию промежуточных результатов, в результате чего нет необходимости в повторных вычислениях. Благодаря своим характеристикам, система поддержки истинности, основанная на

предположениях (ATMS), выбрана в качестве основы для построения абдуктивного алгоритма.

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

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

5) Разработан эвристический метод для алгоритма аиду ктииниш вывода, использующего систему поддержки истинности на основе предположений. Показано, что применение данного метода позволяет повысить эффективность алгоритма АВАА благодаря сокращению пространства поиска.

6) С использованием результатов данной работы на основе ATMS разработан и реализован программный комплекс, осуществляющий составление расписания работ в сложных технических объектах. Программный комплекс тестировался на примере задачи составления расписаний для технических работ.

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Вагин В.Н., Хотимчук KJO. Методы абдуктивного вывода в задачах планирования работы в сложных объектах // Известия РАН. Теория и системы управления, 2010, №5, с. 95-113.

2. Вагин В.Н., Хотимчук KJO. Абдуктивный вывод versus дедукция // Программные продукты и системы, 2010, №4, с. 106-110.

3. Вагин В.Н., Хотимчук К.Ю. Абдукция в задачах планирования работ в сложных объектах // Искусственный интеллект и принятие решений. - М.: Ленанд, 2011. - Т.1 с.3-13.

4. Хотимчук К.Ю. Исследование методов нахождения минимальных абдуктивных объяснений // Радиоэлектроника, Электротехника и Энергетика. Тринадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. T.I. М.: Издательский дом МЭИ, 2007. -508с. с. 378-379.

5. Хотимчук К.Ю. Исследование и разработка методов нахождения минимальных абдуктивных объяснений // Технологии Microsoft в теории и практике программирования: труды IV Всероссийской конференции студентов, аспирантов и молодых учёных. Центральный регион. Москва, 2-3 апреля 2007 г. - М.: Вузовская книга, 2007. - 211 с. с. 127 - 128.

6. Хотимчук К.Ю. Применение первичных импликат для нахождения минимальных абдуктивных объяснений // Труды международной научно-

технической конференции "Информационные средства и технологии". 16-18 октября 2007 г., в 3-х т. Т 3. - М.: МЭИ, 2007. - 220 с. с. 65 - 68.

7. Вагин В.Н., Хотимчук К.Ю. Нахождение минимальных абдуктивных объяснений с помощью первичных импликат II Тр. 11й национальной конференции по искусственному интеллекту с международным участием (КИИ-2008. г. Дубна, Россия). 2008. Т. 2. Р. 345-355.

8. Хотимчук KJO. Решение задачи планирования работы сложных технических объектов с помощью алгоритмов абдуктивного вывода // Повышение эффективности электрического хозяйства потребителей в условиях ресурсных ограничений. Материалы Всероссийской научно-практической конференции с международным участием (Москва, 16-20 ноября 2009 г.) / Под общ. Ред. Б. И. Кудрина и Ю. В. Матюниной. В 2-ч т. М.: Технетика, 2009. Том II - 258 с. с. 174 - 176.

9. Хотимчук К.Ю. Применение алгоритмов абдуктивного вывода в решении задачи планирования работы сложных технических объектов /'/' Радиоэлектроника, Электротехника и Энергетика. Шестнадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. T.I. М.: Издательский дом МЭИ, 2010. - 492с. с. 386 - 387.

10.Вагин В.Н., Хотимчук KJO. Алгоритм абдуктивного вывода с использованием систем поддержки истинности на основе предположений // Двенадцатая национальная конференция по искусственному интеллекту с международным участием КИИ-2010 (20-24 сентября 2010 г., г. Тверь, Россия): Труды конференции. Т. 1. - М.: Физматлит, 2010. - 392 с. с. 73 -82.

11 Хотимчук К JO. Абдуктивный вывод с использованием систем поддержки истинности на основе предположений // Труды XVI Международной научно-технической конференции "Информационные средства и технологии". 19 - 21 октября 2010г., Москва. В 3 томах. Т.2. М.:Издательский дом МЭИ. 359 с. с. 242 - 249.

12 Хотимчук К JO. Алгоритм абдуктивного вывода для решения задачи планирования работы сложных технических объектов // Радиоэлектроника, Электротехника и Энергетика. Семнадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. T.I. М.: Издательский дом МЭИ, 2011. - 488с. с. 385 - 386.

Свидетельство о государственной регистрации программы для ЭВМ "Fast

Abductive Solver" №2010614887 (27 июня 2010 г.).

Подписано в печать /К CÓ • U зак. Ш TnpjQV Пл. ^г^ Полиграфический центр МЭИ(ТУ) Красноказарменная ул.,д.13

Введение.

1. Абдуктивный вывод: обзор.

1.1. Основные понятия и определения.

1.2. Подходы к организации абдуктивного вывода.

1.2.1. Подход на основе покрытия множеств.

1.2.2. Подход на основе логики.

1.2.3. Подход на уровне знаний.

1.2.4. Подход на основе вероятностных методов.

1.3. Подходы к отбору гипотез.

1.4. Организация абдуктивного вывода с применением теории аргументации.

1.4.1. Основные понятия теории аргументации.

1.4.2. Нахождение множества обоснованных гипотез.

1.5. ДСМ-метод автоматического порождения гипотез.

1.6. Выводы по главе 1.

2. Методы и алгоритмы абдуктивного вывода.

2.1. Алгоритм нахождения минимальных покрытий.

2.2. Алгоритм абдуктивного вывода с применением первичных импликат.

2.2.1. Алгоритм 1трАА.

2.2.2. Примеры работы алгоритма 1трАА.

2.2.3. Эвристический метод для алгоритма 1шрАА.

2.3. Алгоритм абдуктивного вывода с применением теории аргументации.

2.3.1. Алгоритм построения целевых деревьев.

2.3.2. Пример работы алгоритма построения целевых деревьев.

2.3.3. Использование алгоритма целевых деревьев в организации абдуктивного вывода.

2.4. Абдуктивный вывод в логике предикатов первого порядка.

2.5. Выводы по главе 2.

3. Системы поддержки истинности.

3.1. Обзор систем поддержки истинности.

3.1.1. Основные достоинства систем поддержки истинности.

3.1.2. Семейства систем поддержки истинности.

3.2. Система поддержки истинности, основанная на предположениях.

3.2.1. Архитектура систем рассуждения.

3.2.2. Основные определения.

3.2.3. Основные структуры данных.

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

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

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

3.6. Выводы по главе 3.

4. Решение задачи составления расписаний работ в сложных технических объектах и их подсистемах.

4.1. Задача составления расписаний в искусственном интеллекте.

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

4.3. Задача о составлении расписания технических работ.

4.4. Модификация алгоритма абдуктивного вывода с использованием систем поддержки истинности, основанных на предположениях.

4.4.1. Первая модификация алгоритма абдуктивного вывода с использованием систем поддержки истинности, основанных на предположениях.

4.4.2. Вторая модификация алгоритма абдуктивного вывода с использованием систем поддержки истинности, основанных на предположениях.

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

4.6. Модификации алгоритмов 1трАА и 1трАА\Н.

4.7. Практические результаты.

4.8. Выводы по главе 4.

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

5.1. Архитектура программного комплекса.

5.2. Язык запросов программного комплекса.

5.3. Сценарии взаимодействия пользователя и программного комплекса.

5.4. Выводы по главе 5.

Актуальность темы исследований. Важной задачей, с которой сталкиваются при проектировании систем поддержки принятия решений, является разработка таких моделей и методов, которые способны функционировать в открытых и динамичных проблемных областях, с возможностью корректировки и пополнения модели принятия решений в процессе поиска. Абдуктивный вывод успешно используется для достижения этой цели, и заключается в выводе причины для наблюдения. Термин "абдукция" впервые ввел американский философ Пирс[1]. Вывод по абдукции не является строгим, это правдоподобный вывод, который может подвергаться пересмотру, что позволяет повысить гибкость разрабатываемых моделей и методов для интеллектуальных систем.

Вывод по абдукции успешно применяется для решения задач диагностики неисправностей [2], распознавания образов, понимания естественного языка [3], накопления и обработки знаний, пересмотра убеждений, в автоматизированном планировании [4] и составлении расписаний.

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

Одним из вариантов организации абдуктивного вывода, определяющим высокую скорость поиска решений, мощные средства для пересмотра решений и обеспечения непротиворечивости выводимых решений, является сохранение выводимых данных в системе поддержки истинности, основанной на предположениях (Assumption-based Truth-Maintenance System, ATMS).

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

В теорию и практику организации абдуктивного вывода большой вклад внесли отечественные учёные Финн В.К., Кузнецов С.О., Аншаков О.М., Виноградов Д.В., Рузавин Г.И., Васюков B.J1. и другие [5-8], а так же учёные Пирс Ч.С., Пол Г., Флэч П., Какас А., Габбай М., Бергадано Ф., Дюбуа Д., Прейд X., МакИлрайт Ш., Аллемань Д., Джозефсон Дж., Конолиге К., Ковальски Р., Тони Ф., Иноу К., Сакама Ч., Левек X., Кокс Ф., Пиетржиковски Т., Аппелт Д., Поллак М., Консоле Л., Дюпре Д., Пул Д. и другие [1, 925].

В организации абдуктивного вывода популярным является подход на уровне логики. В развитие этого подхода внесли свой вклад такие учёные, как Пол Г., Флэч П., Какас А., Габбай М., МакИлрайт Ш., Ковальски. Р., Тони Ф. [9-11,15,18]. Суть этого подхода заключается в том, что знания представляются в виде обобщённых логических теорий, в которых литера может выступать и как следствие, и как причина. Данный подход является очень гибким для реализации большинства механизмов абдуктивного вывода в современных интеллектуальных системах.

При реализации алгоритмов абдуктивного вывода в рамках подхода на основе логики могут использоваться возможности, предоставляемые системами поддержки истинности [26-40]. Значительный вклад в исследование и разработку систем поддержки истинности внесли такие учёные, как Дойл Дж. [27], разработавший одну из самых первых систем поддержки истинности, ДеКлир Дж. [33-37], который ввёл термин "основанный на предположениях" и представил соответствующую систему поддержки истинности, МакАллестер Д. [28-30], Рейтер Р. [31, 35], Мартине Дж. [32], Форбус К. [26, 36] и другие. К достоинствам данных систем относится обеспечение объяснений и сохранение произведённых и промежуточных выводов, работа с противоречиями, умолчаниями, новыми фактами и обоснованиями.

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

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

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

Объектом исследования являются системы поддержки истинности, основанные на предположениях. Предметом исследования являются методы и алгоритмы систем поддержки истинности на основе предположений для реализации абдуктивного вывода.

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

Для достижения указанной цели требовалось решение следующих задач:

1. Исследование существующих методов и алгоритмов абдуктивного вывода.

2. Разработка алгоритма абдуктивного вывода с применением первичных импликат.

3. Разработка эвристического метода для алгоритма абдуктивного вывода с применением первичных импликат.

4. Исследование возможностей систем поддержки истинности на основе предположений для организации абдуктивного вывода.

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

6. Разработка модификации алгоритма абдуктивного вывода на основе системы поддержки истинности для решения задачи составления расписаний.

7. Разработка на основе системы поддержки истинности, основанной на предположениях, эвристического метода выбора начального порядка литер в исходных дизъюнктах.

8. Разработка и программная реализация на базе системы поддержки истинности алгоритма абдуктивного вывода.

9. Проверка работы алгоритма и его программной реализации на задаче составления расписания работ в сложных технических объектах.

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

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

Научная новизна. Новыми являются:

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

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

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

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

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

Практическая значимость работы подтверждена использованием полученных результатов в интеллектуальной системе поддержки принятия решений "СПРИНТ-РВ" и в учебном процессе в МЭИ (ТУ) при изучении дисциплины "Математическая логика", о чём имеются акты о внедрении.

Реализация результатов. Результаты диссертационной работы Хотимчука К.Ю. -ч вошли в отчёты по НИР, выполняемым кафедрой ПМ по грантам РФФИ № 09-01-00076а "Исследование и разработка методов анализа данных и обнаружения знаний в «зашумленных» базах данных", № 08-07-00212 "Исследование и разработка методов и инструментальных средств индуктивного формирования понятий в интеллектуальных системах поддержки принятия решений", в отчёты по НИР, выполняемым Хотимчуком К.Ю. по гранту "У.М.Н.И.К.", а также были использованы в учебном процессе в курсе "Математическая логика". На разработанный в диссертационной работе программный комплекс выдано свидетельство о государственной регистрации программы для ЭВМ №2010614887 (27 июня 2010 г.).

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 13-й, 16-й и 17-й научно-технических конференциях аспирантов и студентов "Радиоэлектроника, электротехника и энергетика" в МЭИ (ТУ) (г. Москва, 2007, 2010, 2011 г.), 11-й и 12-й национальных конференциях по искусственному интеллекту с международным участием КИИ-2008 (г. Дубна, 2008 г.) и КИИ-2010 (г.

Тверь, 2010 г.), "Информационные технологии в науке, социологии, экономике и бизнесе" IT+S&E'll (Украина, г. Гурзуф, 2011 г.), МНТК-2010 (г. Москва, 2010 г.), "Повышение эффективности электрического хозяйства потребителей в условиях ресурсных ограничений. Материалы Всероссийской научно-практической конференции с международным участием".

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 12 печатных работах, из них 3 — в журналах, относящихся к списку ВАКа.

Структура и объём работы. Диссертация состоит из введения, пяти глав, заключения, списка использованной литературы (69 наименований) и приложения. Диссертация содержит 118 страниц машинописного текста (без приложений).

5.4. Выводы по главе 5

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

С использованием результатов данной работы разработано программный комплекс решения задачи составления расписания (Глава 4), использующий систему поддержки истинности, основанную на предположениях (Глава 3), которая является базой для разработанного алгоритма (Глава 3) и используется последним для хранения промежуточных результатов, что сокращает повторные вычисления. Данный программный комплекс использует разработанную эвристику (Глава 4) для сокращения пространства поиска.

5. Заключение

В данной работе получены следующие результаты.

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

2. Выполнено исследование и анализ систем поддержки истинности. Особое внимание уделено системам поддержки истинности, основанным на предположениях, ключевым достоинством которых является сохранение выводов, что приводит к кэшированию промежуточных результатов, в результате чего нет необходимости в повторных вычислениях. Благодаря своим характеристикам, система поддержки истинности, основанная на предположениях (ATMS), выбрана в качестве основы для построения абдуктивного алгоритма.

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

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

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

6. С использованием результатов данной работы на основе ATMS разработан и реализован программный комплекс, осуществляющий составление расписания работ в сложных технических объектах. Программный комплекс тестировался на примере задачи составления расписаний для технических работ.

1. Peirce C.S., Philosophical'writings. N.Y.: Dover Publications, Inc, 1955. P. 386.

2. Cox P.T. andPietrzykowski T. General diagnosis by abductive inference // Proc. IEEE

3. Sympos. Logic Programming. San Francisco. 1987. P. 183-189.

4. Hobbs J., Stickel M.E., Appelt D. et al. Interpretation as abduction // Artificial Intelligence.1993.63(1 -2). P. 69-142.i

5. Eshghi K. Abductive planning with the event calculus. // Robert A. Kowalski, Kenneth A. Bowen editors: Logic Programming, Proc. of the Fifth International Conference and Symposium, Seattle, Washington, August 15-19, 1988. MIT Press, 1988, P.562-579.

6. Финн В.К. Синтез познавательных процедур и проблема индукции // Интеллектуальные системы и общество: сборник статей, изд.2-е, испр. и существ, доп., Москва: КомКнига, 2006. 352с. С. 130-219.

7. Виноградов Д.В. Формализация правдоподобных рассуждений в логике предикатов //

8. ДСМ-метод автоматического порождения гипотез: Логические и эпистемологическиеоснования, Москва: Книжный дом "ЛИБРОКОМ", 2009. 432 с. С. 287-293.

9. Рузавин Г.И. Абдукция как метод поиска и обоснования объяснительных гипотез //

10. Теория и практика аргументации. М., 2001. с. 28-48.

11. Васюков B.JI. Научное открытие и контекст абдукции // Философия науки. Вып. 9. М.:1.ИФ РАН, 2003. с. 180-205.

12. Flach P.A., Kakas А.С. On the relation between abduction and inductive learning //

13. Handbook of defeasible reasoning and uncertainty management systems: Volume 4 abductive reasoning and learning, Kluwer Academic Publishers Norwell, MA, USA, 2000, P. 1-33.

14. Bergadano F., Cutello V., Gunetti D. Abduction in machine learning // Handbook of defeasible reasoning and uncertainty management systems: Volume 4 abductive reasoningj and learning. Kluwer Academic Publishers Norwell, MA, USA, 2000, P. 197-229.

15. Dubois D., Prade H. An overview of ordinal and numerical approaches to causal diagnosticproblem solving // Handbook of defeasible reasoning and uncertainty management systems:

16. Volume 4 abductive reasoning and learning. Kluwer Academic Publishers Norwell, MA, USA, 2000, P. 231 -280.r '5 ' , 'i i

17. Kakas A.C., Kowalski R.A., Toni F. The role of abduction in logic programming // Handbook of Logic in Artificial Intelligence and Logic Programming / Ed. Gabbay D.M., Hogger C J. and Robinson J.A. Oxford, UK. Oxford University Press. 1998, P. 235-324.

18. Inoue K., Sakama C. Abductive framework for nonmonotonic theory change // Proc. 14th International Joint Conference on Artificial Intelligence, Montreal, Quebec, Canada, 1995, P. 204-210.

19. Levesque H. A knowledge-level account of abduction // Proc 11th International Joint Conference on Artificial Intelligence. San Francisco, CA, USA. 1989. P. 1061-1067.

20. Cox P., Pietrzykowski T. Causes for Events: Their Computation and Applications. // Proc. 8th International Conference on Automated Deduction, Oxford, England, 1986, P. 608-621.

21. Pople H. E. On the mechanization of abductive logic // Proc. of the 3rd international joint conference on Artificial intelligence, 1973, San Francisco, CA, USA 1973, P. 147-152.

22. Appelt D.E., Pollack M.E. Weighted Abduction for Plan Ascription // Proc. of User Modelling and User-Adapted Interaction, Volume 2(1-2) 1992, Kluwer, Netherlands, P. 1-25.

23. Console L., Dupre D. T. Abductive Reasoning with Abstraction Axioms // Foundations of Knowledge Representation and Reasoning, (G. Lakemayer, B. Nebel eds.), Lecture Notes in Computer Science 810, Springer Verlag, 1994, P. 98-112.

24. Poole D. Probabilistic Horn abduction and Bayesian networks // Artificial Intelligence, Volume 64, Numbers 1, 1993, P. 81-129.

25. Forbus K.D., de Kleer J. Building Problem Solver, The MIT Press, Cambridge, Massachusetts, London, England, 1993.

26. Doyle J. A Truth Maintenance System // Artificial Intelligence, 1979, Vol.12. P.231-272.

27. McAllester D. A Three-valued Truth Maintenance System / S.B. Thesis, Department of Electrical Engineering, MIT, Cambridge, MA, 1978.

28. McAllester D. An Outlook on Truth Maintenance. Artificial Intelligence Laboratory, AIM-551, MIT, Cambridge, MA, 1980.

29. McAllester D. Truth Maintenance // Proc. Of AAAI-90, 1990. P. 1109-1116.

30. Reiter R. A Logic for Default Reasoning // Artificial Intelligence, 1980, Vol. 13.P.81-132.

31. Castro J.L., Zurita J.M. A Generic ATMS // International Journal of Approximate Reasoning, 1996, Vol. 14, P.259-280.

32. Dechter R., Dechter A. Structure Driven Algorithms for Truth Maintenance // Artificial Intelligence, 1996, Vol. 82, P. 1-20.

33. Thompson C.A. Inductive learning for abductive diagnosis. Texas: the University of Texas at Austin, 1993. P. 53.

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

35. Вагин В.Н., Хотимчук К.Ю. Нахождение минимальных абдуктивных объяснений с помощью первичных импликат // Тр. 11й национальной конференции по искусственному интеллекту с международным участием (КИИ-2008. г. Дубна, Россия). 2008. Т. 2. Р. 345-355.

36. Вагин В.Н., Хотимчук К.Ю. Методы абдуктивного вывода в задачах планирования работы в сложных объектах // Известия РАН. Теория и системы управления, 2010, №5, с. 95-113.

37. Charniak Е., Shimony S.E. Cost-Based Abduction and MAP Explanation // Artificial Intelligence Journal, V. 66(2), 1994. P. 345-374.53 .NgH.T., MooneyRJ. On the Role of Coherence in Abductive Explanation // AAAI 1990. P. 337-342.

38. Финн B.K. Об одном варианте логики аргументации // Интеллектуальные системы и общество: сборник статей, изд.2-е, испр. и существ. Доп., Москва, : КомКнига, 2006. — 352с. 220-265.

39. Финн B.K. Правдоподобные выводы и правдоподобные рассуждения // Итоги науки и техники. Сер. Теория вероятностей. Математическая статистика. Теоретическая кибернетика. Т. 28. М. : ВИНИТИ, 1991. С. 3-84.

40. Финн В.К. Правдоподобные рассуждения в интеллектуальных системах типа ДСМ // Итоги науки и техники. Сер. Информатика. Т. 15. М.: ВИНИТИ, 1991. С. 54-101.

41. Dang P.M. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games // Artificial Intelligence Journal, V. 77(2), 1995. P.321-357.

42. Kakas A.C., Toni F. Computing argumentation in logic programming // Journal of Logic and Computation 1999. V. 9. P. 515-562.

43. Kowalski R., Kuhner D. Linear resolution with selection function // Artificial Intelligence. 1971. V. 2. P. 227-260.

44. Танаев B.C., Шкурба В.В. Введение в теорию расписаний. М.: Наука, 1975. С. 256.

45. Маппе A.S. On the Job Shop Scheduling Problem // Operations Research, 1960, 8(2): P. 219223.

46. 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: SpringerVerlag. 2002. V. 2407. P. 402-437.

47. Microsoft Corporation Microsoft Inductive User Interface Guidelines // RSDN Magazine #6, 2004.

48. Fikes R., Nilsson N. STRIPS: a new approach to the application of theorem proving to problem solving // Artificial Intelligence, 2: P. 189-208.ll.McDermott D. The Formal Semantics of Processes in PDDL // Proc. 1С APS Workshop on PDDL.

49. Ghallab M., Nau D.S. Automated Planning: Theory and Practice. Traverso, Paolo: Morgan Kaufmann, 2004. P.