Введение
1. Формальная теория 13
1.1. Основные определения 13
1.2. Нерекурсивные и рекурсивные детерминированные С-модели 16
1.3. Постановка задачи 19
Выводы к главе 1 19
2. Алгоритмы планирования и синтеза программ 21
2.1. Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний 21
2.2. Планирование и синтез в классе НДС-моделей 24
2.2.1. Правила вывода 24
2.2.2. Трансформация вариантной части 25
2.2.3. Компиляция НДС-модели 26
2.2.4. Постановка задачи и схемы алгоритмов вывода 31
2.2.5. Извлечение программы из доказательства 38
2.3. Планирование и синтез в классе РДС-моделей 41
2.3.1. Формальная модель доказательства 41
2.3.2. Подготовка данных и алгоритм вывода на РДС-модели 44
2.4. Программная реализация 50
Выводы к главе 2 60
3. Оценка эффективности 61
3.1. Расчет вычислительных затрат на осуществление вывода в классе С-моделей 61
3.2. Получение вида зависимости вычислительных затрат от объема спецификации РДС-модели 64
3.3. Экспериментальные результаты 65
Выводы к главе 3 68
4. Интерпретация с-модели для ряда логических исчислений 69
4.1. Трансформация спецификаций языка Пролог в конструкции теории С-моделей 70
4.2. Упрощенный метод интерпретации для ряда логических исчислений 75
4.3. Реализация методов преобразования и экспериментальные результаты 78
Выводы к главе 4 83
Заключение 84
Список литературных источников 86
Список сокращений 92
Приложения 93
Приложение 1. Полная модель данных компиляции и доказательства 93
Приложение 2. XML-схема описания С-модели 94
Приложение 3. Исходный код алгоритма планирования 96
Приложение 4. Исходный код процедуры очистки результатов вывода 103
Приложение 5. Пример исходной спецификации РДС-модели для проведения тестов 105
Приложение 6. Пример спецификации в формате CNF 108
Приложение 7. Пример спецификации в формате ТМЕ 109
Приложение 8. Пример спецификации в формате TPTP-FOF ПО
Приложение 9. Пример спецификации для дескриптивной логики на языке OWL Ill
