Главная > Интеллектуальные системы > Системы искусственного интеллекта
<< Предыдущий параграф
Следующий параграф >>
<< Предыдущий параграф Следующий параграф >>
Макеты страниц

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

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

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

<< Предыдущий параграф Следующий параграф >>
Оглавление