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

• Автор: Зо Мьо Хтет
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Москва
• Количество страниц: 137 с. : ил.

Оглавление

УСЛОВНЫЙ АЛФАВИТ.

ВВЕДЕНИЕ.

ГЛАВА 1. ОБЗОР МЕТОДОВ ВЫВОДА ДЛЯ СИСТЕМ ПРИНЯТИЯ РЕШЕНИЙ.

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

1.2.РИНЦИПЫ распараллеливания

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

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

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

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

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

1.5.3. Распределенный план поиска
ГЛАВА 2. ВЫВОД НА АНАЛИТИЧЕСКИХ ТАБЛИЦАХ.
2.1. Метод аналитических таблиц для пропозициональной логики
2.1.1. Непротиворечивость и полнота метода аналитических таблиц для пропозициональной логики.
2.1.2. Повышение эффективности вывода на аналитических таблицах.
2.1.3. Последовательный метод аналитических таблиц для пропозициональной логики.
2.2. Метод аналитических таблиц для логики предикатов первого ПОРЯДКА.
2.2.1 Стратегия выбора формул
2.2.2. Метод полного перебора
2.3. Алгоритм метода полного перебора БТМ
ВБ1ВОДЫ.
ГЛАВА 3. МЕТОД АНАЛИТИЧЕСКИХ ТАБЛИЦ С ФИКТИВНЫМИ ПЕРЕМЕННЫМИ
3.1. Подстановки и их свойства.
3.2. Согласование
3.3. Композиция подстановок
3.4. Алгоритм согласования.
3.5. Введение гранулы и теней
3.6. Работа с множественными конфликтами подстановок.
3.7. Эвристики, улучшающие процедуру опровержения
3.8. Последовательный метод с фиктивными переменными БТМ
3.9. Параллельный метод с фиктивными переменными РТМ,
ВЫВОДЫ.
ГЛАВА 4. МОДИФИКАЦИИ ПАРАЛЛЕЛЬНОГО МЕТОДА
АНАЛИ ТИЧЕСКИХ ТАБЛИЦ С ФИКТИВНЫМИ ПЕРЕМЕННЫМИ
4.1. Параллельный метод полного перебора, использующий стратегию поиска в ширину РШеМ
4.2. Параллельный метод полного перебора, использующий стратегию поиска в глубину РТМей
4.3. Параллельный метод с фиктивными переменными, использующий стратегию поиска в ширину РТМ,УМ
4.4. Параллельный метод с фиктивными переменными, использующий стратегию поиска в глубин у РТМ1
4.5. Программная реализация разработанных методов и их сравнение
4.5.1. Структура программного комплекса РТМ
4.5.2.Гестирование методов
4.5.3. Сравнение метода полного перебора с методом с фиктивными переменными
4.5.4. Сравнение последовательного метода с фиктивными переменными с параллельным методом, использующим стратегии поиска в глубину и в ширину.
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ


Как было показано в [6, 7], особое внимание следует уделить применяемой стратегии распараллеливания (под понятием стратегии распараллеливания в дедуктивном выводе понимается управляющая компонента параллельных дедуктивных методов, которая, с помощью стратегий поиска, производит поиск решения). В настоящее время создан ряд процедур дедуктивного вывода, наиболее известными среди которых являются метод резолюций Робинсона [8], метод обратного вывода Маслова [9], процедура вывода с использованием аналитических таблиц [3], алгоритм Дэвиса-Патнема [] и их модификации. Несмотря на существенные различия этих алгоритмов, ко всем из них применимы различные стратегии распараллеливания. В главе рассмотрены основные виды стратегий распараллеливания и возможность их использования для распараллеливания последовательных алгоритмов дедуктивного вывода. Из упомянутых нами типов параллелизма главное внимание будет уделено параллелизму на уровне распределенного поиска. Ключевой фактор в классификации методов с параллельным поиском заключается в дифференциации и комбинировании активности дедуктивных процессов. Рассматриваемый нами метод аналитических таблиц имеет одну и ту же систему вывода (так называемую гомогенную систему) и осуществляет параллелизм на уровне распределенного поиска. Говоря о распараллеливании последовательных алгоритмов дедуктивного вывода стоит отметить, что, вообще говоря, распараллеливание не сводится к простому одновременному выполнению шагов последовательного алгоритма. Таким образом, если последовательная стратегия поиска не является оптимальной, при использовании параллельного поиска мы можем получить сверхлинейиое ускорение. Примером этого может служить распределенный доказатель Рееп-тсс/, который представляет собой распараллеливание доказателя Е()Р [7|. При запуске Реегэ-тсс/ на теореме «Роббинсовские алгебры являются булевыми» (которая была ранее доказана с помощью Е()Р), было показано сверхлинейиое ускорение, тогда как все остальные факторы (используемое аппаратное обеспечение, версия Е(^)Р, системы вывода) оставались неизменными. Перед тем как перейти к анализу параллельных стратегий, следует рассмотреть основные понятия и терминологию, используемые при рассмотрении последовательных стратегий в дедуктивном выводе. На рис. Рис. Ковальского []. Эти стратегии называют упорядочивающими, так как они работают с множеством дизъюнктов, используя состоятельное упорядочивание на этом множестве и (возможно) удаляя дизъюнкты, которые или больше других дизъюнктов (согласно введенному упорядочиванию), или являются следствиями других дизъюнктов. Подобные стратегии могут или добавлять дизъюнкты во множество дизъюнктов (для выводов расширения - таких как резолюция или парамодуляция), или удалять дизъюнкты (заменять их на меньшие) - для выводов сокращения (например, для перезаписи термов). Состояние вывода содержит множество дизъюнктов, которые были получены и сохранены (то есть, не были удалены в результате операции сокращения). Так как это множество обычно приобретает большие размеры, используются различные способы индексирования для извлечения элементов из множества. Стратегии, которые используют только расширяющие правила, или которые применяюг сокращающие правила только для нормализации сгенерированных данных относительно существующего множества (подобный подход называют прямым сокращением), называются расширяющими стратегиями. Стратегии, использующие как прямое, так и обратное сокращение (то есть нормализацию данных, уже находящихся во множестве, относительно сгенерированных данных), называются сокращающими стратегиями. Упорядочивающие стратегии, вообще говоря, не являются чувствительными к цели, хотя семантические стратегии или стратегии множества поддержки используют семантику для отображения некоторой чувствительности к цели. Стратегии, основанные на сведении к подцелям, включают в себя стратегии, основанные на принципе линейной резолюции, удалении моделей (modeI elimination) и табличных методах, которые будут подробно разобраны во второй главе работы.