Введение
ГЛАВА 1. Обзор предметной области 13
1.1. Введение 13
1.2. Основные определения и обозначения 13
1.3. Интуиционизм и конструктивизм: краткая историческая справка 19
1.4. Программы автоматического логического вывода и области их применения 23
1.5. Методы поиска вывода для логики первого порядка 30
1.6. Заключение 43
ГЛАВА 2. Построение интуиционистского исчисления обратного метода 45
2.1. Введение 45
2.2. Основные определения и обозначения 46
2.3. Универсальная методика построения логических исчислений, подходящих для применения обратного метода 56
2.4. Пример односукцедентного исчисления обратного метода 57
2.5. Построение многосукцедентного исчисления обратного метода 60
2.6. Особенности построенного многосукцедентного исчисления 75
2.7. Пример 76
2.8. Модификации исчислений 80
2.9. Заключение 81
ГЛАВА 3. Разработка стратегий поиска вывода для интуиционистских исчислений обратного метода 83
3.1. Введение 83
3.2. Основные определения и обозначения 84
3.3. Стратегия поглощения секвенций 84
3.4. Стратегия упрощения секвенций 88
3.5. Стратегии удаления недопустимых секвенций з
3.6. Стратегия тривиального сокращения 99
3.7. Сингулярная стратегия 99
3.8. Совместимость стратегий 100
3.9. Применение стратегий к модификациям исчислений
3.10. Примеры 103
3.11. Заключение 110
ГЛАВА 4. Алгоритм поиска вывода и программная реализация обратного метода 112
4.1. Введение 112
4.2. Основные определения и обозначения 112
4.3. Алгоритм поиска вывода 113
4.4. Программа для автоматического поиска вывода WhaleProver 117
4.5. Результаты экспериментов на задачах из библиотеки ILTP 120
4.6. Сравнение программы WhaleProver с существующими программами АЛВ для интуиционистской логики первого порядка 128
4.7. Интерактивный режим 133
4.8. Заключение 138
Заключение 141
Список сокращений и условных обозначений 143
Список использованной литературы 144
