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

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

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

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

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

А В Т О Р Е Ф Е Р А Т

диссертации на соискание ученой степени

кандидата технических наук

Москва – 2011

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

Научный руководитель: лауреат премии президента РФ в области образования, доктор технических наук, профессор

Вадим Николаевич Вагин

Официальные оппоненты: доктор физико-математических наук, профессор

Геннадий Семёнович Осипов;

кандидат физико-математических наук, ведущий научный сотрудник

Алексей Николаевич Аверкин

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

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

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

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

Автореферат разослан «____» ___________ 2011 г.

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

диссертационного совета Д 212.157.01

кандидат технических наук,

доцент

М.В. Фомина

Общая характеристика работы

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

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

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

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

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

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

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

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

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

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

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

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

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

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’11 (Украина, г. Гурзуф, 2011 г.), МНТК-2010 (г. Москва, 2010 г.), “Повышение эффективности электрического хозяйства потребителей в условиях ресурсных ограничений. Материалы Всероссийской научно-практической конференции с международным участием”.

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

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

Содержание работы

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

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

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

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

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

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

Пусть – формула ЛП1П. Конъюнкт =h1h2…hk, где h1,h2,…,hk H, назовем абдуктивным объяснением относительно Т, если:

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

Конъюнкт '=h1h2…hk, где h1,h2,…,hk H, назовем минимальным абдуктивным объяснением относительно Т, если:

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

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

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

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

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

• ' – <L, Ф>-импликата формулы ;
• для всех <L, Ф>-импликат '' формулы выполняется {'''}{'''}.

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

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

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

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

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

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

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

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

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

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

Начало.

Шаг 1.	Создаем дизъюнкт clause = observed,
Шаг 2.	Обращаемся к процедуре SOLSolve с параметрами clause, clauses, Lit(clause)Lit(clauses), где Lit(clause) / Lit(clauses) – множество литер, встречающихся в дизъюнкте/дизъюнктах. Результат выполнения процедуры – множество implicates.
Шаг 3.	Для каждого дизъюнкта implicate из implicates создаем конъюнкт explanation = implicate. Добавляем explanation к result.

Конец.

Алгоритм SOLSolve.

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

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

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

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

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

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

Начало.

Шаг 1.		Образование начального центрального структурного дизъюнкта topClause = <<>, <Lit(clause)>>. В качестве базы правил нужно взять имеющуюся базу правил, объединенную с clause.
Шаг 2.		Найти все первичные импликаты с помощью выполнения шага 4.
Шаг 3.		Выбрать из полученного на предыдущем шаге множества неповторяющиеся дизъюнкты и записать их в result. Конец.
	Шаг 4.	Поиск множества первичных импликат для поступающего на вход узла (структурного дизъюнкта). Возвращается множество дизъюнктов, которые являются первичными импликатами дизъюнкта, образованного из необрамленных литер родительского структурного дизъюнкта topClause, и где резольвировать можно только по литерам из второй компоненты topClause. Для узла, в котором произошел вызов данного шага, выполнить шаг 5, получив множество дизъюнктов s1, и шаг 6, получив множество дизъюнктов s2. Возвратить s1 s2.
	Шаг 5.	Рассматриваем l – первую литеру из второй компоненты topClause. Если l lit, то осуществить перенос (правило Skip) литеры из второй компоненты topClause в первую, иначе Конец. Осуществить редукцию (шаг 7). Если вторая компонента topClause пуста, то возвратить дизъюнкт, полученный из литер левой компоненты topClause. Иначе: продолжить рекурсивный поиск для topClause – выполнить шаг 4.
	Шаг 6.	Осуществить резолюцию (правило Resolve) первой литеры из второй компоненты со всевозможными дизъюнктами из базы правил. Пусть входной структурный дизъюнкт на данном этапе имеет вид <<a1, a2, … ak>, <l, l1, … ln>>, а подходящее правило rule = l’1, …,l’t, ¬l, l’t+1, l’p, тогда резольвента примет вид <<a1, a2, … ak>, < l’1, …,l’t, l’t+1, l’p, [l], l1, … ln>>. При выборе подходящего правила нужно соблюдать условие lit(rule) framed({l, l1, … ln}) =. Кроме того, унификация не должна изменить аргументы литеры l. Осуществить редукцию (шаг 7) всех полученных резольвент и с ними перейти к шагу 4.
	Шаг 7.	Редукция поступающего на вход структурного дизъюнкта (правило Reduce). Если в l1, … ln литера l встречается дважды, то удаляется ее самое левое вхождение. Получаем l11, l12, … l1n1. Если какая-либо литера из a1, a2, … ak совпадает с некоторыми литерами из l11, l12, … l1n1, то удаляем из последнего множества эти литеры. Получаем l21, l22, … l2n2. Удалить все обрамленные литеры из <l21, l22, …, l2n2>, которым не предшествует обрамленная литера.

Конец.

Разработан эвристический метод для алгоритма ImpAA, который позволяет получить заметное ускорение для решения ряда абдуктивных задач. Данный эвристический метод использует выбор начального порядка литер в исходных дизъюнктах в целях уменьшения числа шагов алгоритма SOL-резолюции. Метод заключается в упорядочивании литер в дизъюнкте по возрастанию функции Rank(r, RuleBase), действующей на декартовом произведении множества литер и множества множеств дизъюнктов во множество целых чисел и определённой ниже, где r – литера, RuleBase – множество дизъюнктов. Ранг литеры r в RuleBase определяется следующим образом. Находятся дизъюнкты d1, … dn, содержащие ¬r, i{1, …, n} di RuleBase. Тогда

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

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

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

Разработаны модификации алгоритмов ImpAA и ImpAA\H – ImpAA\M и ImpAA\M\H соответственно. В данных модификациях разрешены абдуктивно недопустимые унификации, которые не разрешены в ImpAA и ImpAA\H. Данные модификации позволяют использовать разработанные алгоритмы в решении задачи составления расписания.

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

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

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

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

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

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

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

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

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

Рис. 1

Рис. 2

Рис. 3

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

,

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

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

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

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

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

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

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

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

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

Начало.

Шаг 1.	Если все дизъюнкты из clauses – хорновские дизъюнкты, то переход к шагу 2. Иначе ОШИБКА, Сообщение “Все дизъюнкты должны быть хорновскими!”, Конец.
Шаг 2.	Вычислить множество , где – множество всевозможных факторов дизъюнктов из clauses.
Шаг 3.	Пусть O1,O2... – это литеры observed. Создать вершину GOAL (операция добавления вершины в ATMS) и добавить к ней обоснование . nO1, nO2… – добавленные таким образом новые вершины (операция добавления обоснования в ATMS).
Шаг 4.	Выполнить процедуру Assume с параметрами nOi, Oi для i=1,2.. (операция добавления предположения в ATMS)
Шаг 5.	Выполнить процедуру ProcessNode с параметрами GOAL, extendedClauses, GOAL,.
Шаг 6.	Вычислить метку на вершине GOAL: обращение к процедуре ComputeLabel с параметром 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.	Резолюция по 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 – это логическая теория первого порядка, представляющая условия и ограничения предметной области, – формула логики первого порядка, содержащая константы 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.

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

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

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

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

Алгоритм ReArrangeLiteras

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

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

Требуется:

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

Начало.

Шаг 1.	Найти в ruleBase все дизъюнкты, содержащие хотя бы одну *-литеру. Обозначим их множество как StarClauses. Пусть N – число таких дизъюнктов. Рассмотрим i – номер текущего дизъюнкта. Присвоим i = 1.
Шаг 2.	Если , то Конец. Иначе рассмотрим clause – i-й дизъюнкт в StarClauses. Пусть литера lit – *-литера в этом дизъюнкте. Найти все дизъюнкты в ruleBase, в которых lit встречается без отрицания. Обозначим найденное множество как S. Пусть NS – число таких дизъюнктов. Рассмотрим j – номер текущего дизъюнкта. Присвоим j = 1.
Шаг 3.	Если , то присваиваем i = i + 1 и переход к шагу 2. Иначе рассмотрим clause – j-й дизъюнкт в S. Выполнить процедуру AnalyzeMath с параметрами clause, ruleBase. Выполнить процедуру AnalyzeArgumentCover с параметром clause. Присваиваем j = j + 1 и переход к шагу 3

Конец.

Алгоритм AnalyzeMath

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

clause – дизъюнкт.

Требуется:

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

Начало.

Шаг 1.	Пусть N – число отрицательных литер в дизъюнкте clause. Рассмотрим i – номер текущей литеры. Присвоим i = 1.
Шаг 2.	Если , то Конец. Иначе рассмотрим lit – i-ю литеру в clause. Если это математическая литера, то поменять её местами с N-й литерой в дизъюнкте clause, присвоить N = N – 1 и к шагу 2. Иначе присвоить i = i + 1 и к шагу 2.

Конец.

Алгоритм AnalyzeArgumentCover

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

clause – дизъюнкт вида , где – литеры, не являющиеся математическими, – литеры, являющиеся математическими.

Требуется:

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

Начало.

Шаг 1.	Пусть Arguments – множество рассматриваемых аргументов. Присвоим . Рассмотрим i – текущая позиция литеры. Присвоим i = 1.
Шаг 2.	Если , то Конец. Иначе найти такую литеру litera среди , что . Присвоить . Поменять местами в дизъюнкте clause литеры litera и . Присвоить i = i + 1 и к шагу 2.

Конец.

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

Рис. 4

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

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

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

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

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

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

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

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

Рис. 5

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

Основные результаты работы

1. Проведено исследование подходов к организации абдуктивного вывода и исследование методов абдуктивного вывода. Выбран подход на уровне логики, работающий с логическими теориями первого порядка. Разработан алгоритм абдуктивного вывода ImpAA с использованием первичных импликат. Разработана модификация алгоритма ImpAA. Разработан эвристический метод для алгоритма ImpAA. Показано, что применение эвристики позволяет повысить эффективность алгоритма ImpAA благодаря сокращению пространства поиска.
2. Выполнено исследование и анализ систем поддержки истинности. Особое внимание уделено системам поддержки истинности, основанным на предположениях, ключевым достоинством которых является сохранение выводов, что приводит к кэшированию промежуточных результатов, в результате чего нет необходимости в повторных вычислениях. Благодаря своим характеристикам, система поддержки истинности, основанная на предположениях (ATMS), выбрана в качестве основы для построения абдуктивного алгоритма.
3. На основе ATMS разработан алгоритм абдуктивного вывода ABAA, осуществляющий составление расписания в сложных технических объектах. Продемонстрировано, как использование ATMS позволяет вводить предположения об истинности гипотез, одновременно строить множество решений задачи составления расписания и для каждого решения сохранять информацию об обосновывающих его предположениях, а также отвергать неверные гипотезы и ошибочные решения.
4. Разработана модификация алгоритма абдуктивного вывода на основе системы поддержки истинности для решения задачи составления расписания, связанная с введением специальных литер, используемых для подтверждения или опровержения вывода.
5. Разработан эвристический метод для алгоритма абдуктивного вывода, использующего систему поддержки истинности на основе предположений. Показано, что применение данного метода позволяет повысить эффективность алгоритма ABAA благодаря сокращению пространства поиска.
6. С использованием результатов данной работы на основе ATMS разработан и реализован программный комплекс, осуществляющий составление расписания работ в сложных технических объектах. Программный комплекс тестировался на примере задачи составления расписаний для технических работ.

Список работ, опубликованных по теме диссертации

1. Вагин В.Н., Хотимчук К.Ю. Методы абдуктивного вывода в задачах планирования работы в сложных объектах // Известия РАН. Теория и системы управления, 2010, №5, с. 95-113.
2. Вагин В.Н., Хотимчук К.Ю. Абдуктивный вывод versus дедукция // Программные продукты и системы, 2010, №4, с. 106-110.
3. Вагин В.Н., Хотимчук К.Ю. Абдукция в задачах планирования работ в сложных объектах // Искусственный интеллект и принятие решений. – М.: Ленанд, 2011. – Т.1 с.3-13.
4. Хотимчук К.Ю. Исследование методов нахождения минимальных абдуктивных объяснений // Радиоэлектроника, Электротехника и Энергетика. Тринадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. Т.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. Вагин В.Н., Хотимчук К.Ю. Нахождение минимальных абдуктивных объяснений с помощью первичных импликат // Тр. 11й национальной конференции по искусственному интеллекту с международным участием (КИИ-2008. г. Дубна, Россия). 2008. Т. 2. P. 345-355.
8. Хотимчук К.Ю. Решение задачи планирования работы сложных технических объектов с помощью алгоритмов абдуктивного вывода // Повышение эффективности электрического хозяйства потребителей в условиях ресурсных ограничений. Материалы Всероссийской научно-практической конференции с международным участием (Москва, 16 – 20 ноября 2009 г.) / Под общ. Ред. Б. И. Кудрина и Ю. В. Матюниной. В 2-ч т. М.: Технетика, 2009. Том II – 258 с. с. 174 – 176.
9. Хотимчук К.Ю. Применение алгоритмов абдуктивного вывода в решении задачи планирования работы сложных технических объектов // Радиоэлектроника, Электротехника и Энергетика. Шестнадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. Т.I. М.: Издательский дом МЭИ, 2010. – 492с. с. 386 – 387.
10. Вагин В.Н., Хотимчук К.Ю. Алгоритм абдуктивного вывода с использованием систем поддержки истинности на основе предположений // Двенадцатая национальная конференция по искусственному интеллекту с международным участием КИИ-2010 (20-24 сентября 2010 г., г. Тверь, Россия): Труды конференции. Т. 1. - М.: Физматлит, 2010. - 392 с. с. 73 – 82.
11. Хотимчук К.Ю. Абдуктивный вывод с использованием систем поддержки истинности на основе предположений // Труды XVI Международной научно-технической конференции "Информационные средства и технологии". 19 – 21 октября 2010г., Москва. В 3 томах. Т.2. М.:Издательский дом МЭИ. 359 с. с. 242 – 249.
12. Хотимчук К.Ю. Алгоритм абдуктивного вывода для решения задачи планирования работы сложных технических объектов // Радиоэлектроника, Электротехника и Энергетика. Семнадцатая Междунар. Науч.-техн. Конф. Студентов и аспирантов: Тез. Докл. В 3 т. Т.I. М.: Издательский дом МЭИ, 2011. – 488с. с. 385 – 386.

Свидетельство о государственной регистрации программы для ЭВМ “Fast Abductive Solver” №2010614887 (27 июня 2010 г.).