Диссертация - АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ
Содержание
ОГЛАВЛЕНИЕ
Введение...3
Глава 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
2
2
