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

Более того, выражения, которые участвуют на каждом этапе, могут быть выбраны из фоновых знаний Background, из описаний примеров Descriptions, из отрицаемых выражений в множестве Classifications или из выражений, выдвинутых в качестве гипотезы, которые уже были сформированы в дереве обратной резолюции. Такое большое количество возможностей означает, что без дополнительного управления возникает большой коэффициент ветвления (и поэтому поиск становится неэффективным). В реализованных на практике системах ILP был опробован целый ряд подходов к управлению поиском, в том числе подходы, описанные ниже.

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

, приведенное выше.

2.    Могут быть наложены ограничения на стратегию доказательства. Например, в главе 9 было показано, что линейная резолюция — это полная, ограниченная стратегия, которая позволяет создавать только такие деревья доказательства, которые имеют линейную структуру ветвления (как на рис. 19.9).