Тема: «Автоматический поиск натурального вывода в классической логике предикатов»

Введение ..................................................................................................................................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

Часть работы