Искусственный интеллект

Как уже говорилось, Робинсон предложил использовать обобщенную резолюцию для создания стратегии вывода, в основе которой лежит опровержение,или доведение до противоречия. Идея этой стратегии вывода состоит в следующем. Предположим необходимо вывести истинность целевой формулы а. Делается опровержение этой формулы, т.е. предполагается истинным ее отрицание -i а. Эта формула, являющаяся отрицанием целевой, заносится в базу знаний. После этого, если, начиная обратный вывод с формулы -, а, удастся установить противоречие, т.е. вывести пару литералов Р и -! Р, то считается, что сделанное предположение об истинности отрицания целевой формулы ошибочно (опровергнуто) и делается заключение об истинности целевой формулы а. Если в результате рассмотрения всех возможных путей вывода такого противоречия установить не удастся, то считается, что целевая формула является ложной.