Эквациональные LP-структуры и их приложения в системах переписывания тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат наук Баранов, Денис Владимирович

• Баранов, Денис Владимирович
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Баранов, Денис Владимирович

Оглавление

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение

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

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

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

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

Литература

Введение диссертации (часть автореферата) на тему «Эквациональные LP-структуры и их приложения в системах переписывания»

Введение

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

переписыванием подразумевают различные теоретические и практические методологии, определяющие процессы последовательной замены частей формул или термов формального языка, на основе некоторого множества (переписывающих) правил. В некоторых источниках [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] показали применимость подобных теоретических положений к созданию программного обеспечения процессов представления и использования знаний продукционного типа. Цель настоящей главы - погружение в тематику и предметную область таких исследований и приложений.

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

1Л. Примеры решаемых задач

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

углубляться в конструкцию отдельных кирпичей. Кирпич в определенной ситуации может служить абстрактным атомарным объектом. Недаром современная системная инженерия изучает холоны - вложенные друг в друга системы [21]. Особо важную роль абстрагирование играет при алгоритмизации решаемых задач.

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

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

Итак, пусть дано квадратное уравнение на множестве вещественных чисел: ах2+Ьх + с = 0 (аФ 0). Оно имеет решение, если неотрицателен дискриминант: Ь2 - 4ас > 0. В этом благоприятном случае вещественные корни уравнения, как известно, можно вычислить по формулам

_-Ь-\/ь2 -4ас _~Ь + ^Ь2 -Лас 2 а 2 а

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

левых—и—правых—частях—отношений_обозначим__термом__Можно„ввести

следующие термы:

~ 0, ~ а, 1ъ~Ъ2 - 4ас, ¡4 ~ ах2 + Ьх + с, ¡5 ~ х]} ~ х2, а также

-b - *Jb2 -4ac -b + \lb2 -4ac t---- t----

2 a 2 a

Здесь, наряду с константами {0,2,4} и переменными {а,Ь,с,х,х],х2},

используются также 1-арная функция изменения знака («минус»), 1-арная функция извлечения корня и стандартные арифметические 2-арные функции (возведение в квадрат можно реализовать произведением). В общем случае (как и в рассматриваемом примере) термы взаимозависимы - один терм может использоваться в качестве аргумента функции в другом терме («подстановка»).

Заметим далее, что условия неравенств (а ф 0, Ь2 - 4ас > 0) могут быть представлены эквивалентными им равенствами термов. В частности, вводя 2-арные функции ф (•, •) и >(•,•) с булевой областью значений, а также термы t9~ 1, tw ~ ф (t2, i,), tu~>{t3,tx), условия на коэффициенты уравнения можно заменить равенствами tl0 = t9 и tu -t9. Здесь константа 1 (терм t9) выбрана в качестве эквивалента булевского значения true.

Таким образом, все упомянутые в примере соотношения могут рассматриваться как равенства термов. При этом можно сформулировать следующее условное «правило переписывания», фактически содержащее математическое знание о решении квадратного уравнения:

¿4 — t\ 1 Ао — ' h 1 — ^9 • Н ~ ' К ~ h • Семантика правила такова: если верны все равенства термов в предпосылке (слева от « : »), то верны все равенства термов в заключении (справа от « : »).

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

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

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

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

Одна из задач, для решения которой могут использоваться системы переписывания - автоматизированная система разбора текстов. Основной целью подобной системы может, например, являться разбиение входящих электронных писем на составляющие для облегчения дальнейшей обработки получаемой информации. Возможный способ выделения элементов текста предоставляют регулярные выражения. Здесь и далее под термином «регулярное выражение» подразумевается не математический объект, а его значение в соответствии с интерпретацией в языках программирования (например, Perl) [84, 70].

Согласно данной трактовке, регулярные выражения - это формальный язык поиска и реализации ряда манипуляций с подстроками в тексте, основанный на использовании метасимволов. Регулярное выражение

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

Введем некоторые понятия для более формального описания задачи. Разбираемый текст состоит из строк символов. Термами в данной задаче будем называть всевозможные строки/подстроки. Строка (терм) s выводится из строки (терма) t (данный факт обозначается если s может быть

получена из t применением содержащихся в t метасимволов, то есть подстановками, в соответствии с семантикой языка регулярных выражений. Например, вместо метасимвола «[1-9]» можно подставить любую ненулевую цифру. Заметим, что направление переписывания может быть принято и обратным, в зависимости от реализуемого подхода к распознаванию подстрок (нисходящий/восходящий). Более того, на некотором уровне абстрагирования системы вместо ориентированных правил переписывания (/ —>• 5) достаточно рассмотреть эквациональную теорию (t = s).

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

В реальном примере (разбор писем) могут быть выделены несколько специальных типов термов, например, следующие.

1. Регулярное выражение (шаблон).

2. Физический токен. Описывает, какие элементы могут быть получены в результате разбора текста:

а) число;

__Ь) дата;________

c) текст;

d) разделитель. i

3. Логический токен. Несет в себе смысл физического токена (бизнес-логику).

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

Вводимая типизация термов порождает, в частности, набор функций на их множестве, а также условные правила переписывания. Так можно ввести 1-арные функции физический _токен{8), со значениями {число, дата, текст, разделитель, null} и другие подобные функции. Последнее из перечисленных значений может выдаваться в случае, когда тестируемый терм 5 вообще не относится к физическим токенам. Некоторые из условных правил могут считаться тавтологиями, поскольку порождаются так называемыми аксиомами. Например, правило

s = t, физический jnoKenis) = дата : физический_токен{1) = дата не зависит от исследуемого текста и даже от текущего набора шаблонов в системе, поэтому является тавтологией. Такие правила обычно не хранятся в базе знаний, а автоматически подразумеваются на уровне семантики системы переписывания, ее машины логического вывода. В то же время правило следующего вида:

физический_moKen{s) = дата, расстояние (5, «контракт») < 20 : логический jnoKenis) = дата_контракта не относится к тавтологиям. Оно не содержит избыточности и может быть использовано для вывода логического типа некоторого физического токена.

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

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

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

Список литературы диссертационного исследования кандидат наук Баранов, Денис Владимирович, 2013 год

Литература

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

части данного раздела отдельным списком.

1. Agarwal R. A Petri-Net based approach for verifying the integrity of production systems / R. A. Agarwal // International Journal of Man-Machine Studies. - 1992. - № 36. - P. 447^68.

2. Aho A. V. The transitive reduction of a directed graph. SIAM J. Computing 1 : 2 / A. V. Aho, M. R. Garey, J. D. Ulman, 1972. - P. 131-137.

3. Andreka H. Algebraic Logic / H. Andreka, J. D. Monk, I. Nemeti. - Dordrecht : North-Holland Publ. Co, 1991.

4. Bergstra J.A., Hearing J., and Klint P., editors. Algebraic Specification. ACM Press and Addison-Wesley, Reading, MA, 1989.

5. Boros E. Horn minimization by iterative decomposition / E. Boros, O. Cepek, A. Kogan // Annals of Mathematics and Artificial Intelligence 23, 3^1 Jan., 1998.-P. 321-343.

6. Buchberger B. Algebraic Simplification / B. Buchberger, R. Loos // Computer Algebra - Symbolic and Algebraic Computation / eds. B. Buchberger, G.E.Collins, R. Loos. - Vienna - New York : Springer-Verlag, 1982. -P. 11-43.

7. Chiba Y. How to Prove Equivalence of Rewriting Systems without (Explicit) Induction / Y. Chiba // 2nd Romanian-Japanese Algebraric Specification Workshop 2011. - Japan Advanced Institute of Science and Technology. -2011.

8. Davis R. An overview of production systems / R. Davis, J. King // Mahine Intelligence. - Chichester : Ellis Horwood Limited. - 1977. - Vol 8. - P. 300332.

9. Dershowitz N. Termination of rewriting / N. Dershowitz // J. Symbolic Comput. - 1987. - V. 3. - P. 69-116.

10. Dershowitz N. A Taste of Rewrite Systems. In Functional Programming, Concurrency, Simulation and Automated Reasoning: international Lecture Series 1991-1992, Mcmaster University, Hamilton, Ontario, Canada / Dershowitz N. ; ed. P. E. Lauer // Lecture Notes In Computer Science. -London : Springer-Verlag. - V. 693. - P. 199-228.

11. Dershowitz N. Canonical Conditional Rewrite Systems / N. Dershowitz, M. Okada, G. Sivakumar // Proceedings of the 9th international Conference on Automated Deduction (May 23-26, 1988) / eds E. L. Lusk, R. A. Overbeek// Lecture Notes In Computer Science. - London : Springer-Verlag. - 1988. -Vol. 310.-P. 538-549.

12. Doorenbos R. B. Production Matching for Large Learning Systems. Doctoral Thesis. UMI Order Number: UMI Order No. GAX95-22942., Carnegie Mellon University / R. B. Doorenbos, 1995.

13. Droster K. Towards executable specification using conditional axioms / K. Droster // Ibid. - 1984. - Vol. 166. - P. 85-96.

14. Fokkink W. Lazy rewriting on eager machinery / W. Fokkink, J. Kamperman P. Walters // ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000). - P. 45-86.

15. Ginsberg A. Knowledge-Base Reduction: A New Approach to Checking Knowledge Bases for Inconsistency & Redundancy / A. Ginsberg // Proceedings of the Seventh National Conference on Artificial Intelligence, 1988.-P. 585-589.

16. Glower F. Logical Testing for Rule-Based Management / F. Glower, H. J. Greenberg // Annals of Operations Research. - 1988. - № 12. - P. 199215.

17. Gupta U. G. Validation and verification of knowledge-based systems: A survey / U. G. Gupta // Journal of Applied Intelligence. - 1993. - V. 3. - P. 343-363.

18. Häjek P. A generalized algebraic approach to uncertainty processing in rule-based expert systems (dempsteroids) / P. Häjek, J. V. Valdes // Comput. Artif. Intell.- 1991,-V. 10, N. 1. - P. 29-42.

19. Hammer P. L. Optimal compression of propositional Horn knowledge bases: complexity and approximation / P. L. Hammer, A. Kogan // Artif. Intell. -

1993.-V. 64, N. l.-P. 131-145.

20. Hsiang J. Refiitational theorem proving using term-rewriting systems / J. Hsiang // Artif. Intell. - 1985. - V. 25. - P. 255-300.

21. IEEE Std. 1220-2005, Standard for Application and Management of the System Engineering Process, IEEE Press, 2007.

22. Joannaud J.-P. and Karlan S., editors. Proc. Intern. Workshop on Conditional Term Rewriting Systems, Berlin. - Springer, 1988.

23. Karlan S. Conditional rewrite rules / S. Karlan // Theor. Comput. Sci. - 1984. -Vol. 33, N2/3.-P. 139-174.

24. Klop J. W. Term rewriting systems / J. W. Klop // Handbook of Logic in Computer Science (Vol. 2): Background: Computational Structures / eds S. Abramsky, D. M. Gabbay and S. E. Maibaum // Osborne Handbooks of Logic In Computer Science. - New York : Oxford University Press. - 1992. -Vol. 2.-P. 1-116.

25. Lee S. Developing a strategy for expert system verification and validation / S. Lee, R. M. O'Keefe // IEEE Trans, on Systems, Man and Cybernetics. -

1994. - Vol. 24. - P. 643-655.

26. Letichevsky A.A. and Kapitonova J. V. Algebraic programming in APS system. In Proc. ISSAC '90 Tokyo, Japan, pages 68-75, New York, 1990. ACM.

27. Metivier Y. About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm / Y. Metivier // Information Processing Letters 16, 1983.

28. Minari P. Analytic combinatory calculi and the elimination of transitivity / P. Minari // Archive for Mathematical Logic. - 2004. - V. 42, № 2. - P. 159-192.

29. Monk J. D. Handbook of Boolean Algebras / J. D. Monk. - Amsterdam : North-Holland Co, 1989. - Vols. I-III.

30. Ohlebusch E. Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems / E. Ohlebusch // Proceedings of the 6th international Conference on Logic Programming and Automated Reasoning

(September 6-10, 1999) / eds H. Ganzinger, D. A. McAllester and A. Voronkov // Lecture Notes In Computer Science. - London : Springer-Verlag.-Vol. 1705.-P.l 11-130.

31. Oles F. J. An Application of Lattice Theory to Knowledge Representation / F. J. Oles // Theor. Comput. Sei. 249, 1 (Oct. 2000). - P. 163-196.

32. Pederson K. Well-structured knowledge bases / K. Pederson // AI Expert. -1989.-№4.-P. 44-55.

33. Poli R. Backward-chaining evolutionary algorithms / R. Poli, W. B. Langdon // Artificial Intelligence. - August 2006. - Vol. 170, № 11. - P. 953-982.

34. Purdom P. A transitive closure algorithm / P. Purdom // BIT. - 1970. -Vol. 10.-P. 76-94.

35. Sahni S. Computationally related problems / S. Sahni II SLAM J. Computing 3 : 2.- 1974.-P. 262-279.

36. Schmitt P. H. A Survey of Rewrite Systems / P. H. Schmitt // Proceedings of the 1st Workshop on Computer Science Logic (October 12-16, 1987) / eds. E. Börger, H. K. Büning and M. M. Richter // Lecture Notes In Computer Science. - London : Springer-Verlag. - Vol. 329. - P. 235-262.

37. Sowa J. F. Conceptual Structures: Information Processing in Mind and Machine / J. F.Sowa. - Reading, MA : Addison-Wesley, 1984.

38. Sowa J. F. Knowledge Representation: Logical, Philosophical and Computational Foundations / J. F. Sowa. - Brooks Cole Publishing Co., Pacific Grove, CA, 1999.

39. Sowyer B. Programming Expert Systems in Pascal / B. Sowyer, D. Foster. -John Wiley & Sons, Inc., 1986.

40. Ter es e. Term Rewriting Systems. Part of Cambridge Tracts in Theoretical Computer Science / Terese. - Cambridge University Press, 2003.

41. Toyama Y. On Equivalence Transformations for Term Rewriting Systems / Y. Toyama // Proceedings of the 1983 and 1984 RIMS Symposia on Software Science and Engineering II / eds E. Goto, K. Araki and T. Yuasa // Lecture Notes In Computer Science. - London : Springer-Verlag. - 1986. -Vol. 220.-P. 44-61.

42. Toyama Y How to prove equivalence of term rewriting systems without induction / Y. Toyama // In Proc. of the 8th international conference on Automated deduction, J H Siekmann (Ed.). Springer-Verlag New York, Inc., New York, NY, USA. - 1986. - P. 118-127.

43. Thatcher J. W. Data type specification: parametrization and the power of specificationtechniques / J. W. Thatcher, E. G. Wagner, J. B. Wright / ACM Trans. On Program Language Systems. - 1982. - Vol. 4. - P. 711-732.

44. Turner D. A. A new implementation technique for applicative languages / D. A. Turner // Software Practice and Experience. - 1979. - V. 9. - P. 31-49.

45. Warren H. S. A modification of Warshall's algorithm for transitive closure of binary relations / H. S. Warren // Communs. ACM. - 1975. - Vol.18, № 4. -P. 218-220.

46. Warshall S. A Theorem on Boolean matrices / S. Warshall // J. Assoc. Computing Machinery. - 1962. - Vol. 9. - P. 11-12.

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

48. Ануреев И. С. Системы переписывания формул / И. С. Ануреев. -Новосибирск, 1997. - 22 с. - (Препр./РАН. Сиб. отд-ние. ПСИ; № 40).

49. Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: пер. с англ. / X. Барендрегт. - М.: Мир, 1985. - 606 с.

50. Вениаминов Е. М. Алгебраические методы в теории баз данных и представлении знаний / Е. М. Вениаминов. - М. : Научный мир, 2003. -184 с.

51. Биркгоф Г. Теория решеток : пер. с англ. / Г. Биркгоф. - М. : Наука, 1984. -568 с.

52. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++ : пер. с англ. / Г. Буч. - М. : Бином, 2000. - 560 с.

53. Васильев С. Н. Метод редукции и качественный анализ динамических систем, I / С. Н. Васильев // Изв. РАН. ТиСУ. - 2006. - № h— С. 21-29.

54. Васильев С. Н. Метод редукции и качественный анализ динамических систем, II / С. Н. Васильев // Изв. РАН. ТиСУ. - 2006. - № 2. - С. 5-17.

55. Воробьев С. Г. Условные системы подстановок термов и их применение в проблемно-ориентированной верификации программ / С. Г. Воробьев : автореф. дис. ... к. ф.-м. н. - Новосибирск : ВЦ СО АН СССР, 1987.

56. Закревский А. Д. Логические уравнения / А. Д. Закревский. - изд. 2-е, стереотипное. - М. : Едиториал УРСС, 2003. - 96 с.

57. Замулин А. В. Алгебраическая семантика императивного языка программирования / А. В. Замулин // Программирование. - 2003. -№6.-С. 51-64.

58. Касьянов В. Н. Графы в программировании: обработка, визуализация и применение / В. Н. Касьянов, В. А. Евстигнеев. - СПб. : БХВ-Петербург, 2003.- 1104 с.

59. Критически важные объекты и кибертерроризм. Часть 1. Системный подход к организации противодействия / О. О. Андреев и др. ; под ред. В. А. Васенина. - М. : МЦНМО, 2008. - 398 с.

60. Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия / О. О. Андреев и др.; под ред. В. А. Васенина. - М. : МЦНМО, 2008. - 607 с.

61. Кормен Т. Алгоритмы: построение и анализ : пер. с англ. / Т. Кормен, Ч. Лейзерсон, Р. Ривест. - М.: МЦНМО, 2001. - 960 с.

62. Куратовский К. Теория множеств : пер. с англ. / К. Куратовский,

A. Мостовский. - М. : Мир, 1970. - 416 с.

63. Левин В. И. Бесконечнозначная логика в задачах кибернетики /

B. И. Левин. - М. : Радио и связь, 1982. - 176 с.

64. Макконнелл С. Совершенный код. Мастер-класс : пер. с англ. /

C. Макконнелл. - М. : Русская редакция ; СПб. : Питер, 2005. - 896 с.

65. Махортов С. Д. Логические отношения на решетках / С. Д. Махортов // Вестник ВГУ. Серия Физика, математика. - Воронеж. - 2003. - № 2. -С. 203-209.

66. Махортов С. Д. Логические уравнения на решетках / С. Д. Махортов // Вестник ВГУ. Серия Физика, математика. - Воронеж. - 2004, № 2. -С.170-178.

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

68. Махортов С. Д. Интегрированная среда логического программирования LPExpert / С. Д. Махортов // Информационные технологии. - 2009. - № 12.-С. 65-66.

69. Махортов С. Д. Математические основы искусственного интеллекта: теория LP-структур для построения и исследования моделей знаний продукционного типа / С. Д. Махортов ; под ред. В. А. Васенина. - М. : МЦНМО, 2009. - 304 с.

70. Мельников С. В. Perl для профессиональных программистов. Регулярные выражения / С.В.Мельников. - М.: «Бином», 2007. - 190 с.

71. Нигиян С. А. О семантике бестиповых функциональных программ / С. А. Нигиян, С. А. Аветисян // Программирование. - 2002. - № 3. -С. 5-14.

72. Обновляемая база данных ошибок в системе Maple [Электронный ресурс]. URL: http://maple.bug-list.org/.

73. Обновляемая база данных ошибок в системе Mathematica [Электронный ресурс]. URL: //code.google.com/p/mathematica/.

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

75. Подловченко Р. И. Иерархия моделей программ / Р. И. Подловченко // Программирование. - 1981. -№ 2. - С. 3-14.

76. Расёва Е. Математика метаматематики : пер. с англ. / Е. Расёва, Р. Сикорский. - М. : Наука, 1972. - 591 с.

77. Рихтер Дж. Программирование на платформе Microsoft .NET Framework

: пер. с англ / Дж. Рихтер^ - 2-е изд.- М^: Русская Редакция72003.-- 5-12с.----

78. Рыбаков В. В. Базисы допустимых правил логик S4 и Int / В. В. Рыбаков // Алгебра и логика. - 1985. - Т. 24, № 1. - С. 87-107.

79. Рыбаков В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики / В. В. Рыбаков // Матем. сборник. - 1985. - Т. 128 (170), №3,-С. 321-338.

80. Рыбаков В. В. Независимые базисы для правил, допустимых в предтабличных логиках / В. В. Рыбаков // Алгебра и логика. - 2000. - Т. 39, № 2. - С. 206-226.

81. Рыбина Г. В. Верификация баз знаний в интегрированных экспертных системах / Г. В. Рыбина, В. В. Смирнов // Новости искусственного интеллекта. - 2005. - № 3. - С. 7-19.

82. Сикорский Р. Булевы алгебры : пер. с англ. / Р. Сикорский. - М. : Мир, 1969.-375 с.

83. Тейз А. Логический подход к искусственному интеллекту: от классической логики к логическому программированию : пер. с франц. / А. Тейз, П. Грибомон и др. - М. : Мир, 1990. - 432 с.

84. Фридл Дж. Регулярные выражения : пер. с англ. / Дж. Фридл. -СПб.: Питер, 2001.-352 с.

85. Фурман M. Е. Применение метода быстрого умножения матриц к задаче нахождения транзитивного замыкания графа / M. Е. Фурман // Докл. АН СССР. - 1970. - Т. 194, № 3. - С. 530.

86. Чечкин А. В. Математическая информатика / А. В. Чечкин. - М. : Наука, Гл. ред. физ.-мат. лит., 1991. -416 с.

Публикации автора по теме диссертации

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

2. Баранов Д. В. Компьютерная реализация устранения избыточных правил в

условных системах переписывания /'Д.В.—Баранов 7/~Программная------

инженерия. - 2013, № 6. - С. 27-32.

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

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

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

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

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

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

8. Баранов Д.В. LP-структуры в условных системах переписывания / С. Д. Махортов, Д.В. Баранов // Современные проблемы информатизации в

моделировании и социальных технологиях: сб. трудов / Под ред. О. Я.

Кравца. - ВоронежТНаучная книга, 20107-Выпг15. - С. 272-276.-----

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

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

федеральное государственное б{ ное учреждение высшего профеа

ооразотчия

Актр: Баранов Денис Владимирович 4НИ)

Змн»М 2013617287

Ддгаг.; сгуа.еик* 13 август 2013 г.

Дкщ госуздрсгъемюй репктршин

в гессгре црс*т>шм ¡¡ля эач 04 октября 2013 г.

шш&ш т

СВИДЕТЕЛЬСТВО

о государственной регистрации программы для ЭВМ

№ 2013619458

.., * 11 ЬРТегшОр11ш!гег