ОГЛАВЛЕНИЕ

Введение................................................................................................................................. 3

Глава 1. Автоматический поиск натурального вывода: история вопроса........................

£ 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