Введение
Глава 1. Метод дедуктивных таблиц 17
1.1 Основные понятия 18
1.2 Свойства дедуктивных таблиц 22
1.3 Дедуктивные правила 24
1.4 Порождение программы 33
1.5 Проблема комбинаторного взрыва 35
Глава 2. Доказательство с использованием волновых правил 37
2.1 Системы переписывания 39
2.2 Формирование волновых правил 41
2.2.1 Основные понятия, связанные с волновыми правилами 41
2.2.2 Алгоритм унификации различий 43
2.3 Применение волновых правил с распространением волн наружу 47
2.4 Применение волновых правил с распространением фронта волны внутрь 49
2.5 Преимущества применения волновых правил. Особенности применения волновых правил для синтеза программ 51
Глава 3. Автоматизация синтеза программ в дедуктивной таблице 53
3.1 Эвристики, ограничивающие число применимых правил 54
3.1.1 Учёт полярности логических выражений 54
3.1.2 Учёт типов термов при выводе... 55
3.2 Применение волновых правил для планирования доказательства в дедуктивной таблице 60
3.2.1 Описание метода 60
3.2.2 Построение волновых правил 61
3.2.3 Доказательство шага индукции с помощью волновых правил 63
3.2.4 Применение волновых правил для построения пути доказательства 66
Глава 4. Система синтеза функциональных программ АЛИСА 70
4.1 Язык спецификаций 70
4.2 Язык синтезируемых программ 71
4.3 Использование встроенных механизмов языка Пролог для реализации системы 75
4.4 Архитектура и схема работы системы 76
4.5 Внутреннее представление дедуктивных таблиц 79
4.6 Реализация дедуктивных правил 81
4.7 Стратегия применения дедуктивных правил 84
4.8 Реализация волновых правил 85
4.9 Результаты синтеза в системе АЛИСА 87
Заключение
