автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Исследование и разработка параллельных методов вывода на аналитических таблицах

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

/ 'О '

Зо Мьо Хтет

ИССЛЕДОВАНИЕ И РАЗРАБОТКА ПАРАЛЛЕЛЬНЫХ МЕТОДОВ ВЫВОДА НА АНАЛИТИЧЕСКИХ ТАБЛИЦАХ

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

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

1 1 ОК Т 2012

Москва-2012

005053002

Работа выполнена на кафедре Прикладной математики Институт; автоматики и вычислительной техники НИУ «МЭИ».

Научный руководитель:

Лауреат премии Президента РФ в облает» образования, доктор технических наук, профессор Вадим Николаевич Вагин

Официальные оппоненты:

доктор технических наук, профессор

Дзегелёнок Игорь Игоревич

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

Ведущая организация: Российский научно-исследовательский

институт информационных технологий и систем автоматизированного проектирования

(ФГБУ РосНИИ ИТ и АП), г.Москва

Защита состоится 12 октября 2012 г. в 16 час. 00 мин. на заседании диссертационного совета Д 212.157.01 при НИУ «МЭИ» по адресу: 111250, Москва, Красноказарменная ул., 17 (ауд. Г 306).

С диссертацией можно ознакомиться в библиотеке НИУ «МЭИ».

Автореферат разослан ^4» сентября 2012 г.

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

диссертационного совета Д 212.157.01 кандидат технических наук, доцент

Фомина М.В.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы исследований. В настоящее время алгоритмы дедуктивного вывода находят широкое применение в системах принятия решений, дедуктивных базах данных, информационно-поисковых системах. В числе других областей использования дедуктивного вывода можно также назвать верификацию спецификаций компьютерного оборудования (процедуры дедуктивного вывода использовались, например, при верификации процессоров компании AMD), проверку корректности систем безопасности, анализ корректности протоколов передачи данных.

Значительный вклад в разработку и исследование алгоритмов дедуртивного вывода внесли Д. Хинтикка (Jaakko Hintikka), Э.Бет (Evert W. Beth), Д. Правитц (Dag Prawitz), Дж. Робинсон (J.A. Robinson), Р.Смаллиан (R.V. Smullan), Мелвин Фитганг (Melvin Fitting), Стив Ривс (Steve Reeves), M. Дэвис (М. Davis), X. Патнэм (Н. Putnam), Р. Ковальски (R. Kowalski), В. Бибель (W. Bibel), Л. Вое (L. Wos), П. Гилмор (P. Gilmore), Д. Лавлэнд (D. Loveland), Н. Эйзингер (N. Eisinger) , С.Ю. Маслов, В.К.Финн, В.Н. Вагин.

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

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

В работах Р. Джонсона (Robert Johnson) было показано, что использование параллелизма методов вывода, основанных на аналитических таблицах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка параллельных методов вывода на аналитических таблицах является актуальной задачей.

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

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

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

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

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

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

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

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

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

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

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

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

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

Практическая значимость результатов диссертационной работы заключается в создании программной системы, в рамках которой реализованы алгоритмы последовательного и параллельного вывода на аналитических таблицах, использующие две стратегии поиска: "в ширину" и "в глубину". Программы реализованы в среде Microsoft Visual Studio 2010 на языке С#. Реализованные алгоритмы были также использованы для решения тестовой задачи «Стимроллер», а также в учебном процессе при изучении дисциплин " Математическая логика " и " Экспертные системы " (на английском языке).

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных "Информационные технологии в науке, образовании, телекоммуникации и бизнесе", IT + S&E'

2012. Украина, Крым, Ялта-Гурзуф, 25.05 - 04. 06. 2012, на 17-ой и 18-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в НИУ «МЭИ» (г. Москва, 2010 - 2012 г.г.).

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 5 печатных работах, включая 2 статьи в изданиях из перечня ВАК.

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

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

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

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

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

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

В параллелизме на уровне дизъюнктов данными, над которыми производится параллельная обработка, являются формулы некоторого языка. В системах, основанных на языке Пролог, имеет место АЖ)-параллелизм и СЖ-параллелизм.

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

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

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

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

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

формулами, представленными в конъюнктивной нормальной форме (КНФ), то метод аналитических таблиц оперирует с формулами, представленными в дизъюнктивной нормальной форме (ДНФ). Представлены четыре правила расширения таблицы, два из которых относятся к логике высказываний (а, Р), а два - для логики предикатов первого порядка (у, 5).

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

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

В работе дан алгоритм последовательного метода таблиц для пропозициональной логики (БТМр) и алгоритм последовательного метода полного перебора (8ТМе) для логики предикатов первого порядка.

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

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

Метод полного перебора (STMe) конструирует таблицу сверху- вниз слева направо, немедленно замыкая путь, на котором найдена контрарная пара формул. В каждой точке расщепления генерируются два пути pi и Р2. (32 помещается в стек, в то время как STMe продолжает вычислять pi, пока замыкание не будет найдено. Все дальнейшие незамкнутые пути, получившиеся в результате расщеплений, помещаются в стек перед Р2. Таким образом, проверка таблицы сверху вниз, слева направо обеспечена. В STMe новая копия любой у-формулы может быть добавлена к пути для каждой константы. Система квот вводится для преодоления проблем, вызванных применением у-правила к единичной формуле бесконечное множество раз. Пусть имеется универсально квантифицированная формула на ветви таблицы и переменная-ограничитель и. Тогда универсально квантифицированная формула может быть использована максимум п раз для введения новых имен на пути, после чего она отмечается как использованная.

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

Мы будем обозначать фиктивные переменные как dx или dx, где * -положительное целое число.

Описывается метод, который параллельно пытается построить подстановки, способные замкнуть таблицу. Отметим, что в таблице могут существовать пути, которые не требуют унификации, т.е. когда контрарная пара F и -iF не нуждается в унификации. Если на пути существуют две формулы, которые замыкают его без унификации, то это называется константным замыканием. Однако, если на пути присутствуют формулы типа F (а, л) и -nF(y, b), где аиЬ-константы, х и у - фиктивные переменные, то эти формулы необходимо

унифицировать, т.е. применить к ним подстановку {<х, Ь>, <у, а>} и получить контрарную пару F(a, b) и -iF(a, tí).

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

Две или более редукций являются противоречивыми, если они пытаются связать одну и ту же фиктивную переменную с различными константами. Противоречивая подстановка - это подстановка, содержащая одну или более пар противоречивых редукций. Рассмотрим два пути Р\, Р2 таблицы Т, где Р\ может быть замкнут после унификации формул F(a, х) и -iF(у, tí), и Р2 может быть замкнут после унификации формул G(а, х) и G(y, с). Р\ требует подстановку {<5с, Ъ>, <у, я>} для замыкания, в то время как Р2 требует {<х,с>, <у,а>}. Очевидно, что эти подстановки противоречивы. Поэтому замыкание путей с такими подстановками несостоятельно и невозможно.

Возможное унифицирующее множество (П-множество) П для подтаблицы Т' таблицы Т содержит редукции, требующиеся для замыкания всех путей в Т'. Каждое П-множество состоит из непротиворечивых идемпотентных подстановок. Необходимое унифицирующее множество (N-множество) N является множеством из П-множеств.

В работе представлен процесс согласования. Во время унификации конструируются подстановки и осуществляется согласование различными таблицами. Каждое N-множество содержит множество П-множеств, каждое из которых унифицирует, по крайней мере, одну пару контрарных формул на всех путях конкретной таблицы. Операция согласования объединяет N-множества Ni и N2, соответствующие паре таблиц, выводя единственное N-множество, содержащее П-множества, которые замыкают обе таблицы. Унификация N-множеств называется согласованием.

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

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

Рис 1. иллюстрирует работу с аналитической таблицей с фиктивными переменными на 3 узлах РО, Р1 и Р2.

Прокомментируем полученное решение. Первые 14 шагов проходят в соответствии с последовательным алгоритмом метода аналитических таблиц с фиктивными переменными. В универсальных формулах с кванторами Ух или —i3jc осуществляются подстановки фиктивных переменных вместо х,у и z, т.е. х = di, х = d2, х = d3, у = d4 и z - d5. Затем в экзистенциональных формулах с

t

кванторами Эх или —Мх реализуются подстановки констант вместо переменных, т.е. у = а (для Цс11у)), у = Ь{ для в {<12у)) и х = с (для Н(дг^)).

После этого идёт разветвление. Применение результатов композиции подстановок даёт следующее: {{Р(с/7,<я), -^{йЗ,а)},{С{с12,Ь}, -^(¿¿З.Ь)}}. Отсюда N1= {{«11Ш>},{«121аЗ>}}.

В отличие от левого пути правый путь ещё раз разветвляется. Имеем:{{Р(<*7,л), -,Р(я,</5)},{ С(с12,Ь), -Х}(М5)}}, N2 = {{<сШа>,<Л5/а>}, {<с121Ь>,<451Ь>}}.{{-Щс44), Щс1345)}}, N3 = {{<с13/с>у<с!4№>}}.

Применяем операцию согласования, которая объединяет N2 и N3, получая Ы-множество N4.

N4= {{<£111а>,<451а>}, {<й21Ъ>,<451Ъ>}}® {{<й31с>,<4Ш5>}}.

Процесс согласования И-множеств, как уже упоминалось, требует создания всех перестановок пар П-множеств из двух ^множеств, причём несогласованные подстановки или экземпляры любых П-множеств из одного и того же М-множества, будут исключены.

УдгЗу УхЗу СЗСдг.у), ЧхЭу (Цху) V 0(лг,у) — Чг(Р(у^) V — Н(^))) 1= ЧхВу Щх^).

1. -[УхЗу Щ*,?) & ЧхЭу в(ху) & ЧхВу (Т(ху) V С(х^) -> V в(у,*) —Щх^))) —УхЭу Щх^)]

2.4x3(1) З.ЧхЗуС(ху) (1)

(1)

5.-УхЗуН(1,у) (1)

6. Зу ¥(с11у) ' (2)

I.3уС{с12,у) (3)

8. Ву (В^Зу) УО(.<13У) V 0(уЛ —Н(<ВД)) (4)

9. Р(<Н,а) (6)

10. С(с12,Ь) (7)

II. ¥(с13,а) №{<13,Ъ) -ЛСДа?) V <3(ад ->Н(<Я ,г)) (8)

12. -*3у Н(с^) (5)

13. Щс,с14) (12)

14. Я(<13,а) ЧСУЗ,Ъ) -*(?(а,с1Г> V в(М.5) -»Н(<«,</5)) (11)

15. ^((¿3,а) VI

16. ~ЩЗ,а) (15) 17-0{с!3,Ь) (15)

□

И

16'. V С(М5)) (1

17'. -¥(а,с15) (16")

{<4ШЗ>} [9:16] {<42!<13>) [10:17]

{<<12МЗ>} [10:17] 18'. -Ч}(Ь,</.5) (16') {^3/с>,<^4Ш>}[13,:16'

□

□

{«¡11а>,«Н1а>)[9:17'] {<421Ъ>,<451Ь>}[\0 :18'] Здесь Р0,Р1,Р2 - номер узла выполняющего вычисления.

= { {<4ИО,<й21Ь>,<431с>,<44Л»,<451Ь>}, {<411а>,<А21ь>,<Л31с>,<с141а>,<451а>)}.

Рис.1. Пример параллельного метода с фиктивными переменными.

N4= {{<dl/a>,<d5/a>}, {<d3/c>,<d4/d5>}} U {{<d2/b>,<d5/b>}, {<d3/c>,<d4/d5>}}= { {<dlla>,<d3lc>,<d4la>,<d5la>}, {<d2/b>,<d3/c>,<d4/b>,<d5/b>}}. Теперь выполняем согласование между левой и правой ветвями: N1 = {{<dl/d3>}, {<d2/d3>}};

N4= {{<dlla>, <d3/c>,<d4/a>,<d5/a>},{<d2/b>,<d3/c>,<d4/b>,<d5/b>}}. N,0N4= {{<dl!d3>},{<dl/a>, <d3/c>,<d4/a>,<d5/a>}} U {{<dl/d3>}, {<d2/b>, <d3/c>,<d4/b>,<d5/b>}} U { {<d2/d3>}, {■<dlla>, <d3lc>,<d4la>,<d5la>} } {{<d2/d3>}, {<d2/b>, <d3!c>,<d4/b>,<d5/b>}} = = {{<dlla>, <d3la>.<d3lc>.<d4/a>.<d5/a> 1 {<dl/c>,<d2/b>, <d3!c>,<d4/b>,<d5/b>} {<dlla>,<d2lc><d3lc><d4la>,<d5la>} (<d2/b>.<d3/b>. <d3lc>.<d4/b>.<d5lb>)} В итоговом согласовании первое и четвертое N-множества являются противоречивыми (подчеркнуто), поэтому их следует исключить. N^r = {{<dl/c>,<d2/b>,<d3/c>,<d4/b>,<d5/b>}, {<dlla>,<62lc>,<d3lc>,<d4la>,<d5la>}}.

Предложено использовать подход Ривса (Reeves) к затенению, когда конфликтующие подстановки обнаруживаются. Ривс добавляет экземпляр у-формулы, содержащей новую переменную к таблице, только если константное замыкание не смогло выполниться с текущим множеством фиктивных переменных и констант. Для метода с фиктивными переменными, затенение заменяет процесс, принятый переборным методом для сохранения полноты. Затенение происходит после согласования. Переборный метод добавляет экземпляр для каждой универсально квантифицированной формулы к концу пути, всякий раз, когда вводится новая константа. Если различные пути требуют различных подстановок для определенной фиктивной переменной, тогда тень добавляется к каждому пути с требуемой константой (или новой фиктивной переменной), подставленной вместо фиктивной переменной, которая вовлечена в конфликтующую подстановку. Например, имеем четыре пути PI, Р2, РЗ и Р4, которые требуют подстановки ({*, а), {х, Ь), {х, с} и {х, d}) соответственно, тогда гранула х найдена (назовем её S) и результирующие пути Р2 U {S{<x, b>}}, РЗ U {S{<x, с>}}, и Р4 U {S{<x, й>}} расширены и произведен поиск на замыкание. Отметим, что мы позволим Р1 замкнуться с подстановкой {<х, а>} и затеним только остающееся дерево.

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

Разработаны следующие параллельные методы аналитических таблиц для логики предикатов первого порядка :

- параллельный метод полного перебора, использующий стратегию поиска "в ширину" (РТМеМ);

и

- параллельный метод полного перебора, использующий стратегию поиска "в глубину" (РТМ^и);

- параллельный метод с фиктивными переменными, использующий стратегию поиска "в ширину" (РТМ^);

- параллельный метод с фиктивными переменными, использующий стратегию поиска "в глубину". (РТМ<ш);

РТМем расширяет все открытые ветви таблицы параллельно до тех пор, пока ограничитель порождения не будет превышен. Вне (за пределом) этого момента подтаблицы конструируются локально. Расширение "в ширину" с отдельным порождением процессов стремится распределить пути вокруг доступных процессоров.

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

РТМ«и применяет ту же самую политику порождения процессов для табличного разбиения, что и РТМеМ. Однако, как только счётчик порождения становится равным вычисленному значению ограничителя порождения процессов, РТМ^ переходит в режим "в глубину", и "слева-направо".

Параллельный метод с фиктивными переменными, использующий стратегию поиска "в ширину" (РТМ^м) расширяет все пути параллельно, распределяя пути тем же самым образом, что и РТМем. Это расширение происходит асинхронно до тех пор, пока не потребуется унификация. Унификация требуется, когда путь завершен (полностью расширен) и константное замыкание потерпело неудачу. Во время унификации строятся подстановки, и осуществляется согласование различными таблицами (желательно смежными). Этот процесс требует синхронизации. Если И-множество для всей таблицы не может быть сконструировано, выбирается М-множество, которое замыкает больше всего путей. Эти пути замыкаются, и начинается затенение для оставшихся путей. Затенение может происходить асинхронно до тех пор, пока снова не понадобится унификация. На рис.2 приведен пример параллельного метода с фиктивными переменными, использующий стратегию "в ширину".

(1) -,3*(ЗД &(}(*))

(2) ульвдуос^вд)

(3) э^рм)уал-(ом)

(4) %г(-,(С!(х)УВД)У8(д:))

(5)-,Эх(Р(*)УВД)

(6) З^РИ) [3] (7) З-Т«}«) [3]

(8) Р(а) [6] (8') 0(6) [7]

(9) -.(ВД) & ВД» [5] (9') -ЧБУг) & ЪШ) [1]

(Ю) ^Р^^ИэГ^^^'^^Ж^) [9] (10')-ОД р'Т^'^ОП^СгС^Р']

I I

[8:10 ;М/я}] (12) -ВД) V СК</4) V ад) [2] (12') -<<2№) V ад» V [4] [8':1Г;{<ВД]

(13) -,*(<!,) [12] (14) 0(11,) [12] (15) ад) [12]

□ | □

[8;13;{<^"}] (16)-,(БУ5)&0№))[1] [11:15; {¿Л}] Р1

(13') -,(0(4) V ад» [12'] (14')5(<У [12']

(17) -ад) [16]

I

(19) -.(Оад V ад» V Э(с/в) [4]

(18)-,Ч№) [16]

[14:18;{ад>]

(15') -,<3№) [13']

(16') -А№)[13'] □

[8М5-;{ОД]

(20) -,(0(<*б) V ад» [19] (21) вад [19]

(22) ЧОШ [20] □

(23) -лад [20] [17:21;{^^6}]

□

[14:22; ДОЛ

Рх - (х -номер процессора)

„ = {<¿1 1а>, <¿1/Ь>, «уъ>, «Ь!а>, <4ь!а>, <(4/д>}.

Рис.2. Пример параллельного метода с фиктивными переменными для логики предикатов первого порядка, использующий стратегию "в ширину" (с использованием 2 ядер).

(1) -эх^М & <3(*»

(2) У^РМУОМУЯМ)

(3) Эл<Р(лЗ) V Элг(<ЗМ)

(4) УхМ0МУВД)У8М)

(5)-,Э*<РС>г)&1ВД)

С6) э<РМ) [3]

(8) Р(а)[б]

(9)-п(Р№)&ВД)) [5] 1.Р1

(7)ЭХ(0М)[3] (12) <3№)[7] (13) -.(8№)&<5№»[1]

(10)-,Р№) [9] □

[8:10

2Л

(22)-,Р(<?4)[21]

(11)-,ВД) [9]

(14)-,8№)[13]

(21) -,ру4) V <з«о V ад) [22] (16) -,(ош V ад» V ей) [4]

1.Р1

(15) -Чад [13]

О

[12:15;№/г>>]

2.Р2

(23) <5(4) [21]

(24) ад) [21]

(17) -<<3№) V ад) [16] (18) вй) [16]

[8;22;{^а)] (25) & ()(</,)) [1] [11:24; {¿,/ОД]

З.Р1

(26) -^(¿э) [25]

(27) -пОШ [25]

(19) [17]

(20) -,ад3) [17] □

[12:19;{ед]

[14:18;

(28) -,(С2№ V ад» V [4] [23:27;{¿М)]

(29) -п(<3№> V ад6» [28] (30) ЭШ [28]

(31) -,<}«,) [29] □

(32) -Сад) [29] [26:30;{^4)]

□

[23:31;{й,/ед

У.Рх - ( У = число прохождений процессора; х « номер процессора)

Кто1 = {<¿1 1а>, <Лг!Ъ>, <с1г1Ъ>, <с?5/а>, <Лб/а>).

Рис.3. Пример параллельного метода с фиктивными переменньши предикатов первого порядка, использующий стратегию "в использованием 2 ядер).

для логики глубину"(с

PTMidd следует другой схеме параллелизма чем та, которая была в PTMrfM. Стек неполных задач (незамкнутые пути) поддерживается централизовано. Сеть из я процессоров дает возможность РТМш исследовать п путей параллельно. При каждом раздвоении создаются два пути. Вычисление одного пути продолжается, в то время как другой путь помещается в стек Tasks (задачи) активных открытых путей вместе с уникальным идентификатором и данными управления. Если процессор "master" (главный) осуществляет хранение Tasks, то расширение и замыкание путей выполняется процессорами "slave" (подчиненный). Когда процессор становится свободным, находящийся в стеке путь повторно активируется. Каждый из п активированных путей решается параллельно и одновременно происходит согласование. Когда происходит замыкание пути, берется новый путь из Tasks. Процесс продолжается до тех пор, пока Tasks не станет пустым, и никакой другой процессор не работает на незамкнутом пути. Тогда в этот момент таблица объявляется замкнутой. Если какой - либо процессор находит открытый путь, все вычисления заканчиваются сообщением из центрального пункта распределения сообщений (процессор "master").

На рис.3 приведен пример параллельного метода с фиктивными переменными, использующий стратегию "в глубину".

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

В работе программно реализованы описанные параллельные методы вывода, приводятся результаты сравнения работ параллельных методов дедуктивного вывода. Сравнения производятся на тестовых задачах (3 легкие задачи, проблема Гилмора и задача «Стимроллер») .

Легкие задачи

1) 3x[C(x)&{Vy(P(y) -*L(x,y))}], Vx(C(x) ->{Vy(H(y) -> -iL(x,y))}) l=Vy(P(y)->-,H(y))

2) Vx3y[F(x,y)], Vx3y[G(x,y)],

Vx3y[{F(x,y) v G(x,y)} ->{Vz{{F(y,z) v G(y,z)} -*H(x,z)}}] l=Vx3yH(x,y)

>

I

3) -dx(S(x) & Q(x)), Vx(-iP(x) v Q(x) v R(x)), 3x(P(x)) v Эх (Q(x)), VxKQ(x)vR(x))vS(x)) l= 3x(P(x) v R(x))

Проблемы посложнее

4) Проблема Гилмора (Gilmore problem)

H Vx3y[[{F(y) ->G(y)} <-»F(x)]&[{F(y)->H(y)}<-»G(x)]&[[{F(y)->G(y)} -Ш(у)] oH(x)]]->Vz {F(z)&G(z)&H(z)}

5) Задача "Стимроллер" 3xW(x),

3xF(x), 3xB(x), 3xC(x), 3xS(x),

Vx(W(x) ->A(x)), Vx(F(x) ->A(x)), Vx(B(x) ->A(x)), Vx(C(x) ->A(x)), Vx(S(x)-*A(x)), 3xG(x),

Vx(G(x) ->P(x)),

VxVyVzVv[[{A(x)&P(y)}-»E(x,y)]v[{A(z)&P(v)&M(z,x)&E(z,v)} ->E(x,z)]], [VxVy[{C(x)&B(y)} ->M(x,y)]]& VxVy[{S(x)&B(y)} ->M(x,y)], VxVy[{B(x)&F(y)} ->M(x,y)], VxVy[{F(x)&W(y)} ->M(x,y)],

VxVy[{W(x)&F(y)} -»-,E(x,y)].

VxVy[{W(x)&G(y)} -тЕ(х,у)], VxVy[{B(x)&C(y)} -»E(x,y)], VxVy[{B(x)&S(y)} -iE(x,y)], Vx3y[C(x) ->{P(y)&E(x,y)}], Vx3y[S(x)-»{P(y)&E(x,y)}] l=3x3y[{A(x)&A(y)}&[{E(x,y)}&3z{G(z)&E(y,z)}]]

Условия эксперимента: Windows 7 Professional.

Processor: Intel (R) Core (TM) 2 Quad CPU Q 8300 @2.50 GHz 2.50 GHz. Installed memory (RAM) 4.00 GB (3.25 GB usable)

Задача 1.

_Таблица. 1.

Количество РТМ.м РТМ.Л, РШа,, РТИи,

процессоров (секунды) (секунды) (секунды) (секунды)

1 0,0725197 0,1427895 0,2794677 0,3583594

2 0,0437943 0,1754636 0,2350575 0,3016914

3 0,0832202 0,2022179 0,2263397 0,3402666

4 0,0428872 0,2266498 0,3400607 0,3224897

а.4

ра

Количество процессоров

РТМ(еЫ) РТМ(е(«) РТМ((1Ьс[) РТМ(йс1с1)

Рис.4.Результаты для задачи 1.

Задача 2.

Таблица.2.

Количество РТМ.м РТМ«и РТМ^м РТМлй

процессоров (секунды) (секунды) (секунды) (секунды)

1 0,7119277 2,5705974 3,6946656 4,3583594

2 0,8037942 2,0187224 2,8899844 3,9016914

3 1,5032202 2,9725663 3,1684812 3,3402666

4 1,6029728 3,05746163 3,3306021 3,3224897

Количество процессоров

-РТМ(еИ

-ртм(еаа) -ртм(сша) -ртм(ааа)

Рис.5.Результаты для задачи 2.

Задача 3.

Таблица.З.

Количество РТМ,м РТМ*и РТМ^м РТМли

процессоров (секунды) (секунды) (секунды) (секунды)

1 1,3942722 1,9888753 2,5168543 3,6140641

2 1,2747713 0,8674326 2,2937031 3,0785893

3 1,0032787 1,5236543 1,8846743 2,5698716

4 1,4555136 1,1543278 1,7849632 2,3890925

—РТМ(еЬс1) -Ш-РТМ(ес1а) РТМ(аЬс1)

ствопроцессоров

Рис.б.Результаты для задачи 3. Проблема Гилмора

Таблица.4.

Количество РТМ,м РТМ.^ РТМм РТМли

процессоров (секунды) (секунды) (секунды) (секунды)

1 70,3954222 56,8865531 24,7752692 22,7325742

2 61,3982791 40,5974336 21,2426667 19,9661091

3 54,0022787 45,9221543 18,6692931 14,4931026

4 53,4555136 37,9983258 16,4895347 14,171059

РТМ(еМ)

ртмма)

PTM(dbd) ртм(айс))

чествопроцессоров

Рис.7.Результаты для проблемы Гилмора. Задача "Стимроллер"

Таблица.5.

Количество РТМ.Ы РТМ„и РТМ« ртми,

процессоров (секунды) (секунды) (секунды) (секунды)

1 неудача неудача 140,802268 72,6130082

2 неудача неудача 125,8395874 58,8022019

3 • неудача неудача 110,138551 48,8022019

4 . . неудача неудача 107,2166469 48,29333

Рис.8.Результаты для задачи "Стимроллер".

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

Метод полного перебора лучше справляется с задачами малой сложности, но плохо справляется со сложными задачами. Так, для лёгких задач 1,2,3 (см. первую строку (1 процессор) табл. 1, 2, 3) методы полного перебора (РТМеМ и РТМ«и) тратят меньше времени, чем методы с фиктивными переменными (РТМ^м и РТМ<ш).(см. также рис.4,5,6)

Метод с фиктивными переменными, наоборот, лучше справляется со средними и сложными задачами (сравним результаты, данные в таблицах 4 и 5 и рис.7), даже если метод потребует связь между процессами. Недостатки, связанные с этой связью, перевешивают многократное применение у-экземпляров. Так, для задачи 4 (проблема Гилмора) в таблице 4 методы с фиктивными переменными ( РТМ^^ и РТМ^уу) тратят меньше времени чем методы полного перебора ( РТМсМ и РТМ^). Что касается задачи "Стимроллер" (см. табл. 5) алгоритмы полного перебора потерпели неудачу при её решении (слишком большой перебор), в то время как алгоритмы с фиктивными переменными ( РТМ<*ми РТЙш) успешно её решили (см. также рис. 8).

I

I

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

Отметим также, что при решении задач 4 (проблема Гилмора) и 5 (задача "Стимроллер") мы видим, что с ростом числа вершин положительный эффект от применения параллелизма будет сказываться по сравнению с методом полного перебора ввиду ускорения процесса вычислений. Хотя сам параллельный метод с фиктивными переменными не учитывает стоимость связи между процессами, он предлагает более эффективное распределение загрузки процессоров, нежели метод полного перебора.

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

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

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

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

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

4) Для метода унификаций предложен более эффективный способ работы с подстановками.

5) Предложены эвристики, повышающие эффективность вывода, как для пропозициональной логики, так и для логики предикатов первого порядка.

6) Разработаны последовательные и параллельные методы с фиктивными переменными, использующие стратегии "в глубину" и "в ширину" для аналитических таблиц, и разработаны алгоритмы, реализующие эти методы.

7) Программно реализованы параллельные алгоритмы полного перебора, использующие стратегии поиска "в ширину" (РТМеМ) и "в глубину" (РТМ^), а также параллельные алгоритмы с фиктивными переменными, использующие те же самые стратегии поиска (РТМам и РТМ«ш).

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

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

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Вагин В.Н, Зо Мьо Хтет. Параллельный вывод в методе аналитических таблиц, Программные продукты и системы, № 3(95),

2011, с. 8-13.

2. Вагин В.Н, Зо Мьо Хтет. Модификации параллельного метода аналитических таблиц. Журнал Открытое образование. № 1(90) 2012. с. 60-70.

3. Вагин В.Н, Зо Мьо Хтет. О параллельном методе аналитических таблиц с фиктивными переменными //Матералы 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных "Информационные технологии в науке, образовании, телекоммуникации и бизнесе", IT + S&E' 2012. Украина, Крым, Ялта-Гурзуф 25.05 - 04. 06.

2012, с. 102-105.

4. Вагин В.Н, Зо Мьо Хтет. Стратегии вывода в параллельном методе аналитических таблиц //Радиоэлеюроника, электротехника и энергетика. Восемнадцатая международная научно-техническая конференция студентов и аспирантов; Тезисы докладов. В 4 т. — Т.2. - М.: НИУ «МЭИ», 2012. -С.42-43.

5. Вагин В.Н, Зо Мьо Хтет. Параллельный вывод в методе аналитических таблиц с фиктивными переменными //Радиоэлектроника, электротехника и энергетика. Восемнадцатая международная научно-техническая конференция студентов и аспирантов; Тезисы докладов. В 4 т. - Т.2. - М.: НИУ «МЭИ», 2012. - С. 44.

Подписано в печать^/»D9<№(%1~Зак.Л90 тир. fOO п.л.

Полиграфический центр МЭИ(ТУ)

Красноказарменная ул.,д.13

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

ВВЕДЕНИЕ.

ГЛАВА 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. Алгоритм метода полного перебора: БТМ,,.

ВЫВОДЫ.

ГЛАВА 3. МЕТОД АНАЛИТИЧЕСКИХ ТАБЛИЦ С ФИКТИВНЫМИ ПЕРЕМЕННЫМИ.

3.1. Подстановки и их свойства.

3.2. Согласование.

3.3. Композиция подстановок.

3.4. Алгоритм согласования.

3.5. Введение гранулы и теней.

3.6. Работа с множественными конфликтами подстановок.

3.7. Эвристики, улучшающие процедуру опровержения.

3.8. Последовательный метод с фиктивными переменными: БТМ,/.

3.9. Параллельный метод с фиктивными переменными: РТМ,,.

ВЫВОДЫ.

ГЛАВА 4. МОДИФИКАЦИИ ПАРАЛЛЕЛЬНОГО МЕТОДА АНАЛИТИЧЕСКИХ ТАБЛИЦ С ФИКТИВНЫМИ ПЕРЕМЕННЫМИ.

4.1. Параллельный метод полного перебора, использующий стратегию поиска "в ширину" : РТМеМ.

4.2. Параллельный метод полного перебора, использующий стратегию поиска "в глубину" : PTMerfrf.

4.3. Параллельный метод с фиктивными переменными, использующий стратегию поиска "в ширину" : ртм^.

4.4. Параллельный метод с фиктивными переменными, использующий стратегию поиска "в глубину":PTMddd.

4.5. Программная реализация разработанных методов и их сравнение

4.5.1. Структура программного комплекса РТМ.

4.5.2.Тестирование методов.

4.5.3. Сравнение метода полного перебора с методом с фиктивными переменными.

4.5.4. Сравнение последовательного метода с фиктивными переменными с параллельным методом, использующим стратегии поиска "в глубину" и "в ширину".

ВЫВОДЫ.

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

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

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

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

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

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

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

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

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

- выполнить программную реализацию исследованных методов для многоядерных машин с общей памятью;

- произвести сравнение результатов, полученных на тестовых примерах.

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

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

Научная новизна полученных в диссертации результатов состоит в том, что

1) проведён анализ преимущества параллельного вывода на аналитических таблицах по сравнению с последовательным методом в задачах практической сложности.

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

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

Практическая значимость результатов диссертационной работы заключается в создании программной системы, в рамках которой реализованы алгоритмы последовательного и параллельного вывода на аналитических таблицах, использующие две стратегии поиска: "в ширину" и "в глубину". Программы реализованы в среде Microsoft Visual Studio 2010 на языке С#.

Реализованные алгоритмы были также использованы для решения тестовой задачи «Стимроллер», а также в учебном процессе при изучении дисциплин " Математическая логика " и " Экспертные системы " (на английском языке).

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных "Информационные технологии в науке, образовании, телекоммуникации и бизнесе", IT + S&E' 2012. Украина, Крым, Ялта-Гурзуф, 25.05 - 04. 06. 2012, на 17-ой и 18-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в НИУ «МЭИ» (г. Москва, 2010 — 2012 г.г.).

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 5 печатных работах, включая 2 статьи в изданиях из перечня ВАК.

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

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

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

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

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

Выводы

В настоящей главе получены следующие выводы.

1. Представлены параллельный метод с фиктивными переменными, использующий стратегию поиска "в ширину", и параллельный метод с фиктивными переменными,. использующий стратегию поиска "в глубину".

Заключение

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

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

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

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

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

4) Для метода унификаций предложен более эффективный способ работы с подстановками.

5) Предложены эвристики, повышающие эффективность вывода, как для пропозициональной логики, так и для логики предикатов первого порядка.

6) Разработаны последовательные и параллельные методы с фиктивными переменными, использующие стратегии "в глубину" и "в ширину" для аналитических таблиц, и разработаны алгоритмы, реализующие эти методы.

7) Программно реализованы параллельные алгоритмы полного перебора, использующие стратегии поиска "в ширину" (РТМеМ) и "в глубину" (РТМе£/Д а также параллельные алгоритмы с фиктивными переменными, использующие те же самые стратегии поиска (РТМ^м и РТМ Мс1).

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

1. Вагин В.Н,Головина Е.Ю.,Загорянская А.А., Фомина М.В.

2. Достоверный и правдоподобный вывод в ителлектуальных системах // Под ред.В.Н Вагина, Д.А. Поспелова. М., Физматлит, 2008, 712 с.

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

4. Smullan R.V. First-order logic! Springer-Verlag, Berlin, Heidelberg, New York, 1968, 158 p.

5. Robert Johnson. Parallel Analytic Tableaux Systems, Submitted for the degree of Doctor of Philosophy, 1996, 372 p.

6. Bonacina M.P. A Taxonomy of Parallel Strategies for Deduction // Ann. Of Math, and Artificial Intell. 2000. 29 (1, 2, 3, 4), pp. 223-257.

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

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

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

10. Davis М., Putnam Н. A computing procedure for quantification theory // Journal of the ACM. -№7. 1960. - pp. 201-215.

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

12. Knuth D. E. and Bendix P. B. "Simple Word Problems in Universal Algebra." In Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967). Pergamon Press, pp. 263-297, 1970.

13. Kowalski R. A Proof Procedure Using Connection Graphs // J. of the ACM. 1975. V.22D). P. 572-599.Karlsruhe, FRG, 1976.

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

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

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

17. 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.

18. 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.

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. 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 Academic Publisher, 1991. pp. 3160.

21. 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.

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

23. 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.

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

25. 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.

26. Conry 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.

27. S. Oppacher, E. Suen; 1988. HARP: A Tableau-Based Theorem Prover. In Journal of Automated Reasoning 4 (1988) pp. 69-100.

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

29. 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.

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

31. Jaakko Hintikka; 1955. Form and Content in Quantification Theory. Acta Philosophica Fennica, no.8, pp. 7-55, Helsinki.

32. Jaakko Hintikka; 1955. Notes of Quantification Theory, Societas Scientiarum Fennica, Commentations Physico-Mathematicae, vol.17, no. 12, Helsinki.

33. Evert W. Beth; 1962 Formal Methods. D. Reidel Publishing Co., Dordrecht, Hplland, and Gordon and Breach, Science Publishers Inc.,New York.

34. Evert W. Beth; 1966. The Foundations of mathematics. North- Holland Publishing Company, Amsterdam 1959 (rev. 1964) , and Harper Torchbooks, Harper Row, Publishers Incorporated, New York.

35. Melvin Fitting. Intuitionistic model theory and forcing. North-Holland, Amsterdam, 1969.

36. Melvin Fitting. Proof methods for model and intuitionistic logics, 1983.

37. Fabio Massacci. Single step tableaux for modal logics: Methodology, computations, algorithms, Journal of Automated Reasoning, 24(3):319-364, 2000.

38. Marcello D'Agostino. Handbook of tableaux methods, Springer, 1999 , 670 p.

39. Melvin Fitting. First-Order Logic and Automated Theorem Proving. -N.Y.:Springer-Verlag, 1990, 511 p.

40. Joachim Possega. " Compiling proof Search in Semantic Tableaux ", In proceedings 7th International Symposium on methodologies for Intelligent Systems. Springer LNAI. 1993.

41. Richard C. Jeffrey; 1967. Formal Logic: It's scope and limits. McGraw-Hill.

42. Dag Prawitz; 1960. An Improved Proof Procedure. In Theoria 26, pp. 102139.

43. Steve Reeves; 1986. Theorem-proving by semantic tableaux. Ph.D. thesis. Centre for Computing and Computer Science, Faculty of Science and Engineering, University of Birmingham.

44. Steve Reeves; 1987. Semantic Tableaux as framework for Automated Theorem-Proving. In advances in Artificial Intelligence, eds. John Hallam and Chris Mellish. Wiley.

45. Hai-Ping Ko and Mark E. Nadel; 1991. Substitution and Refutation Revisited. In proceedings of ICLP, Furukawa (ed.), pp.679-692, MIT Press.

46. Jophien Van Vaalen. An extension of unification to substitutions with an application to automatic theorem proving. Mathematisch Centrum, Amsterdam, The Netherlands.

47. G.H. Pollard; 1981. Parallel Execution of Horn Clause Programs. Ph.D. thesis, Department of Computing, Imperial College, London.

48. Tom Khabaza; 1989. Towards and/ or logic programming. Ph.D. thesis. Cognitive Science Research paper, serial no. CSRP 158. University of Sussex, Brighton, BN1 9QN.

49. Chin-Liang Chang, Richard Char-Tung Lee; 1973. Symbolic Logic and Mechanical Theorem Proving. Academic Press Inc. (London) Ltd.

50. L. Wos, G. Robinson, D. Carson; 1965. Efficiency and completeness of the set of support strategy in theorem proving. JACM 12 (4), pp 536 541.

51. L. Wos; 1988. Automated Reasoning 33 Basic Research Problems. Prentice Hall.

52. Bernhard Beckert, Reiner Hahnle Automated Deduction: A Basis for Applications, volume I, chapter 1, 1998, 30 p.

53. Вагин B.H, Зо Мьо Хтет. Параллельный вывод в методе аналитических таблиц, Программные продукты и системы, № 3(95), 2011, с. 8-13.

54. Вагин В.Н, Зо Мьо Хтет. Модификации параллельного метода аналитических таблиц. Журнал "Открытое образавание". № 1(90) 2012. с. 6070.

55. Bernhard Beckert, Reiner Hahnle; 1992. An Improved Method for Adding Equality to Free Variable Semantic Tableaux. In proceedings CADE-11, 11th Conference on Automated Deduction, Albany NY. Springer, LNCS.

56. Francis Jeffry Pellertier. Seventy-Five Problems for Testing Automatic Theorem Provers//Journal of Automated Reasoning, 2, 1986, D. Reidel Publishing Company, pp. 191-216.58. http://rriai.org;.ru/si'edstva-avtomaticheskogo-dokazatelstva-teorem-5.html

57. J. Schumann, R. Letz, 1990. PARTHEO: A high performance parallel theorem prover. In proceedings of the Tenth International Conference on Automated Deduction (CADE), pp 40-56.