12.2. Простые стратегии очищения
12.2.0. Очищение
Применение принципа резолюции без ограничений приводит к слишком большому множеству предложений, чтобы с ним можно было работать на практике. Рассмотрим вывод пустого 
или какого-нибудь другого предложения при помощи резолюции и
соответствующее графовое представление в виде дерева (рис. 12.4). В отличие от деревьев, которые мы изучали при решении задач, это дерево „растет" вниз от листьев, представляющих исходные предложения, к корню.
Рис. 12.4. Дерево вывода.
Каждый узел, не являющийся листом (в том числе и корень), представляет предложение, полученное в результате резолюции двух предложений, расположенных непосредственно над ним.
На рис. 12.4 показан только один из выводов. Можно было бы построить и другие выводы, распространяющиеся от исходных предложений в иных направлениях (рис. 12.5).
Рис. 12.5. Распространение вывода от исходных предложений.
Некоторые из них приведут к пустому предложению 
и потому будут непротиворечивыми доказательствами невыполнимости. В других случаях пустое предложение не будет получено, и, быть может, процесс никогда не закончится. Чтобы применять резолюцию на практике, надо уметь заранее определять, какие выполнять резолюции и какие производить выводы.
Алгоритм, осуществляющий отбор резолюций, называется стратегией очищения. Правило, изменяющее порядок, в котором пробуются резолюции, но не изменяющее их числа, будет называться стратегией упорядочения. Стратегии очищения разбиваются на три класса: синтаксические, семантические и стратегии, учитывающие ход вывода. Применение синтаксической стратегии предполагает отбор предложений, участвующих в резолюции, по критерию, основанному на их структурных свойствах, таких, как число содержащихся в них литералов безотносительно интерпретации атомов рассматриваемого предложения как истинных или ложных для определенной модели. Применение семантической стратегии предполагает совсем обратное, поскольку отбираются предложения, про которые известно, что они истинны только для определенных моделей. Применение стратегии, учитывающей ход вывода, предполагает отбор предложений для последующей резолюции на основе хода уже осуществленного вывода этих предложений. Например, в случае стратегии исходных данных в каждой резолюции должно участвовать по крайней мере одно предложение из исходного множества предложений S.
Стратегии очищения составляют основу для написания программ доказательства теорем, работающих только с ограниченным подмножеством всех возможных резолюций. Для того чтобы доказать, что такая программа дает непротиворечивое доказательство теорем, необходимо показать, что для рассматриваемого ограниченного множества резолюций, определяемого данной стратегией очищения, выполняется теорема полноты. Трудность доказательства полноты сильно зависит от выбранной стратегии. Как правило, здесь мы не приводим доказательств, а отсылаем интересующегося читателя к соответствующим работам.
Некоторые стратегии очищения довольно сложны, и они будут обсуждаться каждая отдельно. Другие, кратко обсуждаемые в настоящем разделе, просты и легко реализуемы. Что же касается стратегий упорядочения, то практически все полезные стратегии просты, так что мы их тоже обсудим здесь.
