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