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

• Автор: Аверин, Андрей Игоревич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Москва
• Количество страниц: 139 с. : ил. + Прил. (с.140-200:ил.)

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

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

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

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

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

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

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

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

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

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

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

Щ 2.1.1. Определения.
2.1.2. Строковое представление терма и представление терма в виде дерева
2.1.3. представление термов.
2.1.4. Плоские термы
2.1.5. представление термов
2.2. Структуры представления индексов для термов.
2.2.1. Позиционные строки ii i
2.2.1.1. Основные определения.
2.2.1.2. Совместимость позиционных строк
2.2.1.3. Характеристическое множество строк.ч
2.2.2. Индексация путей ixi.
2.2.2.1. Построение индекса
2.2.2.2. Алгоритм нахождения множества унифицируемых термов
2.2.2.3. Преимущества и недостатки подхода, основанного на использовании строковых путей.
2 Различающие деревья iiii .
2.2.3.1. Построение индекса.
2.2.3.2. Операции просмотра терма.
2.2.3.3. Алгоритм нахождения унифицируемых термов.
2.2.3.4. Преимущества и недостатки подхода, основанного на использовании различающих деревьев
2.2.4. Деревья подстановок ii .
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. Распараллеливание алгоритма унификации.
Выводы к главе
3. ПАРАЛЛЕЛИЗМ НА УРОВНЕ ДИЗЪЮНКТОВ. ПРОЦЕДУРА ВЫВОДА НА ГРАФАХ СВЯЗЕЙ.
3.1. Последовательная I 1роцедура доказательства методом графа связей
3.2. Стратегии поиска в графе связей
3.3. Достоинства процедуры дедуктивного вывода на графе связей
3.3.1. Проблема нахождения контрарной пары
3.3.2. Проблема вычисления унификаторов для связи.
3.3.3 Проблема удаления дизъюнктов, которые не могут быть использованы в дальнейшем пространстве поиска.
3.4. Параллельный вывод на графе связей.
3.4.1. Метод Жпараллельной резолюции
3.4.2. ОСОРпараллельный вывод
3.4.3. АЬГОпараллельная резолюция
3.5. Модификация процедур параллельного вывода.
3.5.1. Принципы создания эвристических функций.
3.5.2 Эвристическая функция 1.
3.5.3 Эвристическая функция 2.
3.5.4. Эвристическая функция Н
3.5.4.1. Вычисление эвристической оценки дизъюнкта
3.5.4.2. Вычисление эвристической оценки унификатора
3.5.4.3. Вычисление эвристической оценки предикатной литеры
3.5.4.4. Выбор коэффициентов
3.5.4.5. Применение эвристической функции Н1 при решении задачи
Стимроллер
ВЫВОДЫ К ГЛАВЕ 3.
4. АНАЛИЗ ЭФФЕКТИВНОСТИ ПРЕДСТАВЛЕННЫХ АЛГОРИТМОВ ВЫВОДА
4.1 Основные понятия.
4.2 Сравнение эффективности на тестовой задаче Стимроллер
Выводы к главе 4.
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ


Упорядочивающие стратегии обычно применяют поиск первый лучший с использованием различных эвристических функций. Так как они аккумулируют все сгенерированные неизбыточные данные, эти стратегии не являются чувствительными к порядку вывода , то есть, если система вывода является полной, а план поиска справедливым, порядок выводов не влияет на полноту. Эти стратегии не нуждаются в операции бэктрекинга, и
все их действия могут стать в дальнейшем одной из попыток вывода. В качестве примера, рассмотрим типичный управляющий алгоритм, который используется в доказателях, применяющих стратегии, основанные на упорядочивании например . В этих алгоритмах рассматривается множество дизъюнктов, которые могут быть выбраны как бы граница поиска и список дизъюнктов уже выбранных. Предположим, что план поиска осуществляет поиск в глубину, следовательно список дизъюнктов, которые могут быть выбраны, может быть реализованы в виде стека. Таким образом, даже при использовании поиска в глубину, этот вид стратегии не нуждается в бэктрекинге, так как при выборе дизъюнкта р, который не порождает потомков, достаточно просто переместить этот дизъюнкт в список уже выбранных и продолжить работу алгоритма выбрав другой дизъюнкт. Стратегии, основанные на сведении к подцелям, обычно используют планы поиска в глубину с бэктрекингом и итеративным углублением. Однако подобные планы поиска требуют от стратегии порождения и сохранения в памяти множества попыток доказательства линейных дедукций или таблиц, которые представляют собой границу поиска. Поиск в глубину с итеративным углублением, как правило, является более предпочтительным, так как он требует сохранения только одной попытки вывода в данный момент времени, в то время как остальные будут рассмотрены во время выполнения операции бэктрекинга. Если ни один шаг доказательства не является применимым к текущему линейному дедуктивному выводу или таблице, план поиска выполняет операцию возврата бэктрекинга. Нами были рассмотрены основные стратегии, использующиеся в последовательных процедурах дедуктивного вывода. Перейдем к рассмотрению основных принципов распараллеливания последовательных процедур. В рассмотренной ниже классификации основным критерием является различие между параллелизмом на уровне термов, параллелизмом на уровне дизъюнктов и параллелизмом на уровне поиска. Выделяется три вида параллелизма параллелизм на уровне термов, параллелизм на уровне дизъюнктов и параллелизм на уровне поиска. В параллелизме на уровне термов, данные, которые обрабатываются параллельно, являются подвыражениями формулы например термами или литерами. Под формулой, в данном случае, подразумевается основная единица обработки в системе вывода. В случае доказательства методом резолюции это дизъюнкты. Операции, которые выполняются параллельно, в свою очередь, являются подзадачами шага вывода. Таким образом, распараллеливание производится как бы ниже уровня вывода. Примерами подобного параллелизма являются параллельное сопоставление i, параллельная унификация и параллельная перезапись термов. В параллелизме на уровне дизъюнктов, данными, обрабатываемыми параллельно, являются формулы, а параллельными операциями являются выводы, так что распараллеливание производится на уровне вывода. Методы доказательства теорем, использующие параллельные выводы внутри одного процесса поиска например, параллельно выполняющиеся шаги резолюции, относятся к этой категории параллелизма. Смысл использования подобного распараллеливания заключается в ускорении процесса вывода путем выполнения нескольких выводов на одном шаге. В параллелизме на уровне поиска, множественные дедуктивные процессы производят поиск параллельно, до того, как один из них не найдет доказательство. Каждый процесс исполняет стратегию, производит вывод и строит свое собственное множество данных. Параллелизм на уровне термов, дизъюнктов и на уровне поиска представляют собой примеры мелко, средне и крупнозернистого параллелизма для дедуктивного вывода. Рассмотрим таблицу 2. Границу между параллелизмом на уровне дизъюнктов и параллелизмом на уровне термов не всегда можно четко обозначить.