Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 101
Текст из файла (страница 101)
Кдпд(до(зп) л Ь гееду(до)2п) =) Ецз1(доил) Канд(ятспаюй л бгееду(язслакд) =-> Еу11(лзс)захд) Ктпд(уае)1ех(аппп)) л Бкееду(7ае(зех(до(зп)) ~ Езг11(7аг)зек(до)зп)) Согласно правилу сь конкретизации высказывания с квантором всеобщности (сокрагценно ()! — !)п1уегва!! пз(ап((айоп), мы можем вывести логическим путем любое высказывание, полученное в результате подстановки базового тсрма (герма без переменных) вместо переменной, на которую распространяется квантор всеобшности'. Чтобы записать это правило логического вывода формально, воспользуемся понятием подстановки, введенным в разделе 8.3.
Допустим, что Бц)зэк (О, а) обозначает результат применения подстановки 0 к высказыванию а. В таком случае данное правило для любой переменной у и базового терма д можно записать следуюшим образом: нц)звс((у/д),а) ' Эти подстановки не следует путать с расширенными интерпретациями, которые использовались для определения семантики кванторов. В подстановке переменная заменяется термом (синтаксической конструкцией) для получения нового высказывания, тогда как любая интерпретация отображает некоторую переменную на объект в проблемной области. 382 Часть И1.
Знания и рассуждения Например, три высказывания, приведенные выше, получены с помошью подстановок (х/.тоЛп», (х/нзсйахЯ и (х/Гасйех(,тоЛН) ). Соответствующее правило 'гв конкретизации высказывания с квантором существования (Ехияепба!!пмапбагюп — Е1) для квантора существования является немного более сложным. Для любых высказывания а, переменной о и константного символа )г, который не появляется где-либо в базе знаний, имеет место следуюшее: яп)оас ( (е/)г), а) Например, из высказывания Зх Сгоеп (х) а Опнеао) (х, Оолп) можно вывести высказывание Сгоеп(С,) х Оплеаг) (Сг, толп) при условии, что константный символ С, не появляется где-либо в базе знаний. По сути, в этом высказывании с квантором существования указано, что существует некоторый объект, удовлетворяюший определенному условию, а в процессе конкретизации просто присваивается имя этому объекту.
Естественно, что это имя не должно уже принадлежать другому объекту. В математике есть прекрасный пример: предположим, мы открыли, что имеется некоторое число, которое немного больше чем 2,71828 и которое удовлетворяет уравнению с) (х") /с)у=х'для х. Этому числу можно присвоить новое имя, такое как е, но было бы ошибкой присваивать ему имя существующего объекта, допустим, я. В логике такое новое имя называется 'ох сколемовской константой. Конкретизация высказывания с квантором существования — это частный случай более обшего процесса, называемого сколемизапией, который рассматривается в разделе 9.5.
Конкретизация высказывания с квантором существования не только сложнее, чем конкретизация высказывания с квантором всеобщности, но и играет в логическом выводе немного иную роль. Конкретизация высказывания с квантором всеобщности может применяться много раз для получения многих разных заключений, а конкретизация высказывания с квантором сушествования может применяться только один раз, а затем соответствуюшее высказывание с квантором существования может быть отброшено. Например, после того как в базу знаний будет добавлено высказывание К111 (/гипс)ехеп, Исс1га), становится больше нс нужным высказывание Зх к111(х, )/Зссхгп) .
Строго говоря, новая база знаний логически не эквивалентна старой, но можно показать, что она ох эквивалентна с точки зрения логического вывода, в том смысле, что она выполнима тогда и только тогда, когда выполнима первоначальная база знаний. Приведение к пропознцнонвльному логическому выводу Получив в свое распоряжение правила вывода высказываний с кванторами из высказываний без кванторов, мы получаем возможность привести вывод в логике первого порядка к выводу в пропозициональной логике.
В данном разделе будут изложены основные идеи этого процесса, а более подробные сведения приведены в разделе 9.5. Основная идея состоит в следуюшем: по аналогии с тем, как высказывание с квантором существования может быть заменено одной конкретизацией, высказы- 383 Глава 9. Логический вывод в логике первого порядка вание с квантором всеобщности может быть заменено множеством всех возможных конкретизаций. Например, предположим, что наша база знаний содержит только такие высказывания: Чх Кдпд(х) л Огееау(х) ~ Еу11(х) Кдпд( дода) Огеес(у(дода) Вгогдег(ядслагс, Юодп) (9.1) Затем применим правило конкретизации высказывания с квантором всеобшности к первому высказыванию, используя все возможные подстановки базовых термов из словаря этой базы знаний — в данном случае (х/ тоЛп) и (х/ЯусЛагЯ.
Мы получим следующие высказывания: Кдпд(дода) л агеесу(дслп) ~ Еу11(.Толп) кдпд(ядслага) л дгеесу(е1слагс) => еч11(К1слагс) и отбросим высказывание с квантором всеобшности. Теперь база знаний становится по сути пропозициональной, если базовые атомарные высказывания (КЗпд(гоЛп), Сгеес(у( тоЛп) и т.д.) рассматриваются как пропозициональные символы. Поэтому теперь можно применить любой из алгоритмов полного пропозиционального вывода из главы 7 для получения таких заключений, как еъ 11 ( гоЛп ) .
Как показано в разделе 9.5, такой метод 'а. пропозиционализации (преобразования в высказывания пропозициональной логики) может стать полностью обобщенным; это означает, что любую базу знаний и любой запрос в логике первого порядка можно пропозиционализировать таким образом, чтобы сохранялось логическое следствие. Таким образом, имеется полная процедура принятия решения в отношении того, сохраняется ли логическое следствие... или, возможно, такой процедуры нет. Дело в том, что сушествует такая проблема: если база знаний включает функциональный символ, то множество возможных подстановок базовых термов становится бесконечным! Например, если в базе знаний упоминается символ еа сЛег, то сушествует возможность сформировать бесконечно большое количество вложенных термов, таких как Еа СЛег(уаСЛег(уаСЛег(доЛп) ) ) .
А применяемые нами пропозициональные алгоритмы сталкиваются с затруднениями при обработке бесконечно большого множества высказываний. К счастью, имеется знаменитая теорема, предложенная Жаком Эрбраном [650), согласно которой, если некоторое высказывание следует из первоначальной базы знаний в логике первого порядка, то существует доказательство, которое включает лишь конечное подмножество этой пропозиционализированной базы знаний. Поскольку любое такое подмножество имеет максимальную глубину вложения среди его базовых термов, это подмножество можно найти, формируя вначале все конкретизации с константными символами (кдслагс) и толп), затем все термы с глубиной 1 (еаслег(к1слагс)) и еаслег(толп) ), после этого все термы с глубиной 2 и т.д.
до тех пор, пока мы не сможем больше составить пропозициональное доказательство высказывания, которое следует из базы знаний. Выше был кратко описан один из подходов к организации вывода в логике первого порядка с помощью пропозиционализации, который является полным, т.е. позволяет доказать любое высказывание, которое следует из базы знаний. Это — важное достижение, если учесть, что пространство возможных моделей является бесконечным.
С другой стороны, до тех пор пока это доказательство не составлено, мы не 384 Часть П1. Знания и рассуждения знаем, следует ли данное высказывание из базы знаний! Что произойдет, если это высказывание из нее не следует? Можем ли мы это определить? Как оказалось, для логики первого порядка это действительно невозможно.
Наша процедура доказательства может продолжаться и продолжаться, вырабатывая все более и более глубоко вложенные термы, а мы не будем знать, вошла ли она в безнадежный цикл или до получения доказательства остался только один шаг. Такая проблема весьма напоминает проблему останова машин Тьюринга. Алан Тьюринг [1518] и Алонсо Черч [255[ доказали неизбежность такого состояния дел, хотя и весьма различными способами. сь" Вопрос о следствии для логики первого порядка является полуразрешимым; зто означает, чпю существуют алгоритмы, которые позволяют найти доказательство для любого высказывания, которое следует из базы знаний, но нет таких алгоритмов, которые позволяли бы также определить, что не существует доказательства для камсдого высказывания, ко?парие не следуеп? из базы знаний.
9.2. УНИФИКАПНЯ И ПОДНЯТИЕ В предыдущем разделе описан уровень понимания процесса вывода в логике первого порядка, который существовал вплоть до начала 1960-х годов. Внимательный читатель (и, безусловно, специалисты в области вычислительной логики, работавшие в начале 1960-х годов) должен был заметить, что подход на основе пропозиционализации является довольно неэффективным. Например, если заданы запрос ри1 1 (х) и база знаний, приведенная в уравнении 9.1, то становится просто нерациональным формирование таких высказываний, как Кзпо(ЯЗс??акс?) л Скеес?у(??ус)закс?) ~ Еи11(кус)загх?).
И действительно, для любого человека вывол факта Киб 1 ( ~о??п) из следующих высказываний кажется вполне очевидным: Чх К?пя(х) ь Сгееау(х) => Ки11 (х) К?по(лона) е сеес?у (.топо ) Теперь мы покажем, как сделать его полностью очевидным для компьютера. Правило вывода в логике первого порядка Процедура вывода того факта, что Джон — злой, действует следующим образом: найти некоторый х, такой, что х — король и х — жадный, а затем вывести, что х— злой.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
