Процедура вывода того факта, что Джон — злой, действует следующим образом: найти некоторый х, такой, что х— король их— жадный, а затем вывести, что х — злой. Вообще говоря, если существует некоторая подстановка 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, которая удовлетворяет условиям обобщенного правила отделения. Поэтому из p1' ,..., pn* можно вывести следующее: Subst(O, p1`) ^ … ^ Subst(O, pn) а из импликации p1 ^ … ^ pn = q — следующее: Subst(O, p1) ^ … ^ Subst(O, pn) => (O, p) Теперь подстановка O в обобщенном правиле отделения определена так, что Subst(O, p1`) = Subst(O, p1) для всех i, поэтому первое из этих двух высказываний точно совпадает с предпосылкой второго высказывания. Таким образом, выражение Subst(O, g) следует из правила отделения. Как принято выражаться в логике, обобщенное правило отделения представляет собой поднятую версию правила отделения — оно поднимает правило отделения из пропозициональной логики в логику первого порядка. В оставшейся части этой главы будет показано, что могут быть разработаны поднятые версии алгоритмов прямого логического вывода, обратного логического вывода и резолюции. Основным преимуществом применения поднятых правил логического вывода по сравнению с пропозиционализацией является то, что в них предусмотрены только те подстановки, которые требуются для обеспечения дальнейшего выполнения конкретных логических выводов. Единственное соображение, которое может вызвать недоумение у читателя, состоит в том, что в определенном смысле обобщенное правило вывода является менее общим, чем исходное правило отделения (с. 303): правило отделения допускает применение в левой части импликации любого отдельно взятого высказывания ос, а обобщенное правило отделения требует, чтобы это высказывание имело специальный формат. Но оно является обобщенным в том смысле, что допускает применение любого количества выражений pi.
|