Диссертация - Автоматический поиск натурального вывода в классической логике предикатов
Содержание
ОГЛАВЛЕНИЕ
Введение...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
