Введение
1. Задача проверки эквивалентности программ 4
1.1. Модели программ и задача проверки эквивалентности в рамках этих моделей 7
1.2. Логико-термальная эквивалентность стандартных схем программ 2. Задача выделения метода 13
3. Задачи унификации и антиунификации 17
4. Цели исследования. 20
5. Результаты исследования
5.1. Формулировка основных результатов 21
5.2. Методика получения результатов 24
5.3. Новизна и значимость 27
5.4. Структура работы 29
Глава 1. Основные понятия 30
1.1. Алгебра подстановок 30
1.2. Стандартные схемы программ 42
1.3. Логико-термальная эквивалентность программ 48
Глава 2. Задача проверки логико-термальной эквивалентности программ 51
2.1. Граф совместных вычислений 51
2.2. Процедура разметки графа совместных вычислений 57
2.3. Редуцированные подстановки и алгоритм редукции 64
2.4. Редуцированная антиунификация подстановок 71
2.5. Модифицированный алгоритм проверки логико-термальной эк
вивалентности, его корректность и сложность 76
Глава 3. Логико-термальная унифицируемость программ 79
3.1. Задача унификации программ 79
3.2. Алгоритм проверки логико-термальной унифицируемости программ 83
3.3. Полиномиальный алгоритм проверки логико-термальной унифицируемости программ и его корректность 90
Глава 4. Двусторонняя унификация программ 97
4.1. Задача двусторонней унификации подстановок 98
4.2. Задача ограниченного домино 101
4.3. Обоснование полноты задачи двусторонней унификации подстановок 105
4.4. Задача проверки двусторонней унифицируемости программ 113
Заключение 117
Список литературы
