Процедура вывода того факта, что Джон — злой, действует следующим образом: найти некоторый х, такой, что х— король их— жадный, а затем вывести, что х — злой. Вообще говоря, если существует некоторая подстановка 9, позволяющая сделать предпосылку импликации идентичной высказываниям, которые уже находятся в базе знаний, то можно утверждать об истинности заключения этой импликации после применения 9. В данном случае такой цели достигает подстановка {х/ John}.

Фактически можно обеспечить выполнение на этом этапе вывода еще больше работы. Предположим, что нам известно не то, что жаден Джон— Greedy(John), а что жадными являются все: Vy Greedy (у).

Но и в таком случае нам все равно хотелось бы иметь возможность получить заключение, что Джон зол — Evil (John), поскольку нам известно, что Джон — король (это дано) и Джон жаден (так как жадными являются все). Для того чтобы такой метод мог работать, нам нужно найти подстановку как для переменных в высказывании с импликацией, так и для переменных в высказываниях, которые должны быть согласованы. В данном случае в результате применения подстановки {х/John, у/John} к предпосылкам импликации King(x) и Greedy(х) и к высказываниям из базы знаний King (John) и Greedy [у) эти высказывания становятся идентичными. Таким образом, теперь можно вывести заключение импликации.

Такой процесс логического вывода может быть представлен с помощью единственного правила логического вывода, которое будет именоваться обобщенным правилом отделения (Generalized Modus Ponens).

В этом правиле имеется n+1 предпосылка: п атомарных высказываний n± и одна импликация. Заключение становится результатом применения подстановки 0 к следствию.

Можно легко показать, что обобщенное правило отделения — непротиворечивое правило логического вывода. Прежде всего отметим, что для любого высказывания р (в отношении которого предполагается, что на его переменные распространяется квантор всеобщности) и для любой подстановки 0 справедливо следующее правило: p =Subst(O, p)

Это правило выполняется по тем же причинам, по которым выполняется правило конкретизации высказывания с квантором всеобщности. Оно выполняется, в частности, в любой подстановке 0, которая удовлетворяет условиям обобщенного правила отделения. Поэтому из p₁' ,..., p_n* можно вывести следующее:

Subst(O, p₁`) ^ … ^ Subst(O, p_n)

а из импликации p₁ ^ … ^ p_n = q — следующее:

Subst(O, p₁) ^ … ^ Subst(O, p_n) => (O, p)

Теперь подстановка O в обобщенном правиле отделения определена так, что Subst(O, p_1`) = Subst(O, p₁) для всех i, поэтому первое из этих двух высказываний точно совпадает с предпосылкой второго высказывания. Таким образом, выражение Subst(O, g) следует из правила отделения.

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