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

• Автор: Баранов, Денис Владимирович
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2013
• Место защиты: Воронеж
• Количество страниц: 120 с. : ил.

Оглавление

Введение

Глава 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угег
А.2. Класс СЬатСгеаЮг
А.З. Класс ЕциаОопаИщШсе
Литература
Введение

В ряде областей математики и информатики вводятся и используются так называемые системы переписывания. Под (формальным)
переписыванием подразумевают различные теоретические и практические методологии, определяющие процессы последовательной замены частей формул или термов формального языка, на основе некоторого множества (переписывающих) правил. В некоторых источниках [40] процесс переписывания называется редуцированием (ARS - Abstract Reduction Systems). Изначально понятие переписывания было введено для развития методологии лямбда-исчисления [49]. Впоследствии большая часть результатов и приложений на данном направлении оказалась связанной с переписыванием первого порядка [40]. Такого рода системы называются системами переписывания термов (СПТ).
В настоящее время теория систем переписывания представляет эффективный аппарат для решения важных проблем информатики, искусственного интеллекта и компьютерной алгебры. Системы переписывания термов и подобные им структуры находят применения в таких известных задачах как верификация компьютерных программ [55] и их преобразования [58], спецификация абстрактных типов данных [43, 13], реализация функциональных языков программирования [44], автоматическое доказательство теорем [20], символьное упрощение алгебраических выражений [6] и других.
Можно сказать, что в обобщенном смысле система переписывания - это формально описанная совокупность знаний (правил), разработанная для некоторой предметной области. Такие знания могут быть применены для реализации практических задач, в частности, перечисленных выше. Как и любая другая компьютерная система знаний, СПТ нуждается в управлении и сопровождении [16] - автоматизированном представлении [38], верификации [25], оптимизации [15], а также реализации процессов логического вывода.
пополнением Л( Е) относительно определенных выше дополнительных операций 1) -3).
Очевидно, что эквациональная решетка является атомно-порожденной. Нетрудно также заметить, что при пустом множестве функций и пустой области определения операции Тг(-) эквациональная решетка совпадает с булеаном, представляя собой, таким образом, его обобщение.
Как уже подчеркивалось, рассматривается условная эквациональная теория, содержащая условные правила вида з, = ,,х„ = *„ :щ = у,,...,ми -Ут .
Таким образом, предпосылка и заключение правила являются элементами Р.
Используя в качестве основы аксиомы и правила, определенные в [24], сформулируем их аналоги для условной эквациональной дедукции. Аксиомы порождаются перечисленными в п. 1.2 правилами вывода равенств. Правило вывода 2) означает наличие условного правила (аксиомы) а: f(a) для любых а = (я, = /,,...,5Я = ?„} и / е Ея; из 3) следует аксиома а: а(а) для любых а е Р и подстановки а. Правило 5) порождает аксиому а ■.Тг(а) для каждого подходящего с; £ Р. Такие условные правила в рассматриваемой логике можно также назвать тавтологиями. Еще одной очевидной тавтологией является правило а: Ъ, а,Ь еЕ при а^Ь.
Правила вывода в условной эквациональной логике таковы:
1) а:Ь~ <7(а):сг(Ь) (а,Ь е¥) для любой подстановки сг (см. аналогичное правило в [24] с исходными обозначениями);
2) а:Ь, а:с~а:Ь[]с (а,Ь,с)е¥ (возможность вывода по частям);
3) аЬ,Ь:с~а:с (а,Ь,с)&¥ (транзитивность).
2.2. Логическое замыкание и эквивалентные преобразования
~ В данном подразделе рассматриваются бинарные отношения на эквациональной решетке. Ниже будет введено понятие логического