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

3.10. Принцип резолюции и язык Пролог

3.10.1. Принцип резолюции

В 1930 г. Эрбран в докторской диссертации по математике предложил оригинальный метод доказательства теорем в формальных системах первого порядка. Общая идея метода состоит в том, чтобы получить некоторое заключение С, исходя из гипотез т. е. чтобы доказать теорему

достаточно доказать противоречивость формулы

в которой отрицание заключения добавлено к исходным гипотезам. Такое доказательство может быть существенно проще прямого вывода. Для доказательства противоречивости формулы достаточно показать, что является не-теоремой, так как в ней содержится подвыражение вида Эрбран предложил эффективный способ доказательства за конечное число подстановок в формулу когда исходное выражение Т является теоремой. Ниже эта проблема рассматривается более подробно.

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