Введение
Глава 1. Автоматический поиск натурального вывода: история вопроса 9
1.1. Натуральный вывод как тип логического вывода 9
1.2. История создания систем автоматического поиска вывода 16
1.3. Автоматический поиск вывода в натуральном исчислении 23
Глава 2. Анализ системы натурального вывода BMV 28
2.1. Формулировка системы BMV 28
2.2. Семантическая непротиворечивость системы BMV 35
Глава 3. Алгоритм поиска вывода в системе BMV 43
3.1. Изменение формулировки системы BMV 43
3 2. Унификация 47
3.3. Правила поиска вывода в системе BMV 53
3.4. Описание алгоритма поиска вывода в системе BMV 60
Глава 4. Анализ алгоритма поиска вывода в системе BMV 81
4.1. Семантическая непротиворечивость алгоритма 81
4.2. Свойства алгоритма 85
4.3. Семантическая полнота алгоритма 96
Заключение 102
Литература 106
