Исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Аверин, Андрей Игоревич

• Аверин, Андрей Игоревич
• кандидат технических наук
• 2004

Оглавление диссертации кандидат технических наук Аверин, Андрей Игоревич

ВВЕДЕНИЕ.

ГЛАВА 1. ВИДЫ ПАРАЛЛЕЛИЗМА В ДЕДУКТИВНОМ ВЫВОДЕИ

1.1. Последовательные стратегии в доказательстве теорем.

1.2. Принципы распараллеливания

1.3. План поиска и параллелизм на уровне термов. ф, 1.4. План поиска и параллелизм на уровне дизъюнктов.

1.5. Параллелизм и план поиска на уровне поиска.

1.5.1. Параллельный поиск с использованием подхода «главный -подчиненный».

1.5.2. Параллельный поиск с использованием равноправных процессов.

1.5.3. Распределенный план поиска.

1.5.4 Применение стратегий распараллеливания к процедурам вывода.

ГЛАВА 2. УНИФИКАЦИЯ В ПРОЦЕДУРАХ ПАРАЛЛЕЛЬНОГО ДЕДУКТИВНОГО ВЫВОДА.

2.1. Структуры представления данных в системах дедуктивного вывода

1Ц 2.1.1. Определения.

2.1.2. Строковое представление терма и представление терма в виде дерева

2.1.3. DAG-представление термов.

2.1.4. Плоские термы.

2.1.5. Prolog-представление термов.

2.2. Структуры представления индексов для термов.:.

2.2.1. Позиционные строки (position strings).

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

2.2.1.2. Совместимость позиционных строк.

2.2.1.3. Характеристическое множество строк.ч

2.2.2. Индексация путей (path indexing).

2.2.2.1. Построение индекса.

2.2.2.2. Алгоритм нахождения множества унифицируемых термов.

2.2.2.3. Преимущества и недостатки подхода, основанного на использовании строковых путей.

2.2.3. Различающие деревья (discrimination trees).

2.2.3.1. Построение индекса.

2.2.3.2. Операции просмотра терма.

2.2.3.3. Алгоритм нахождения унифицируемых термов.

2.2.3.4. Преимущества и недостатки подхода, основанного на использовании различающих деревьев.

2.2.4. Деревья подстановок (substitution trees).

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

2.2.4.2. Построение индекса.

2.2.4.3. Нахождение унифицируемых термов.

2.2.5. Выводы к разделу 2.2.

2.3. Предлагаемый способ представления термов в логике предикатов первого порядка.

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

2.3.2. Установление связей между путями.

2.3.3 Решение задачи унификации.

2.3.4. Распараллеливание алгоритма унификации.

• Выводы к главе 2.

3. ПАРАЛЛЕЛИЗМ НА УРОВНЕ ДИЗЪЮНКТОВ. ПРОЦЕДУРА ВЫВОДА НА ГРАФАХ СВЯЗЕЙ.

3.1. Последовательная процедура доказательства методом графа связей

3.2. Стратегии поиска в графе связей.

3.3. Достоинства процедуры дедуктивного вывода на графе связей.

3.3.1. Проблема нахождения контрарной пары.

3.3.2. Проблема вычисления унификаторов для связи.

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

3.4. Параллельный вывод на графе связей.

3.4.1. Метод OR-параллельной резолюции.

3.4.2. DCDP-параллельный вывод.

3.4.3. AND-параллельная резолюция.

3.5. Модификация процедур параллельного вывода.

3.5.1. Принципы создания эвристических функций.

3.5.2 Эвристическая функция №1.

3.5.3 Эвристическая функция №2.

3.5.4. Эвристическая функция HI.Ill

3.5.4.1. Вычисление эвристической оценки дизъюнкта.

3.5.4.2. Вычисление эвристической оценки унификатора.

3.5.4.3. Вычисление эвристической оценки предикатной литеры.

3.5.4.4. Выбор коэффициентов.

3.5.4.5. Применение эвристической функции HI при решении задачи «Стимроллер».

Ф Выводы к главе 3.

4. АНАЛИЗ ЭФФЕКТИВНОСТИ ПРЕДСТАВЛЕННЫХ АЛГОРИТМОВ ВЫВОДА.

4.1 Основные понятия.

4.2 Сравнение эффективности на тестовой задаче «Стимроллер».

Выводы к главе 4.

Введение диссертации (часть автореферата) на тему «Исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах»

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

Использование графовых структур в качестве основы для построения процедур дедуктивного вывода является одним из способов повышения эффективности процесса вывода. Создан ряд алгоритмов дедуктивного вывода на графовых структурах [4, 9, 12, 40, 54, 62, 63]. Однако при решении задач практической сложности, которые характеризуются экспоненциальным ростом числа дизъюнктов, данные алгоритмы не всегда показывали удовлетворительные результаты, что привело к дальнейшим исследованиям в области повышения эффективности процедур вывода. Одним из способов повышения эффективности является распараллеливание процесса вывода.

В работах целого ряда авторов [3, 37, 44, 45, 46, 55] было показано, что использование параллелизма в алгоритмах вывода, основанных на графовых структурах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах является актуальной задачей.

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

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

1) Использование эффективного способа представления термов. Термы логики предикатов первого порядка являются основной структурой обработки в процедурах вывода, и их неэффективное представление ведет к неэффективной работе доказателя в целом.

2) Использование эффективного способа представления множества дизъюнктов. Множество дизъюнктов является объектом работы процедуры дедуктивного вывода, и выбор способа представления множества дизъюнктов крайне важен для создания эффективных процедур вывода.

3) Использование эффективной стратегии поиска. Резольвирование дизъюнктов является основной операцией в процедурах дедуктивного вывода, и неэффективный выбор дизъюнктов для резольвирования приводит к практической непригодности процедуры вывода.

4) Использование эффективной стратегии распараллеливания. Данную проблему необходимо решать совместно с проблемой выбора эффективной стратегии поиска. Выделяется три основных вида параллелизма: параллелизм на уровне термов, параллелизм на уровне дизъюнктов и параллелизм на уровне поиска (более подробная классификация видов параллелизма рассматривается в первой главе работы). При создании эффективных параллельных процедур вывода, необходимо уделять внимание всем трем разновидностям параллелизма.

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

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

Графы связей Ковальского являются основой для построения алгоритмов параллельного дедуктивного вывода. В настоящее время существует несколько способов распараллеливания процедур вывода на графе связей. В работе рассматриваются алгоритмы OR, DCDP и AND параллельного вывода на графах связей Ковальского. В данных алгоритмах реализован как параллелизм на уровне дизъюнктов (в случае OR и AND параллелизма), так и на уровне поиска (DCDP параллелизм). Для повышения эффективности процесса вывода предлагаются эвристические критерии оценки множества связей для параллельного резольвирования.

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

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

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

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

2. Метод построения множества связей для DCDP-параллельного вывода, позволяющий повысить эффективность DCDP-параллельного вывода.

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

4. Комплексный подход к распараллеливанию процесса вывода, объединяющий в себе OR-, AND- и DCDP- параллелизм.

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

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

Реализация результатов. Результаты диссертационной работы Аверина А.И. вошли в отчеты по НИР, выполняемым кафедрой ПМ по по грантам РФФИ № 99-01-00049, № 02-07-90042 по теме «Исследование и разработка инструментальных средств создания экспертных систем семиотического типа», а также в учебном процессе при изучении дисциплины «Математическая логика».

Произведена реализация представленного алгоритма вывода в рамках системы диагностики, представляющей собой надстройку над стандартной функциональностью интегрированной системы управления предприятием SAP R/3 и используемой для ускорения процесса диагностики и устранения неисправностей, возникающих во время работ по инсталляции, системной настройке и системному администрированию системы в НПО «Мекомп».

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 6-й, 7-ой, 8-ой, 9-ой и 10-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в МЭИ (ТУ) (г. Москва, 2000 - 2004 г.г.), на 4-ой международной летней школе-семинаре по искусственному интеллекту для студентов и аспирантов (Бра-славская школа) (Беларусь, г. Браслав, 1999 г.), на «Научных сессиях МИФИ» (г. Москва, 2000 - 2004 г.г.), на 7-й национальной конференции по искусственному интеллекту с международным участием КИИ'2000 (г. Переславль-Залесский, 2000 г.), международном форуме МФИ-2003 (Международные конференции «Информационные средства и технологии») (г. Москва, 2003), на Международной научно-технической конференции «Интеллектуальные системы» AIS'03 (Россия, п. Дивноморское, 2003 г.) и международной конференции JCKBSE - 2004 (Россия, г. Переславль-Залесский, 2004г., доклад на английском языке).

Рассмотрим структуру диссертационной работы подробнее.

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

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

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

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

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Аверин, Андрей Игоревич

Выводы к главе 4

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

2. Проведенный анализ показал, что применение эвристик позволило значительно повысить эффективность процедуры вывода. Продемонстрировано, что наиболее чувствительными к выбору эвристики являются процедуры ЭСЭР параллельного вывода.

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

Заключение

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

Произведенное в первой главе работы исследование стратегий распараллеливания показало, что существуют недостаточно изученные способы использования параллельных стратегий в дедуктивном выводе. Среди них можно отметить использование АМ> и (Ж- параллелизма для упорядочивающих стратегий, а также применение в дедуктивном выводе параллельной унификации. Это обусловлено объективными причинами. Если говорить о параллельной унификации и параллельном сопоставлении, то это объясняется структурой параллелизма на уровне термов, применение которого, без использования параллелизма на других уровнях, не приводит к заметному увеличению производительности процедуры вывода. Недостаточные исследования в области А№> и ОЙ.- параллелизма применительно к упорядочивающим стратегиям объясняются неудобством применения большинства упорядочивающих стратегий для одновременной обработки всех литер одного дизъюнкта (в случае АЬЮ-параллелизма) или одной литеры дизъюнкта (в случае (Ж-параллелизма).

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

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

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

Процедура вывода на графе связей служит основой для разработки алгоритмов параллельной резолюции. В работе представлены три стратегии распараллеливания (OR, AND и DCDP параллелизм). Для повышения эффективности стратегии поиска были разработаны эвристические функции выбора связи. Сравнение результатов работы процедуры вывода при использовании этих функций и без использования эвристических функций, показали заметное повышение эффективности процедуры вывода при использовании эвристических функций оценки связи.

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

Основными полученными результатами являются:

1) разработка комплексного подхода к решению задачи создания эффективной процедуры вывода, основанного на применении параллелизма на уровне термов и параллелизма на уровне дизъюнктов;

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

3) разработка алгоритма параллельной унификации, использующего представленную структуру представления термов и направленного на применение в процедурах параллельного вывода;

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

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

Список литературы диссертационного исследования кандидат технических наук Аверин, Андрей Игоревич, 2004 год

1. Аверин А.И., Вагин В.Н., Хамидулов М.К. Исследование алгоритмов параллельного вывода на задаче "Стимроллер" //Известия Академии Наук. Теория и системы управления, 2000. №5. - С. 92-100.

2. Аверин А.И., Вагин В.Н. Параллелизм в дедуктивном выводе на графовых структурах //Автоматика и телемеханика. №10. - 2001. - С. 54-64.

3. Вагин В.Н., Салапина Н.О. Система параллельного вывода с использованием графа связи // Известия Академии Наук. Теория и системы управления, №5,1998.-С.39-48.

4. Вагин В. Н. Дедукция и обобщение в системах принятия решений. — М.: Наука.-1988.-384с.

5. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, т.98, стр. 26-87,1968 г.

6. Astrachan O.L., Loveland D.W. METEORs: high performance theorem provers using model elimination/Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer AcademiaPublisher^l991^— pp. 31-60.

7. Avenhaus J., Denzinger J., Fuchs M. DISCOUNT: a system for distributed equational deduction. In Jieh Hsiang, editor, Proceedings of the 6th RTA, volume 914 of LNCS, Springer Verlag, 1995. pp. 397-402.

8. Baader F., Snyder W. Unification Theory //Handbook of Automated Reasoning/ A. Robinson, A. Voronkov eds. Elsevier Science. - 2001. - pp. 445532.

9. Barklund, J., Hagner, N., Wafin, M. Condition Graphs // Proceedings of the Fifth International Conference and Symposium on Logic Programming/ Kowalski, R. Bowen K.A. Seattle: The MIT Press. - 1988. - pp. 435-446

10. Bellia M., Occhuito M.E., Combinatorial lazy unification. Journal of Symbolic Computation. № 27 - 1999. - pp. 185-206.

11. Bellia M., Occhiuto M.E. New Bounds in Parallel Unification: Proc. of CSP'2002. pp. 53-64.

12. Bibel W. On Matrices with Connections // Journal of the ACM. № 28(4). -1981.- pp. 633-645.

13. Bibel W. Automated Theorem Proving. Friedr. Vieweg & Sohn, 2nd edition, 1987.-289 pp.

14. Bonacina M.P., Hsiang J. Parallelization of deduction strategies: an analytical study // Journal of Automated Reasoning. №13. — 1994. - pp. 1-33.

15. Bonacina M.P., Hsiang J. The Clause—Diffusion methodology for distributed deduction//Fundamenta Informaticae. №24. — 1995. - pp.177—207.

16. Bonacina M.P. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method // Journal of Symbolic Computation. — 1996. — №21.- pp. 507-522.

17. Bonacina M.P., Hsiang J., Zhang H. PSATO: a distributed propositional prover and its application to quasigroup problems//Journal of Symbolic Computation. №21.-1996. - pp. 543-560.

18. Bonacina M.P., Hsiang J. Ten years of parallel theorem proving: a perspective /Notes of the Workshop on Strategies m Automated Deduction, Federated Logic Conference/Gramlich B., Kirchner H., Pfenning F. eds. — Trento, Italy, 1999. pp. 3-15.

19. Bose S., Clarke E. M., Long D. E., Michaylov S. Parthenon: a parallel theorem prover for non-Horn clauses//Journal of Automated Reasoning, 8(2). — 1992.-pp. 153-182.

20. Ciprietti G., EC-expressions:linear unification and lazy narrowing, Thesis, Universita di Pisa, 1995.

21. Chaiyin G.J., Auslnder M.A., Chandra A.K., Cocke J., Hopkins M.E., Markstein P.W. Register allocation via coloring. // Computer Languages, 6:4757,1981.

22. Christian J. Fast Knuth-Bendix completion: A summary/ Proceedings of the 3rd International Conference on Rewriting Techniques and Applications./ N. Dershowitz, ed., Vol.355 of Lecture Notes in Computer Science, Springer Verlag, 1989.-pp. 551-555.

23. Christian J. Flatterais, discrimination nets, and fast term rewriting//Journal of Automated Reasoning. № 10(1). - 1993. - pp. 95-113.

24. Corny S.E., Macintosh D.J., Meyer D.J. DARES: A Distributed Automated Reasoning System: Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990). AAAI Press/MIT Press, 1990. - pp. 78-85.

25. Corbin J., Bidoit M. A Rehabilitation of Robinson's Unification Algorithm /Information Processing 83/R.E.A. Mason (ed.). Elsevier Science Publisher B.V (North-Holland), IFIP, 1983. - pp. 909-914.

26. Davis M., Putnam H. A computing procedure for quantification theory // Journal of the ACM. -№7. 1960. - pp. 201-215.

27. Denzinger J., Lind J. Twlib: a library for distributed search applications/Proceedings of ICS-96/Chu-Sing Yang, editor, 1996 pp. 101-108.

28. Dwork C., Kannelakis P.C., Mitchell J.C. On the sequential nature of unification// J. Logic Programming. № 1. - 1984. - pp.35-50

29. N. Eisinger. Completeness, Confluence, and Related Properties of Clause Graph Resolution//Research Notes in Artificial Intelligence. Pitman Ltd., London, 1991.

30. Fuchs D. Requirement-based cooperative theorem proving/Proceedings of the 6th JELIA/ Jurgen Dix, Luis Farinas del Cerro, Ulrich Furbach, editors,, volume 1489 ofLNAI, Springer, 1998.-pp. 139-153.

31. Graf P., Substitution tree indexing /Rewriting Techniques and Applications/ J. Hsiang, ed., Vol. 914 of Lecture Notes in Computer Science, 1995. pp. 117-131.

32. Graf P., Term Indexing, Vol. 1053 of Lecture Notes in Computer Science, Springer Verlag.

33. Hillenbrand Th., Buch A., Vogt R., Löchner B., Waldmeister: HighPerformance Equational Deduction//Journal of Automated Reasoning. № 18(2). -1997. - pp. 265-270.

34. Hornung G., Knapp A., Knapp U. A parallel connection graph proof procedure / J. H. Siekmann, ed // German Workshop on Artificial Intelligence, Springer-Verlag, Berlin. 1981. pp. 160-167.

35. Huet G., Resolution d'équations dans les language d'ordre 1,2,.,w, Ph.D dissertation, Univ. de Paris VII, France, 1976.

36. Kerber M., Choi S. The semantic clause graph procedure// In proceedings of the CADE-17 Workshop on Model Computation-Principles, Algorithms, and Applications/ P. Baumgartner et al., eds., Pittsburgh, PA, USA. June 2000. pp. 2937.

37. Kirchner C., Viry P. Implementing parallel rewriting /Parallelization in Infërence Systems / Bertram Fronhofer and GrahamWrightson, Eds. № 590, LNAI. Springer-Verlag. 1990. - pp. 123-138

38. Knight K. Unification: a multidisciplinary survey //ACM Computing Surveys. №21. - 1989. -pp. 93—124

39. Kowalski.R. A Proof Procedure Using Connection Graphs. // Journal of the ACM, 22(4), October 1975, p.595-599.

40. Letz R., Schumann J., Bayerl S., Bibel W. SETHEO: A high-performance theorem prover//Journal of Automated Reasoning. №8(2). — 1992.- pp. 183-212.

41. Loganantharaj R., Mueller R.A. Parallel Theorem Proving with Connection Graphs// CADE 1986. pp. 337-352

42. Loganantharaj R. Parallel Link Resolution of Connection Graph Refutation and Its Implementation //International Conference on Parallel Processing (ICPP '87),

43. University Park, PA, USA, August 1987. Pennsylvania State Univ. Press, 1987-pp.154-157

44. Loganantharaj R., Liou A.A. Parallel Deduction of Connection Graphs // Advances in Logic Programming and Automated Reasoning /R.W. Wilkerson ed. -Ablex, 1990.-pp. 1-48.

45. R.Loganantharaj and A. A. Liou, Experience with Extended DC Parallelism of Connection Graphs //International Journal of Mini and Microcomputers.- vol 16(2).- 1994. pp. 33-47.

46. Loganantharaj R., Liou A.A.Experience with Or-Parallelism of Connection Graphs Proceedings of the 19th annual conference on Computer Science, ACM -1991.-pp. 381-390

47. Lusk E.L., McCune W., Slaney J. ROO: a parallel theorem prover /Proceedings of the 11th CADE/ Deepak Kapur, editor, volume 607 of LNAI, Springer Verlag, 1992.-pp. 731-734.

48. Martelli A., Montanari U. An Efficient Unification Algorithm//ACM Trans, on Progr. Lang, and Sys., 4, 2, 1982.- pp. 259-282.

49. McCune W. Experiments with discrimination-tree indexing and path indexing for term retrieval//Journal of Automated Reasoning. № 9(2). - 1992. - pp. 147167.

50. McCune W. Otter 3.0 reference manual and guide, Technical Report 94/6, MCS Division, Argonne National Laboratory, 1994.-57 pp.

51. De Nivelle H., Datastructures for Resolution pjieiapoHHbiH pecypc. — 2000.- http://www.mpi-sb.mpg.de/~nivelle/software/bliksem/

52. Nieuwenhuis R., Rivero J., Vallejo M. //The Barcelona prcver, Journal of Automated Reasoning. №18(2). - pp. 171-176.

53. Ohlbach H. Abstraction tree indexing for terms: in proceedings of the 9th European Conference on Artificial Intelligence. Pitman Publishing, London, 1990.- pp. 479-484.

54. Ohlbach H. J., Siekmann J.H. The Markgraf Karl Refutation Procedure //Computional Logic Essays in Honor of Alan Robinson / Jean Louis Lassez and GordonPlotkin(ed.).-MITPress.- 1991.- ISBN0-262-12156-5.- pp. 41-112

55. Powers D. M. V. Parallel and Efficient Implementation of the Compartmentalized Connection Graph Proof Procedure// Parallelism in Inference Systems. Springer-Verlag, 1991. - pp. 210-233.

56. Ramesh R., Ramakrishnan I., Warren D. 1995., Automata-driven indexing of Prolog clauses// Journal ofLogic Programming. № 23(2). — 1995.- pp.151-202.

57. Robinson J. A machine-oriented logic based on the resolution principle// Journal of the ACM. №12(1). - 1965. - pp. 23-41.

58. Robinson J. New directions in mechanical theorem proving // Information Processing 68, Proceedings of IFIP Congress 1968, Edinburgh, UK, 510 August 1968, Volume 1 Mathematics, Software - 1968. - pp. 63-69.

59. Schulz, S. E A Brainiac Theorem Prover // Journal of AI Communications № 15(2/3).- 2002.-pp.111-126.

60. Schumann J., Letz R. PARTHEO: a high-performance parallel theorem prover/ Proceedings of the 10th CADE/Mark E. Stickel, editor, volume 449 of LNAI, Springer Verlag, 1990.-pp. 28-39.

61. Sekar R., Ramakrishnan I.V., Voronkov A. Term indexing /Handbook of Automated Reasoning/A. Voronkov, A.Robinson eds, Elsiever Science Publishers, 2001.-pp. 1853-1954.

62. Sickel S. A search technique for clause interconnectivity graphs // IEEE Transactions on Computers, G25(8). 1976. — pp. 823- 835.

63. Shostak R.E. Refutation graphs //Artificial Intelligence.- №7. pp.51-64.

64. Stickel M. E. Schubert's steamroller problem: Formulations and solutions // Journal of Automated Reasoning, 2.- 1986. pp. 89-101.

65. Stickel M. E. The path-indexing method for indexing terms, Technical Report 473, SRI International, Menlo Park, California, USA 1989.

66. Vitter J.S., Simons R.A. Parallel algorithms for unification and other complete problems in P: in ACM'84 Conference Proceedings (San Francisco, California, Oct. 8-10). ACM, New York, 1984.

67. Vitter, J. S. and Simons, R. A. (1986). New classes for parallel complexity: A study of unification and other complete problems for P/IEEE Transactions on Computers, C-35(5):23.- pp.403-418.

68. Voronkov A. The Anatomy of Vampyre, Implementing BottomUp Procedures with Code Trees//Journal of Automated Reasoning.- №15. 1995. - pp. 237-265.

69. Weidenbach C., Gaede B., Rock G. SPASS & FLOTTERProceedings of the 13th CADE/ McRobbie M., Slaney J. editors, volume 1104 ofLNAI, Springer, 1996.-pp. 141-145.

70. Weidenbach, C., 1999, Combining Superposition, Sorts and Splitting /A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, Elsevier,2001. pp. 1965-2013.

71. Werner S., Siekmann J.H. Completeness and Soundness of the Connection Graph Proof. AISB/GI (ECAI). 1978. - pp. 340-344.

72. Wos L. Note on McCune Discrimination trees//Journal of Automated Reasoning. №9 (2). - 1992. - pp. 145-146.1. ОГ- -Г/39-/ т. 2.

73. Московский энергетический институт (технический университет)1. На правах рукописи1. Аверин Андрей Игоревич

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

75. Специальность 05.13.11 Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей

76. Диссертация на соискание ученой степеникандидата технических наук