3.8.3. Использование алгоритма унификации при автоматическом доказательстве теорем

Теперь мы можем составить эффективные программы для доказательства каких-либо теорем в простых формальных системах: ниже мы воспользуемся банком пробных задач для тестирования программ, которые возникают при использовании принципа резолюции (разд. 3.9) или в экспертных системах (гл. 7).

Однако остается проблема, которую надо решить, чтобы перенести на ЭВМ алгоритм унификации: необходимо отсечь от дерева поиска те его части, которые ведут к бесконечным Процедурам.