8.5. СТРАТЕГИЯ ПОДДЕРЖИВАЮЩЕГО МНОЖЕСТВА

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

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