Введение
ГЛАВА 1. Виды параллелизма в дедуктивном выводе 11
1.1. Последовательные стратегии в доказательстве теорем 12
1.2. Принципы распараллеливания 17
1.3. План поиска и параллелизм на уровне термов 21
1.4. План поиска и параллелизм на уровне дизъюнктов 22
1.5. Параллелизм и план поиска на уровне поиска 25
1.5.1. Параллельный поиск с использованием подхода «главный -подчиненный» 25
1.5.2. Параллельный поиск с использованием равноправных процессов.. 27
1.5.3. Распределенный план поиска 29
1.5.4 Применение стратегий распараллеливания к процедурам вывода... 30
ГЛАВА 2. Унификация в процедурах параллельного дедуктивного вывода 34
2.1. Структуры представления данных в системах дедуктивного вывода 36
2.1.1. Определения 36
2.1.2. Строковое представление терма и представление терма в виде дерева 38
2.1.3. DAG-представление термов 39
2.1.4. Плоские термы 40
2.1.5. Prolog-представление термов 41
2.2. Структуры представления индексов для термов ; 42
2.2.1. Позиционные строки (position strings) 44
2.2.1.1. Основные определения 44
2.2.1.2. Совместимость позиционных строк.. 45
2.2.1.3. Характеристическое множество строк. 45
2.2.2. Индексация путей (path indexing) 47
2.2.2.1. Построение индекса „ 47
2.2.2.2. Алгоритм нахождения множества унифицируемых термов .49
2.2.2.3. Преимущества и недостатки подхода, основанного на использовании строковых путей. 50
2.2.3. Различающие деревья (discrimination trees) 50
2.2.3.1. Построение индекса 51
2.2.3.2. Операции просмотра терма 53
2.2.3.3. Алгоритм нахождения унифицируемых термов 54
2.2.3.4. Преимущества и недостатки подхода, основанного на использовании различающих деревьев... 55
2.2.4. Деревья подстановок (substitution trees) 56
2.2.4. L Основные определения 56
2.2.4.2. Построение индекса 57
2.2.4.3. Нахождение унифицируемых термов 58
2.2.5. Выводы к разделу 2.2 60
2.3. Предлагаемый способ представления термов в логиісе предикатов первого порядка 61
2.3.1. Основные определения 61
2.3.2. Установление связей между путями 63
2.3.3 Решение задачи унификации 69
2.3.4. Распараллеливание алгоритма унификации 74
Выводы к главе 2 82
ГЛАВА 3. Параллелизм на уровне дизъюнктов. процедура вывода на графах связей. 84
3.1. Последовательная процедура доказательства методом графа связей 85
3.2. Стратегии поиска в графе связей 91
3.3. Достоинства процедуры дедуктивного вывода на графе связей 94
3.3.1. Проблема нахождения контрарной пары 94
3.3.2. Проблема вычисления унификаторов для связи 94
3.3.3 Проблема удаления дизъюнктов, которые не могут быть
использованы в дальнейшем пространстве поиска 95
3.4. Параллельный вывод на графе связей 95
3.4.1. Метод OR-параллельной резолюции 95
3.4.2. DCDP-параллельный вывод 97
3.4.3. AND-параллельная резолюция 102
3.5. Модификация процедур параллельного вывода 106
3.5.1. Принципы создания эвристических функций 106
3.5.2 Эвристическая функция №1 108
3.5.3 Эвристическая функция №2 109
3.5.4.Эвристическая функция HI Ill
3.5.4.1. Вычисление эвристической оценки дизъюнкта... 112
3.5.4.2. Вычисление эвристической оценки унификатора 113
3.5.4.3. Вычисление эвристической оценки предикатной литеры 113
3.5.4.4. Выбор коэффициентов 113
3.5.4.5. Применение эвристической функции HI при решении задачи «Стимроллер» 115
Выводы к главе 3 120
ГЛАВА 4. Анализ эффективности представленных алгоритмов вывода 121
4.1 Основные понятия 121
4.2 Сравнение эффективности на тестовой задаче «стимроллер» 123
Выводы к главе 4 129
Заключение 130
Список литературы.
