УНИФИКАЦИЯ И ПОДНЯТИЕ

В предыдущем разделе описан уровень понимания процесса вывода в логике первого порядка, который существовал вплоть до начала 1960-х годов. Внимательный читатель (и, безусловно, специалисты в области вычислительной логики, работавшие в начале 1960-х годов) должен был заметить, что подход на основе пропозицио-нализации является довольно неэффективным. Например, если заданы запрос Evil (х) и база знаний, приведенная в уравнении 9.1, то становится просто нерациональным формирование таких высказываний, как King {Richard) А Greedy {Richard) => Evil {Richard). И действительно, для любого человека вывод факта Evil {John) из следующих высказываний кажется вполне очевидным:
Vx King{x) A Greedy{x) => Evil{x) King{John) Greedy {John)
Теперь мы покажем, как сделать его полностью очевидным для компьютера.
Правило вывода в логике первого порядка
Процедура вывода того факта, что Джон — злой, действует следующим образом: найти некоторый х, такой, что х— король их — жадный, а затем вывести, что х — злой. Вообще говоря, если существует некоторая подстановка 0, позволяющая сделать предпосылку импликации идентичной высказываниям, которые уже находятся в базе знаний, то можно утверждать об истинности заключения этой импликации после применения 0. В данном случае такой цели достигает подстановка {х/ John}.
Фактически можно обеспечить выполнение на этом этапе вывода еще больше работы. Предположим, что нам известно не то, что жаден Джон — Greedy(John), а что жадными являются все:
Vy Greedy (у) (9.2)
Но и в таком случае нам все равно хотелось бы иметь возможность получить заключение, что Джон зол — Evil (John), поскольку нам известно, что Джон — король (это дано) и Джон жаден (так как жадными являются все). Для того чтобы такой метод мог работать, нам нужно найти подстановку как для переменных в высказывании с импликацией, так и для переменных в высказываниях, которые должны быть согласованы. В данном случае в результате применения подстановки {х/ John, у/ John} к предпосылкам импликации King(x) и Greedy(x) и к высказываниям из базы знаний King (John) и Greedy (у) эти высказывания становятся идентичными. Таким образом, теперь можно вывести заключение импликации.
Такой процесс логического вывода может быть представлен с помощью единственного правила логического вывода, которое будет именоваться обобщенным правилом отделения (Generalized Modus Ponens): для атомарных высказываний pi5 Pi * ид, если существует подстановка 0, такая, что Subst (0,Pi' ) =Subst (0,Pi), то для всех i имеет место следующее:
Pi', Р2' Ai', (Pi Л Р2 Л ... Л рп => д)
Subst(8fq)
В этом правиле имеется л+1 предпосылка: л атомарных высказываний р±' и одна импликация. Заключение становится результатом применения подстановки 0 к следствию д. В данном примере имеет место следующее:
Pi1 — это King(John) Pi — это King(x)
Р21 — это Greedy (у) р2 — это Greedy(x)
0 — это {х/John,у/John} q — это Evil(x)
Subst (0,g) - это Evil(John)
Можно легко показать, что обобщенное правило отделения — непротиворечивое правило логического вывода. Прежде всего отметим, что для любого высказывания р (в отношении которого предполагается, что на его переменные распространяется квантор всеобщности) и для любой подстановки 0 справедливо следующее правило:
р И Subst(9,р)
Это правило выполняется по тем же причинам, по которым выполняется правило конкретизации высказывания с квантором всеобщности. Оно выполняется, в частности, в любой подстановке 0, которая удовлетворяет условиям обобщенного правила отделения. Поэтому из рг' ,..., рп * можно вывести следующее:
Subst (0,pi') л ... л Subst (9,pn')
а из импликации р1 А ... л pn => д—следующее:
Subst (0,pi) л ... л Subst (0,рп) => Subst (0,g)
Теперь подстановка 0 в обобщенном правиле отделения определена так, что Subst (0,Pi1 ) = Subst (0,Pi) для всех i, поэтому первое из этих двух высказываний точно совпадает с предпосылкой второго высказывания. Таким образом, выражение Subst (0, g) следует из правила отделения.
Как принято выражаться в логике, обобщенное правило отделения представляет собой поднятую версию правила отделения — оно поднимает правило отделения из пропозициональной логики в логику первого порядка. В оставшейся части этой главы будет показано, что могут быть разработаны поднятые версии алгоритмов прямого логического вывода, обратного логического вывода и резолюции, представленных в главе 7. Основным преимуществом применения поднятых правил логического вывода по сравнению с пропозиционализацией является то, что в них предусмотрены только те подстановки, которые требуются для обеспечения дальнейшего выполнения конкретных логических выводов. Единственное соображение, которое может вызвать недоумение у читателя, состоит в том, что в определенном смысле обобщенное правило вывода является менее общим, чем исходное правило отделения (с. 303): правило отделения допускает применение в левой части импликации любого отдельно взятого высказывания ос, а обобщенное правило отделения требует, чтобы это высказывание имело специальный формат. Но оно является обобщенным в том смысле, что допускает применение любого количества выражений р± •.







Материалы

Яндекс.Метрика