Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 110
Текст из файла (страница 110)
путем получения пустого выражения. Алгоритмический подход, применяемый в логике первого порядка, идентичен подходу в пропозициональной логике, который показан в листинге 7.5, поэтому мы не будем здесь его повторять. Вместо этого приведем два примера доказательства. Первым нз них является пример доказательства преступления, описанного в разделе 9.3.
Соответствующие высказывания, преобразованные в форму СХГ, выглядят следующим образом: Атегдсап (х) ч Иеароп (у)ч Яе11а (х, у, х) ч Ноае11е( х) ч О г1тдпа1 (х) Мзаа11е(х) ч Оепа(Мопс,х) ч Яе11а(ыеае,х,Мопс) — епету(х, Атегз са) ч лса с11е (х) Мхаа11е(х) ч Ыеарсп(х) Оепа (Мопс, №) Мзаа11е(№) Атегзсап ((чеае) Епету(Испо,лтегзса) В число этих высказываний должна быть включена также отрицаемая цель схбтбпа1 (й)еес) . Процедура доказательства по методу резолюции показана на рис. 9.7.
Обратите внимание на его структуру: единственный "хребет" начинается с целевого выражения, и операция резолюции применяется к выражениям из базы знаний до тех пор, пока не образуется пустое выражение. В этом состоит характерная особенность применения метода резолюции к базам знаний, представленным в виде хорновских выражений. В действительности выражения, расположенные вдоль главного хребта, точно соответствуют последовательным значениям целевых переменных в алгоритме обратного логического вывода, приведенном в листинге 9.3. Это связано с тем, что для резолюции всегда выбирается выражение, положительный литерал которого унифицируется с самым левым литералом "текущего" выражения в хребте; именно это происходит при обратном логическом выводе. Таким образом, обратный логический вывод в действительности представляет собой просто частный случай резолюции, в котором применяется конкретная стратегия управления для определения того, какая операция резолюции должна быть выполнена в следующую очередь.
В рассматриваемом здесь втором примере используется сколемизация и применяются выражения, которые не являются определенными. Это приводит к созданию немного более сложной структуры доказательства. На естественном языке эта задача формулируется, как описано ниже. Каждого, кто любит всех животных, кто-то любит. Любого, кто убивает животных, никто не любит. Джек любит всех животных. Кота по имени Тунец убил либо Джек, либо Любопытство. Действительно ли этого кота убило Любопытство? 4]4 Часть ]П. Знания и рассуждения Рис. 9.7.
Процедура доказательства с помощью резолюции пега, чта полковник Уэст совершил преступление Вначале представим в логике первого порядка первоначальные высказывания, некоторые фоновые знания и отрицаемую цель рд А. Чх [(ту Апдта1(у) ~ Ьочев(х,у)] ~ [Зу Ьоиеа(у,х)] В, )тх [зу Апзта1(у) л к111з(х,у)] ~ [(тк ьочев(а,х)] с. [тх Апдта1(х) ~ ьочеа(.гас)с,х) К111а(Ласк, типа) ч К111е(Сигдоа1еу,типа) Е.
Сае(Типа) Е. Чх Сае(х) => Апдта1(х) П. К111а(Сис1овдеу,Типа) Затем применим процедуру преобразования, чтобы преобразовать каждое высказывание в форму С]ч[Г; А1. Ап1та1 (К(х) ) ч Ьоиеа (0(х), х) А2. Ьочеа(х,р(х)) ч 1оиее(О(х),х) В. Ап1та1(у) ч К111а(х,у) ч Ьочеа(к,х) С. Ап1та1(х) ч Ьочев(гас)с,х) Р.
К111а(тас)с, Типа) ч К111а(Сис1овдеу, Типа) Е. Сае(Типа) СаС(х) ч Ап.ипа1(х) -~0. -~К111а(Сик1оа1су, Типа) Доказательство с помощью метода резолюции того, что кота убило Любопытство, приведено на рис. 9.8. На естественном языке это доказательство может быть перефразировано, как показано ниже. Предположим, что кота Тунца убило не Любопытство. Мы знаем, что это сделал либо Джек, либо Любопытство; в таком случае это должен был сделать Джек. Итак, Тунец— кот, а коты — животные, поэтому Тунец — животное. Любого, хто убивает животное, никто не любит, поэтому мы делаем вывод, что никто не любит Джека.
С другой стороны, Джек любит всех животных, поэтому кто-то его любит; таким образом, возникает противоречие. Это означает, что кота убило Любопытство. 415 Глава 9. Логический вывод в логике первого порядка Рцс. 9.8. Процедура доказательства с номен(ью резолюции того, что кота убило Пюбоаытство. Обракште вномание на то, что арц выводе выразкения ьонея (О (пас)с), засИ использовалась факторизация Такое доказательство действительно отвечает на вопрос "Действительно ли этого кота убило Любопытство?*', но часто требуется найти ответ на более обшие вопросы, такие как "Кто убил кота?" Резолюция позволяет это сделать, но для получения ответа требует немного больше работы. Данная цель может быть представлена в виде выражения Зы К111я ( ье, Типа), КОтОрОЕ ПОслЕ ЕГО ОтриЦания приниМаЕт в фОрме С)ч(Р вид К111я (ьв, Типа) .
Повторяя доказательство, показанное на рис. 9.8, с новой отрицаемой целью, мы получим аналогичное дерево доказательства, но с подстановкой (ыуСикбоябсу) водном из этапов. Поэтому в данном случае для поиска того, кто убил кота, достаточно проследить за связываниями, которые применяются к переменным запроса в этом доказательстве. К сожалению, в методе резолюции могут вырабатываться ъ. неконструктивные доказательства для сушествующих целей.
Например, в выражении к111я(ы, Типа) после применения операции резолюции удаляется взаимно дополнительный литерал, входяший в состав выражения к111я(гас)с, типа) м к111я(сикбоябсу, типа), с получением выражения к111я (тяс)с, типа), к которому снова применяется операция резолюции с использованием выражения — К111я(ы, Типа), что приводит к получению пустого выражения. Обратите внимание на то, что в этом доказательстве переменная ы имеет два различных связывания, а правило резолюции сообщает нам, что кто-то действительно убил кота Тунца — либо Джек, либо Любопытство.
Но в этом для нас нет ничего нового! Одно из решений данной проблемы состоит в том, чтобы регламентировать допустимые этапы резолюции так, чтобы переменные запроса могли быть связанными только один раз в каждом конкретном доказательстве; в таком случае можно будет предусмотреть применение перехода с возвратом по всем возможным связываниям. Еще одно решение состоит в добавлении специального ск литерала ответа к отрицаемой цели, которая принимает вид К111я(ы, Типа) ы Апяьеек(ы). Теперь процесс резолюции вырабатывает ответ каждый раз, когда формируется выражение, содержашее только единственный литерал ответа. Для доказательства, приведенного на рис. 9.8, таковым является выражение Апяыек(Сикбоябсу). Неконструктивное доказательство привело бы к выработке выражения лпяыек(сикфояфсу) г рлзяыек(гас)с), которое не может рассматриваться как ответ и отбрасывается.
416 Часть! П. Знания и рассуждения Полнота резолюции Любое множес~во прелложений б представимо | в бзорме импликационных выражений Допустим, что множество б невыполнимо н представлено в йорма импзнкацнонных выражений Некоторое множество Убазовых экземпляров невыполнимо Реюлюция позволяет найти противоречие в б' | В этом состоит доказательство по методу резолюции противоречия в У Теорема Эрбрана Базовая теорема резолюции Лемма поднятия Рис. 9.9. Структура доказатпсльства полноты резолюции 1.
Вначале отметим, что если множество выражений ~ невыполнимо, то существует такое конкретное множество базовых экземпляров выражений Я, что это множество также невыполнимо (теорема Эрбрана). В настоящем разделе приведено доказательство полноты резолюции. Это доказательство может пропустить без ущерба для дальнейшего понимания текста любой читатель, который готов принять его на веру. Мы покажем, что резолюция обеспечивает сж полноту опровержения (герюайоп сотпр!еуепезз), а это означает, что если множество высказываний является невыполнимым, то резолюция всегда позволяет прийти к противоречию. Резолюцию нельзя использовать для выработки всех логических следствий из множества высказываний, но она может применяться для подтверждения того, что данное конкретное высказывание следует из множества высказываний.
Поэтому резолюция может служить для поиска всех ответов на данный конкретный вопрос с помощью метода отрицаемой цели, который был описан выше в настоящей главе. Примем как истинное такое утверждение, что любое высказывание в логике первого порядка (без использования равенства) может быть перезаписано в виде множества выражений в форме СХ Р.
Это можно доказать по индукции на основе анализа формы высказывания, применяя в качестве базового случая атомарные высказывания (336). Поэтому наша цель состоит в том, чтобы доказать следующее; сзр если Я вЂ” невьтолнимое мномсество вырасчсений, то применение к Я конечного количества этапов резолюции приведет к противоречию. Схема нашего доказательства повторяет первоначальное доказательство, приведенное Робинсоном, с некоторыми упрощениями, которые были внесены Генезеретом и Нильссоном [537]. Основная структура этого доказательства показана на рис. 9.9; оно осуществляется, как описано ниже. 417 Глава 9.
Логический вывод в логике первого порядка 2. Затем прибегнем к базовой теореме резолюции (агонией геьо!шюп гпеогет), приведенной в главе 7, в которой утверждается, что пропозициональная резолюция является полной для базовых высказываний. 3.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
