Введение
1 Отраженная логика доказательств . 11
1.1 Основные определения 11
1.2 Конструкция наименьшей модели 13
1.3 Отраженный фрагмент логики доказательств 18
1.4 Сложность фрагментов логики доказательств 20
2 Типизация термов в рефлексивной комбинаторной логике . 26
2.1 Определение правильно построенных формул RCL 26
2.2 Типизация подтермов 28
2.3 Типы в RCL 32
2.4 Соответствие между правильно построенными формулами и типами 37
2.5 Восстановление типов 41
3 Выводимость в рефлексивной комбинаторной логике . 48
3.1 Выводимость из гипотез в RCL 48
3.2 Устранение сечения в RCLTG 52
3.3 Разрешимость RCLTG 67
3.4 Оценки сложности 72
