Резолюция с входными высказываниями

В стратегии резолюции с входными высказываниями (input resolution) на каждом этапе резолюции комбинируется одно из входных высказываний (из базы знаний или запроса) с некоторым другим высказыванием. В доказательстве, показанном на рис. 9.7, использовались только этапы резолюции с входными высказываниями и поэтому дерево доказательства имело характерную форму в виде единого "хребта" с отдельными высказываниями, комбинирующимися с этим хребтом. Очевидно, что пространство деревьев доказательства такой формы меньше по сравнению с пространством всех возможных графов доказательства. В хорновских базах знаний как своего рода стратегия резолюции с входными высказываниями может рассматриваться правило отделения, поскольку при использовании этого правила некоторая импликация из первоначальной базы знаний комбинируется с некоторыми другими высказываниями. Таким образом, нет ничего удивительного в том, что метод резолюции с входными высказываниями является полным применительно к базам знаний, которые находятся в хорновской форме, но в общем случае он неполон. Стратегия линейной резолюции (linear resolution) представляет собой небольшое обобщение, в котором допускается применять в одной операции резолюции высказывания р и Q, если Р находится в первоначальной базе знаний или Р является предком Q в дереве доказательства. Метод линейной резолюции является полным.