3.10.6. Стратегии
Важной проблемой, связанной с проблемой “комбинаторного взрыва” числа резолюций, остается проблема соответствующего выбора предложений и литералов для унификации. Этот выбор должен выполняться так, чтобы пустое предложение достигалось наискорейшим образом. В данном случае также не имеется общего метода. На каждом этапе конкретный выбор зависит от текущего контекста задачи. Однако некоторые стратегии выбора вне зависимости от текущего состояния процесса решения задачи, приводящие к ограничению числа возможных резолюций, все же разработаны. Пользуясь ими, важно не потерять полноты метода, т. е. гарантию получения хотя бы каким-то одним способом необходимого доказательства. Ниже мы приведем несколько таких стратегий.
Стратегия унитарности. Одно из родительских предложений должно всегда иметь единственный литерал. Эта стратегия очевидно не является полной, так как если набор предложений не содержит предложения с единственным литералом, то работа программы заканчивается. Приведенные выше доказательства могли быть получены с помощью этой стратегии.
Стратегия исходных данных. В этом случае одно из предложений является одной из гипотез или отрицанием заключения. Данная стратегия была использована в первом примере доказательства методом резолюции.
Стратегия поддержки. Используются одно из родительских предложений и доказываемое заключение или одно из предложений, вытекающих из них. Систематически удаляются от результата резолюции, двигаясь от него в обратном направлении и пытаясь подняться но дереву решения к гипотезам, запрещая всякую резолюцию вне исходной системы. Эта стратегия является полной, но очень длинной, так как она опирается на структуру, которая не всегда является эффективной.
Линейная стратегия. Одно из предложений является предложением предшествующей резольвенты, а другое — одним из ее “предков” или исходным предложением. Эта стратегия (улучшенный вариант стратегии исходных данных) является полной и одной из наиболее эффективных.
В литературе встречаются и другие стратегии. Следует отметить, что пересечение любых двух из описанных выше стратегий приводит к более ограниченному варианту, в частности результирующая стратегия может быть неполной, хотя исходные стратегии и были полными.
Теперь остается рассмотреть проблему выбора литералов. Они обычно выбираются вне родительских предложений, когда
возможны многочисленные унификации. В общем случае литералы задаются заранее и программы выбирают из них первую же пару, использование которой приводит к успешному результату. Когда нумерация литералов передана от «родителей» к резольвенте, получают стратегию, называемую стратегией замка (лок-стратегия), которая является полной и эффективной.
