Главная arrow Логика arrow Правило вывода
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Правило вывода Печать

Процедура вывода того факта, что Джон — злой, действует следующим образом: найти некоторый х, такой, что х— король их— жадный, а затем вывести, что х — злой. Вообще говоря, если существует некоторая подстановка 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.