8.3. СТРАТЕГИИ ОЧИЩЕНИЯ

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

нужны все резольвенции. Иными словами, достаточно выполнить резольвенции только для предложений, удовлетворяющих определенным требованиям. Мы будем обозначать через объединение множества и множества всех резольвент всех пар предложений из удовлетворяющих критерию С. Ясно, что

Про стратегию очищения, использующую критерий С, говорят, что в ней используется «резольвенция по отношению к . Для применения такой стратегии мы сначала вычисляем затем до тех пор, пока при некотором не окажется пустого предложения (обозначаемого

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

Мы рассмотрим две основные стратегии очищения, снижающие затраты усилий на перебор, а также некоторые их частные случаи.