автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Эквациональные LP-структуры и их приложения в системах переписывания

ФГБОУ ВПО Московский государственный университет имени М.В. Ломоносова

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

БАРАНОВ Денис Владимирович

(ОСа

Эквациональные ЬР-структуры и их приложения в системах

переписывания

Специальность 05.13.17 - теоретические основы информатики

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

5 ДЕК 2013

Москва-2013

005542442

Работа выполнена на кафедре математического обеспечения ЭВМ факультета прикладной математики, информатики и механики ФГБОУ ВПО «Воронежский государственный университет».

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

доцент

Махортов Сергей Дмитриевич

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

Кулик Борис Александрович, доктор физико-математических наук, старший научный сотрудник, ФГБУН Институт проблем машиноведения РАН

Афонин Сергей Александрович, кандидат физико-математических наук, ведущий научный сотрудник, НИИ механики МГУ имени М.В. Ломоносова

Ведущая организация: ФГБУН Институт систем информатики

им. А.П. Ершова Сибирского отделения РАН

Защита диссертации состоится 25 декабря 2013 года 16-45 час на заседании диссертационного совета Д 501.002.16, созданный на базе, ФГБОУ ВПО «Московский государственный университет имени М.В. Ломоносова» по адресу: 119991, Москва, ГСП-1, Ленинские горы, д.1, ФГБОУ ВПО МГУ имени М.В. Ломоносова, механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в Фундаментальной библиотеке ФГБОУ ВПО «Московский государственный университет имени М.В. Ломоносова» (Москва, Ломоносовский проспект, д.27, сектор А, 8 этаж).

Автореферат разослан «25» ноября 2013 г.

Ученый секретарь диссертационного совета

Д 501.002.16, созданный на базе, ФГБОУ ВПО, МГУ им. М.В. Ломоносова у

д. ф.-м. н., профессор

Корнев А. А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Тематика и актуальность исследования. В ряде областей математики и информатики вводятся и используются системы переписывания. Под (формальным) переписыванием подразумевают различные теоретические и практические методологии, определяющие процессы последовательной замены частей формул или термов формального языка, на основе некоторого множества (переписывающих) правил. В ряде источников процесс переписывания называется редуцированием (ARS - Abstract Reduction Systems). Изначально понятие переписывания было введено для развития методологии лямбда-исчисления. Впоследствии большая часть результатов и приложений на данном направлении оказалась связанной с переписыванием первого порядка. Такого рода системы называются системами переписывания термов (СПТ).

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

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

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

Как известно, эффективным средством формального построения и исследования моделей в информатике и программировании являются алгебраические системы (см. работы Замулина А. В., Подловченко Р. И. и других авторов). Это положение непосредственно относится и к инженерии знаний. Алгебраические методы представления знаний и управления знаниями описаны, например, в работах Hájek Р., Oles F. J., Sowa J. F., а также монографиях Бениаминова Е.М., Тейза А. и Грибомона П. Обзор имеющихся подходов к верификации знаний содержится в работах Gupta U. G., Рыбиной Г.В. и Смирнова В. В. В то же время многие модели в информатике по своей сути имеют продукционный характер. Кроме того, структуры представления

информации часто являются иерархическими. Во многих работах иерархические системы изображаются математическими решетками.

Немало публикаций было посвящено непосредственным исследованиям систем переписывания термов. Здесь, в частности, можно привести фундаментальную серию трудов Н. Дершовица, а также ряд работ других авторов (например, Klop J. W., Schmitt P. H.). Следует отметить работу И.О. Ануреева, где предложено обобщение теории СПТ до более мощного средства -систем переписывания формул.

Важными вопросами, связанными с системами переписывания термов, являются эквивалентные преобразования, упрощение и верификация их множеств правил. Данная тематика представлена, в частности, работами Fokkink W., Chiba Y., Metivier Y., Minari P., Toyama Y. Однако для более сложной модели - условных систем переписывания термов отмеченные вопросы практически не решались. Подобные системы образованы правилами переписывания импликативного типа, состоящими из предпосылок и заключений, каждая из которых включает подмножества обычных правил. Условные системы переписывания адекватно формализуют многие предметные области в информатике, которые не могут быть описаны обычными системами. В частности, они играют центральную роль в парадигме алгебраического программирования (Bergstra J.A., Letichevsky А.А.).

В 2009 году была опубликована статья С.Д.Махортова1, где условная СПТ (точнее - лежащая в ее основе условная эквациональная теория, изучающая вопросы равенства термов) рассмотрена как логическая система продукционного типа. Представленный подход позволил по-новому взглянуть на задачи эквивалентных преобразований, минимизации и верификации условных СПТ, а также впервые частично их решить. Подход основан на новом классе решеточных алгебраических систем - эквациональных LP-структурах (Lattice-Production structure). В частности, задача минимизации множества правил условной СПТ сводится к логической редукции LP-структуры. Однако рассмотренная в указанной работе алгебраическая модель имела некоторые ограничения, не позволяющие решить окончательно задачи эквивалентных преобразований и минимизации условной СПТ. Точнее - в ней не учитывалось свойство транзитивности (не условных) атомарных равенств термов. Кроме того, исследование эквациональных LP-структур не было завершено в плане обеспечения верификации условных СПТ. Наконец, до сих пор не существовало компьютерной реализации, показывающей работоспособность подобной модели на практике.

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

1 Махортоа С.Д. Основанный на решетках подход к исследованию и оптимизации множества правил условной системы переписывания термов / С. Д. Махортов // Интеллектуальные системы. - 2009. - Т. 13, вып 1-4. - С. 51-

такой теории. Целью настоящей диссертационной работы является решение сформулированной задачи.

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

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

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

Научная новизна диссертации заключается в следующих положениях.

• Построен класс эквациональных ЬР-структур, обладающий новыми свойствами и адекватно отражающий семантику условных эквациональных теорий. В частности, сняты ограничения, примененные в работе С.Д.Махортова.

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

• Показано, что произвольная эквациональная ЬР-структура может быть приведена к каноническому виду.

• Впервые введено понятие продукционно-логического уравнения в эквациональной ЬР-структуре и обоснован способ его решения, что в приложении соответствует полному обратному выводу. Концепция уравнений может быть применена для верификации условных эквациональных теорий.

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

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

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

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

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

• XV Международной конференции «Современные проблемы информатизации в моделировании и социальных технологиях» (Воронеж, 2010);

• XII Национальной конференции по искусственному интеллекту с международным участием КИИ-2010 (Тверь, 2010);

• Международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж, 2010);

• IV Международной научной конференции «Современные проблемы прикладной математики, теории управления и математического моделирования» (Воронеж, 2011);

• III Всероссийской конференция с международным участием «Знания -Онтологии - Теории» (ЗОНТ-2011) (Новосибирск, 2011);

• X Всероссийской научной конференции «Нейрокомпьютеры и их применение» (НКП-2012) (Москва, 2012);

• XI Всероссийской научной конференции «Нейрокомпьютеры и их применение» (НКП-2013) (Москва, 2013);

• научном семинаре «Проблемы современных вычислительных систем» механико-математического факультета МГУ имени М.В. Ломоносова, рук. В.А. Васенин (Москва, 2013);

а также научных сессиях Воронежского госуниверситета (2010-2013).

Публикации. По теме диссертации опубликовано 10 научных работ, список которых приведен в ее заключительной части. Статьи [1-3] соответствуют Перечню ВАК РФ. Опубликованные работы вполне отражают содержание диссертации. Получено свидетельство о регистрации компьютерной программы [11].

Личный вклад автора. В диссертационной работе изложены результаты, полученные лично автором, включая исследование проблематики, решения задач, алгоритмы и программную реализацию. Из двух работ [7-8], опубликованных совместно с научным руководителем, в диссертацию вошли только результаты автора.

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

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

Глава 1 носит вводный характер. Ее цель - погружение в тематику и предметную область диссертационного исследования и его возможных приложений. Неформально слово «терм» служит в качестве абстрактного обозначения элементов некоторых предметных областей, таких как единицы информации, конструкции формальных языков, математические формулы. При определении системы переписывания термов отправной точкой часто является эквациональная теория, множество правил которой состоит из равенств. Совокупность правил переписывания может быть получена путем «ориентации» равенств. Поскольку обычно именно эквациональная теория является критерием эквивалентности систем переписывания, исследование в этом плане условных СПТ может базироваться на рассмотрении эквивалентности условных эквациональных теорий.

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

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

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

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

2 Подколзин A.C. Компьютерное моделирование логических процессов. Архитектура и языки решателя задач / A.C. Подколзин. - м.: Физматлит, 2008. - 1020 с.

5 Аладьев В.З. Программирование в пакетах Maple и Mathematica: Сравнительный аспект / B.3. Аладьев, B.K. Бойко, Е. А. Ровба. - Гродно: Гродненский Госуниверситет, 2011. - 517 с.

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

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

Эквациональная теория (обычная, то есть не условная) определяется парой

Здесь X - алфавит, представляющий собой объединение следующих непересекающихся множеств: V - множество переменных; £„, « = 0,1,... -множества и-арных функций (функциональных символов) Стандартным образом определяется множество термов Г(2) (К1ор Отображение

а:У—>Г(Е) называется подстановкой. Это понятие распространяется на все 1<=Т(£).

Е с Г(Е) х Г(Е) - множество равенств вида 5 = ? (^, / е Г(2)). В рамках этой теории определяется понятие выводимости равенства я = ? из Е ((X,Е) [-5 = /):

1) если $ = то (£,£)(-$ = ?;

2) если то = ...,?„) для любого

3) если (Г, £) Ь 5 = /, то (Е,Е) Ьсг(^) = сг(?) для любой подстановки ст;

4) (&Е)Н = г,

5) если (Е,£)И,=г2,г2=г3,то (Е,£)И,=Г3;

6) если (Е,£)Ьа = *,то (1,£)1-/ = 5.

Основная задача эквациональной теории - выяснения вопроса о равенстве заданной пары термов. Их равенство может быть выведено из некоторого исходного набора равенств на основе перечисленных правил дедукции 1) -6).

Условная эквациональная теория задается набором условных соотношений

вида 5,=/,.....зп = 1п:и1 =у1,...,«я = у)я. Смысл такого соотношения: если имеют

место равенства термов в, = г = 1,...,и, то выполнены и все / =

Будем называть эти соотношения (условными) эквациональными правилами.

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

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

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

равенств = Каждому правилу sl=tí,...,sll=t„ ...........w„,=v,„ соответствует

пара (a,b)sR, где а={¿,=7,.....sn=tn} и b={u]=v],...,itm=vj. Рассматриваемая

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

Рассмотрим эквациональную теорию (1,£). Для Е введем множество конечных подмножеств Л(Е). В нем определены отношения включения С, Э (з - строгое включение), а также «решеточные» операции П и U - теоретико-множественные пересечение и объединение. Кроме них на решетке потребуются еще три группы операций, связанных соответственно с функциями, подстановками и транзитивностью равенств термов:

1) если a = {s,=t,\i = l,...,n} и /6Z„ то Да) = {/(*,,...,*„) = /(*,,...,*„)};

2) если a = {sj=tj\j = l,...,m}, то (r{á) = {a{s¡) = a{tJ)\j = \>...,m} для подстановки сг;

3) если a = {tt =t2,t2=t3},b = {tt =t3}, то b = Tr(o).

Определение 2.1.1. Пусть задана эквациональная теория (£,£). Эквациональной решеткой называется решетка ПГ, полученная пополнением Л(Е) относительно операций 1)-3).

Основываясь на аксиомах и правилах вывода в обычной эквациональной теории, сформулируем их аналоги для условной эквациональной дедукции. Аксиомы порождаются перечисленными выше правилами вывода равенств 1)-6). Правило вывода 2) означает наличие условного правила (аксиомы) а:Да) для любых a = {í, = tv...,sn =tn) и /е£„; из 3) следует аксиома а: а(а) для любых ае F и подстановки сг. Правило 5) порождает аксиому а: Тг(а) для каждого подходящего а е F. Такие условные правила в рассматриваемой логике можно также назвать тавтологиями. Еще одной очевидной тавтологией является правило а: b при а~эЬ.

Правила вывода в условной эквациональной логике таковы:

1) а:b hа(а):<r(b) (a,beF) для любой подстановки <т;

2) а: Ь, а: с \~а: b U с (a,b,c) е F (возможность вывода по частям);

3) a:b, b:c\~a:c (a,b,c) еF (транзитивность).

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

Отношение R назовем применимым, если для любой подстановки а из (a,b)sR следует (a(a),a(b)) е R. Отношение R назовем U -дистрибутивным, если для любых (a,b,),(a,¿>2) е R выполнено (a,bl \Jb2)eR.

Следующее определение суммирует рассмотренные свойства.

Определение 2.2.3. Бинарное отношение на эквациональной решетке называется логическим, если оно содержит все тавтологии, а также является применимым, U-дистрибутивным и транзитивным. Логическим замыканием произвольного отношения R называется наименьшее логическое отношение, содержащее R.

Теорема 2.2.1. Для произвольного отношения R на эквациональной решетке существует логическое замыкание ——>.

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

Два отношения и R1, определенные на общей эквациональной решетке, называются эквивалентными, если их логические замыкания совпадают. Этот факт будем обозначать Я, ~ R2. Логической редукцией данного отношения R называется минимальное эквивалентное ему отношение Rg.

Теорема 2.2.2. Пусть - отношения на общей эквациональной

решетке. Если при этом Rt ~ R2 и R} ~ R4, то Л, U R¡ ~ R2 U R4.

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

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

Для произвольного отношения R на эквациональной решетке F рассмотрим отношение R, построенное последовательным выполнением следующих шагов:

1) добавить к R все пары (а,Ъ), для которых b = a(a), b = f{a) либо Ъ = Тг(а), и обозначить новое отношение Л,;

2) добавить к Л, всевозможные пары вида (сг(а),сг(6)), для которых (а,Ь) е Rlt и обозначить новое отношение R2;

3) добавить к R2 всевозможные пары вида (я, \Ja2 lL.Ua„„ b¡\Jb2 U...U6J, где (a,,fe,) s R2, и обозначить новое отношение R¡;

4) объединить R3 с отношением гэ.

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

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

1) исключить из Я все пары (а,Ь), для которых агэй, и обозначить новое отношение

2) исключить из все пары (а,Ь) вида (а, 1Ц lL.Ua,,,, 6, 11-Щ,,), где (я„6,)е Д_|5 причем (а,6) не совпадает ни с одной парой (а.,Ь,), и обозначить новое отношение Я_2;

3) исключить из Я_2 всевозможные пары вида (а(а),сг(Ь)), для которых (а,Ь) б Л_2, причем {а,Ь) не совпадает с парой (сг(а),сг(6)), и обозначить новое отношение ;

4) исключить из все пары (а,Ь), для которых Ь-сг(а), Ь-/(а), либо Ъ = Тг(а).

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

Теорема 2.4.2. Пусть для отношения Я на эквациональной решетке Ш" построено соответствующее отношение К. Тогда, если для Я существует транзитивная редукция , то соответствующее ей отношение Я0 представляет собой логическую редукцию исходного отношения Я.

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

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

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

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

Для определения и исследования логических уравнений требуется понятие канонического бинарного отношения на эквациональной решетке.

Определение 3.1.1. Отношение на эквациональной решетке называется каноническим, если оно состоит из пар «хорновского» типа: правая часть пары представляет собой атом решетки, левая - объединение атомов.

Теорема 3.1.1. Дяя любого бинарного отношения на эквациональной решетке существует эквивалентное ему каноническое отношение.

Пусть задано конечное бинарное отношение Я на эквациональной решетке

Согласно предыдущим результатам, без ограничения общности можно

предполагать, что Я представлено логической редукцией в ее канонической форме. Рассмотрим множество всех атомов решетки, образующих элементы пар отношения Я, и обозначим его Оно конечно в силу конечности Я. Обозначим далее ¥я - подмножество решетки Ш", построенное на как системе образующих с помощью операции «решеточного» объединения. Очевидно, также конечно и содержит все элементы пар отношения Я.

Пусть имеет место А—где ——> - логическое замыкание отношения Я. Для данного Ве¥ минимальным прообразом при отношении — называется такой элемент Ае¥, что А—и А является минимальным, то есть не содержит никакого другого А, е Р, для которого А, ——>В.

Определение 3.2.1. Атом х е называется начальным при отношении Я, если в Я нет ни одной пары вида (А,х). Элемент X е называется начальным, если все его атомы начальные. Подмножество 8(7?) с , состоящее из всех начальных элементов ¥й, называется начальным множеством решетки (при отношении Я).

Рассмотрим уравнение

Я1{Х) = В, (3.2.1)

где Я1 - логическое замыкание Я, В - заданный элемент, X - неизвестный.

Определение 3.2.2. Точным (частным) решением X уравнения (3.2.1) называется любой минимальный прообраз элемента В, содержащийся в Приближенным (частным) решением X уравнения (3.2.1) называется любой прообраз элемента В, содержащийся в §. Общим решением уравнения (3.2.1) называется совокупность всех его частных решений {Хр}, реР.

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

Рассмотрен вопрос о том, как меняется общее решение уравнений вида (3.2.1) при объединении их правых частей. С этой целью вводится уравнение

Я1(Х) = В]иВ2 (3.2.2)

Теорема 3.2.1. Пусть {Хр}, реР - общее решение уравнения вида (3.2.1) с правой частью В{, а {Уд},де(2 - общее решение уравнения того же вида с правой частью Вг. Тогда общее решение уравнения (3.2.2) представляет собой множество всех элементов вида Хр{]Уд, из которого исключены элементы, содержащие другие элементы этого же множества.

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

Введем понятие структурного расслоения отношения Я на виртуальные слои (частичные отношения) {Л, | г е Т}. Оно позволяет упростить изучение свойств

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

части. Такое разбиение имеет смысл благодаря тому, что Я является каноническим. Обозначим эти подмножества Яр соответственно их элементу хр,реР.

Определение 3.3.1. Слоем Я, в отношении Я называется подмножество Я, образованное упорядоченными парами, взятыми по одной из каждого непустого Я", ре Р. Решение X уравнения (3.2.1) (точное или приближенное) порождается в Я некоторым слоем Я,, если X—

Теорема 3.3.1. Для нахождения общего решения уравнения (3.2.1) достаточно найти частное решение X, в каждом слое Я1, если оно существует. Далее из полученного множества решений необходимо исключить элементы, содержащие другие элементы этого же множества.

В итоге вопрос о решении уравнения (3.2.1) сводится к задаче нахождения решения уравнения

Я^Х) = Ь, (3.4.1)

где Ь - не начальный атом из , Я,- произвольный слой в Я.

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

Построим такой граф С^. Каждому атому из множества , то есть

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

В полученном графе выберем вершину Ь, соответствующую правой

части уравнения (3.4.1). Рассмотрим подграф С^^сб^, содержащий все вершины, из которых достижима вершина Ь (включая саму Ь) и все дуги, соединяющие такие вершины.

Следующий факт завершает обоснование пошагового процесса решения исходного логического уравнения (3.4.1).

Теорема 3.4.1. Уравнение (3.4.1) имеет не более одного решения. Если граф Ср^ь не содержит ориентированных циклов, то единственное решение

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

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

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

Описана архитектура объектно-ориентированной программной библиотеки, реализующей поиск и исключение избыточных правил в условной эквациональной теории на основе исследования главы 2. На ряде тестов подтверждена работоспособность созданных алгоритмов и, соответственно, практическая значимость новой LP-структуры. Для реализации использованы язык С# и платформа .Net как одна из наиболее распространённых на сегодняшний день систем программирования. Код написанной на данной платформе программы может быть собран с ключами, отвечающими за оптимизацию по скорости, и существенно не проигрывать аналогичным программам, реализованным на других платформах.

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

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

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

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

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

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

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

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

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

Приложение А диссертации содержит исходные тексты некоторых основных объектно-ориентированных классов разработанной программной системы.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ И ПЕРСПЕКТИВЫ

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

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

• Обоснованы эквивалентные преобразования эквациональных ЬР-структур. Данный результат открывает новые возможности автоматизации управления соответствующими базами знаний.

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

• Показано, что произвольная эквациональная ЬР-структура может быть приведена к каноническому виду.

• Впервые введено понятие продукционно-логического уравнения в эквациональной ЬР-структуре и обоснован способ его решения, что в приложении соответствует полному обратному выводу. Концепция уравнений

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

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

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

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

Автор выражает благодарность научному руководителю С.Д. Махортову за постановку задач и внимание к работе.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Баранов Д.В. Логические уравнения в эквациональных ЬР-структурах / Д.В. Баранов // Информационные технологии. - 2012. - № 8. - С. 35-42.

2. Баранов Д.В. Компьютерная реализация устранения избыточных правил в условных системах переписывания / Д.В. Баранов // Программная инженерия. - 2013, № 6. - С. 27-32.

3. Баранов Д.В. Алгебраическая интерпретация условных систем переписывания на основе ЬР-структур / Д. В. Баранов // Вестник ВГУ. Серия Системный анализ и информационные технологии. - Воронеж. -2010.-№ 2.-С. 131-138.

4. Баранов Д.В. Эквациональные ЬР-структуры представления знаний и связанные с ними логические уравнения / Д.В. Баранов // Третья Всероссийская конференция с международным участием «Знания -Онтологии - Теории» (ЗОНТ-2011). Новосибирск, 3-5 октября 2011г.: Материалы конференции. - Новосибирск: Институт математики им. С.Л. Соболева СО РАН, 2011. - Т. 1. - С. 24-29.

5. Баранов Д.В. Исследование логических уравнений в эквациональных ЬР-структурах / Д.В. Баранов // X Всероссийская научная конференция «Нейрокомпьютеры и их применение» (НКП-2012), Москва, 20 марта 2012 года. Тезисы докладов. -М: МГППУ, 2012. - С. 11.

6. Баранов Д.В. О программной реализации поиска тавтологий в условных системах переписывания / Д.В. Баранов // XI Всероссийская научная конференция «Нейрокомпьютеры и их применение» (НКП-2013), Москва, 19 марта 2013 года. Тезисы докладов. - М: МГППУ, 2013. - С. 26.

7. Баранов Д.В. Исследование и оптимизация условных систем переписывания на основе продукционно-логической модели / Д.В. Баранов, С. Д. Махортов // XII национальная конференция по искусственному интеллекту с международным участием КИИ-2010 (20-24 сентября 2010г., г. Тверь): Труды конференции. Т. 1. - М. : Физматлит, 2010.-С. 29-37.

В работе [7] Баранову Д.В. принадлежат формулировки и доказательства теорем.

8. Баранов Д.В. ЬР-структуры в условных системах переписывания / С. Д. Махортов, Д.В. Баранов // Современные проблемы информатизации в моделировании и социальных технологиях: сб. трудов / Под ред. О. Я. Кравца. -Воронеж : Научная книга, 2010. - Вып. 15. - С. 272-276.

В работе [8] Баранову Д.В. принадлежат формулировки и доказательства теорем.

9. Баранов Д.В. Эквациональные ЬР-структуры для оптимизации условных систем переписывания / Д.В. Баранов // Актуальные проблемы прикладной математики, информатики и механики: Сб. трудов Международной конференции. - Воронеж : ИПЦ ВГУ, 2010. - С. 44—46.

Ю.Баранов Д.В. ЬР-структуры для моделирования условных систем переписывания / Д.В. Баранов // Современные проблемы прикладной математики, теории управления и математического моделирования (ПМТУММ-2011): материалы IV Международной научной конференции. - Воронеж : ИПЦ ВГУ, 2011. - С. 23-25. 11 .Баранов Д.В. Библиотека ЬРТегтОрйпнгег / Д.В. Баранов // Свидетельство о государственной регистрации программы для ЭВМ. - М.: Федеральная служба по интеллектуальной собственности. - № 2013619458 от 04.10.2013.

Отпечатано в отделе оперативной печати Геологического ф-та МГУ Тираж |6С экз. Заказ № 6О

Воронежский государственный университет

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

04201451676 БАРАНОВ Денис Владимирович

Эквациональные ЬР-структуры и их приложения в

системах переписывания

специальность 05.13.17 -теоретические основы информатики

ДИССЕРТАЦИЯ

на соискание ученой степени кандидата физико-математических наук

Научный руководитель -доктор физико-математических наук, доцент С.Д. Махортов

Воронеж - 2013

Оглавление

Введение.......................................................................4

Глава 1. ЬР-структуры и решаемые задачи................................12

1.1. Примеры решаемых задач....................................................12

1.2. Термы и условные эквациональные теории...............................18

1.3. Логические системы продукционного типа.................................22

1.4. Базовая терминология теории ЬР-структур................................24

1.5. Модель стандартной продукционной системы...........................28

Глава 2. Эквациональные ЬР-структуры и их свойства.........33

2.1. Модель условной эквациональной теории.................................33

2.2. Логическое замыкание и эквивалентные преобразования..............35

2.3. Структура логических связей.................................................41

2.4. Логическая редукция...........................................................45

2.5. О практической реализации...................................................50

Глава 3. Уравнения в эквациональных ЬР-структурах..........54

3.1. Канонические отношения.....................................................54

3.2. Логические уравнения и их упрощение....................................57

3.3. Методология решения уравнений............................................60

3.4. Теорема о разрешимости.......................................................67

Глава 4. Компьютерная реализация

эквациональных ЬР-структур...................................72

4.1. Общее описание алгоритма...................................................74

4.2. Внутренний формат данных...................................................76

4.3. Компьютерная реализация алгоритма.......................................80

4.4. Описание алфавита языка системы.........................................83

4.5. Базовые классы библиотеки..................................................87

4.6. Ключевые особенности........................................................91

4.7. Основы работы с библиотекой...............................................93

4.8. О практическом применении..................................................97

Заключение.............................................................................99

Приложение А. Некоторые тексты программ........................101

А.1. Класс Таи1:о1с^уАпа1у2ег.....................................................101

А.2. Класс СЬатСгеаШг............................................................104

А.З. Класс ЕдиайопаИ^айюе.......................................................107

Литература............................................................................110

Введение

В ряде областей математики и информатики вводятся и используются так называемые системы переписывания. Под (формальным)

переписыванием подразумевают различные теоретические и практические методологии, определяющие процессы последовательной замены частей формул или термов формального языка, на основе некоторого множества (переписывающих) правил. В некоторых источниках [40] процесс переписывания называется редуцированием (ARS - Abstract Reduction Systems). Изначально понятие переписывания было введено для развития методологии лямбда-исчисления [49]. Впоследствии большая часть результатов и приложений на данном направлении оказалась связанной с переписыванием первого порядка [40]. Такого рода системы называются системами переписывания термов (СПТ).

В настоящее время теория систем переписывания представляет эффективный аппарат для решения важных проблем информатики, искусственного интеллекта и компьютерной алгебры. Системы переписывания термов и подобные им структуры находят применения в таких известных задачах как верификация компьютерных программ [55] и их преобразования [58], спецификация абстрактных типов данных [43, 13], реализация функциональных языков программирования [44], автоматическое доказательство теорем [20], символьное упрощение алгебраических выражений [6] и других.

Можно сказать, что в обобщенном смысле система переписывания - это формально описанная совокупность знаний (правил), разработанная для некоторой предметной области. Такие знания могут быть применены для реализации практических задач, в частности, перечисленных выше. Как и любая другая компьютерная система знаний, СПТ нуждается в управлении и сопровождении [16] - автоматизированном представлении [38], верификации [25], оптимизации [15], а также реализации процессов логического вывода.

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

Как известно, эффективным средством формального построения и исследования моделей в информатике являются алгебраические системы ([57, 71, 75] и другие). Это положение в полной мере непосредственно относится и к инженерии знаний. Алгебраические методы представления знаний и управления знаниями описаны, например, в работах [18, 31, 38], а также монографиях [50, 83]. Обзор имеющихся подходов к верификации знаний содержится в [17, 81]. В то же время многие модели в информатике по своей сути имеют продукционный характер [69, 86]. Кроме того, структуры представления информации часто являются иерархическими [31, 32]. Во многих работах иерархические системы изображаются математическими решетками [51]. Описание методов использования теории решеток для представления знаний можно найти в [31, 37, 83].

Немало публикаций было посвящено непосредственным исследованиям систем переписывания термов. Здесь, в частности, можно привести фундаментальную серию трудов Н. Дершовица [9, 10, 11], а также ряд работ других авторов (например, [24, 36]). Следует отметить работу И.С. Ануреева [48], где предложено обобщение теории СПТ до более мощного средства -систем переписывания формул.

Важными вопросами, связанными с системами переписывания термов, являются эквивалентные преобразования, упрощение и верификация их множеств правил. Данная тематика представлена, в частности, работами [14, 7, 27, 28, 41, 42]. Однако для более сложной модели - условных систем переписывания термов [9, 22, 23, 24] указанные проблемы практически не решались и соответственно далеки от своего завершения. Подобные системы образованы правилами переписывания импликативного типа, состоящими из

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

В 2009 году была опубликована статья [67], где условная СПТ (точнее -лежащая в ее основе условная эквациональная теория, изучающая вопросы равенства термов) рассмотрена как логическая система продукционного типа [1, 8]. Данный подход позволил по-новому взглянуть на задачи эквивалентных преобразований, минимизации и верификации условных СПТ, а также впервые частично их решить. Подход основан на новом классе решеточных алгебраических систем - эквациональных LP-структурах (Lattice-Production structure). В частности, задача минимизации множества правил условной СПТ сводится к логической редукции LP-структуры. Однако представленная в [67] алгебраическая модель имела некоторые ограничения, не позволяющие решить окончательно задачи эквивалентных преобразований и минимизации условной СПТ. Точнее - в ней не учитывалось свойство транзитивности атомарных (не условных) равенств термов. Кроме того, исследование эквациональных LP-структур не было завершено в плане обеспечения верификации условных СПТ. Наконец, до сих пор не существовало компьютерной реализации, показывающей работоспособность подобной модели на практике.

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

Перечисленные выше вопросы относятся к области создания и исследования моделей знаний, методов работы со знаниями, а также определения принципов построения программных средств автоматизации

управления знаниями. Данные положения непосредственно отражены в формуле и паспорте научной специальности 05.13.17 - Теоретические основы информатики (пп. 4, 8, 14).

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

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

Научная новизна диссертации заключается в следующих положениях.

• Построен класс эквациональных ЬР-структур, обладающий новыми свойствами и адекватно отражающий семантику условных эквациональных теорий. В частности, сняты ограничения, примененные в работе С.Д. Махортова [67].

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

• Показано, что произвольная эквациональная ЬР-структура может быть приведена к каноническому виду.

• Впервые введено понятие продукционно-логического уравнения в эквациональной ЬР-структуре и обоснован способ его решения, что в приложении соответствует полному обратному выводу [33]. Концепция уравнений может быть применена для верификации условных эквациональных теорий.

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

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

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

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

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

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

• XV Международной конференции «Современные проблемы информатизации в моделировании и социальных технологиях» (Воронеж, 2010);

• XII Национальной конференции по искусственному интеллекту с международным участием КИИ-2010 (Тверь, 2010);

• Международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж, 2010);

• IV Международной научной конференции «Современные проблемы прикладной математики, теории управления и математического моделирования» (Воронеж, 2011);

• III Всероссийской конференции с международным участием «Знания -Онтологии - Теории» (ЗОНТ-2011) (Новосибирск, 2011);

• X Всероссийской научной конференции «Нейрокомпьютеры и их применение» (НКП-2012) (Москва, 2012);

• XI Всероссийской научной конференции «Нейрокомпьютеры и их применение» (НКП-2013) (Москва, 2013);

• научном семинаре «Проблемьгсовременных вычислительных систем» механико-математического факультета МГУ имени М.В. Ломоносова, рук. В.А. Васенин (Москва, 2013);

а также научных сессиях Воронежского госуниверситета (2010-2013).

По теме диссертации опубликовано 10 научных работ, список которых приведен в ее заключительной части. Статьи [1-3] соответствуют Перечню ВАК РФ. Опубликованные работы вполне отражают содержание диссертации. Получено свидетельство о регистрации компьютерной программы [11].

В диссертационной работе изложены результаты, полученные лично автором, включая исследование проблематики, решения задач, алгоритмы и программную реализацию. Из двух работ [7-8], опубликованных совместно с научным руководителем, в диссертацию вошли только результаты автора.

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

Глава 1 по отношению к основному содержанию диссертации носит вводный характер. Ее цель - погружение в тематику и предметную область диссертационного исследования и его возможных приложений. Рассматриваются некоторые примеры практических задач, впоследствии приводящие к общей алгебраической модели. Излагаются основы эквациональных теорий и систем переписывания термов как исследуемая предметная область. В качестве ее обобщения рассматриваются логические системы продукционного типа. Далее, на пути перехода к абстрактным алгебраическим системам, вводятся необходимые понятия и обозначения из теории отношений и решеток. Наконец, описывается стандартная ЬР-структура как алгебраическая модель продукционной системы, и перечисляются ее основные свойства.

Подобно транзитивному замыканию и транзитивной редукции бинарного отношения на обычном множестве, в теории ЬР-структур решаются более сложные задачи нахождения логического замыкания и логической редукции отношений на иерархических множествах - различных видах решеток._

Глава 2 посвящена определению и изучению эквациональной ЬР-структуры с расширенной логикой. Такая структура возникает в качестве

модели условной эквациональной теории и соответствующей условной системы переписывания термов.

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

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

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

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

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

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

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

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

Глава 1. ЬР-структуры и решаемые задачи

Настоящая диссертационная работа в основном содержании посвящена развитию формализма специальных алгебраических систем (ЬР-структур), моделирующих в различных предметных областях продукционно-логические связи на основе математических решеток и бинарных отношений. Результаты предыдущих исследований [69] показали применимость подобных теоретических положений к созданию программного обеспечения процессов представления и использования знаний продукционного типа. Цель настоящей главы - погружение в тематику и предметную область таких исследований и приложений.

Обсуждаются некоторые примеры практических задач, впоследствии приводящие к общей алгебраическо�