ОГЛАВЛЕНИЕ
Введение................................................................................................................................. 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