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

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

(9.2)

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

Такой процесс логического вывода может быть представлен с помощью единственного правила логического вывода, которое будет именоваться обобщенным правилом отделения (Generalized Modus Ponens): для атомарных высказываний pi Pi' и q, если существует подстановка Θ, такая, что, то для всех i имеет место следующее: