Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 78
Текст из файла (страница 78)
В действительности, если можно было бы составить функцию определения преемника для выработки всех возможных вариантов применения правил логического вывода, это позволило бы использовать для формирования доказательств все алгоритмы поиска, приведенные в главах 3 и 4. Таким образом, вместо трудоемкого перебора моделей может применяться более эффективный способ логического вывода — формирование доказательств. Поиск может проходить в прямом направлении, от первоначальной базы знаний, и осуществляться путем использования правил логического вывода для получения целевого высказывания, или же этот поиск может проходить в обратном направлении, от целевого высказывания, в попытке найти цепочку правил логического вывода, ведущую от первоначальной базы знаний.
Ниже в этом разделе рассматриваются два семейства алгоритмов, в которых используются оба эти подхода. Из того факта, что задача логического вывода в пропозициональной логике является ХР-полной, следует, что в наихудшем случае поиск доказательств может оказаться ие более эффективным по сравнению с перебором моделей. Однако во многих практических случаях са- поиск доказательства моясет быть чрезвычайно эффективным просто потому, что в нем могут игнорироваться не относящиеся к делу (нерелеватпные) высказывания, независимо от того, насколько велико их количество. Например, в приведенном выше доказательстве, ведущем к высказыванию — Р, з м — Р,, ие Упоминались высказываниЯ В, „Р, „Р,, или Р,, Их можно было не рассматривать, поскольку целевое высказывание, Р, „присутствует только в высказывании и,; остальные высказывания из состава я, присутствуют только в и, и Рю поэтомУ пз.
Вз и пз не имеют никакого отношениЯ к доказательствУ. Те же Рассуждения останутся справедливыми, если в базу знаний будет введено иа миллион больше высказываний; с другой стороны, в этом случае простой алгоритм перебора строк в истиниостной таблице был бы буквально подавлен из-за экспоненциального взрыва, вызванного стремительным увеличением количества моделей.
Это свойство логических систем фактически вытекает из гораздо более фундаментального свойства, называемого сь монотонностью. Согласно этому свойству, множество высказываний, которые могут быть получены путем логического вывода, возрастает лишь по мере добавления к базе знаний новой информации". Для любых высказываний а и ]3 справедливо следующее: если КВ е а, то КВ ь ]3 Г- а Например, предположим, что база знаний содержит дополнительное утверждение р, согласно которому в этом экземпляре мира вампуса имеется точно восемь ям.
Эти знания могут помочь агенту прийти к дополнительным заключениям, но ие способны поставить под сомнение какое-либо уже сделанное заключение а, в частности вывод о том, что в квадрате ] 1, 2 ] нет ямы. Монотонность означает, что правила логического вывода могут применяться каждый раз, когда в базе знаний обна- 'ь Немонотоняые логики, в которых нарушается свойство монотонности, отражают типичную черту человеческого мышления — способность менять свое мнение. Эти варианты логики рассматриваются в разделе 10.7. 306 Часть Н!. Знания и рассуждения руживаются подходящие предпосылки, — полученное заключение будет следствием из данного правила, независимо от того, чта еше находится в базе знаний. Резолюция Выше было показано, что все рассматривавшиеся до сих пор правила логического вывода являются непротиворечивыми, но вопрос об их полноте применительно к алгоритмам логического вывода, в которых они используются, еше не обсуждался.
Алгоритмы поиска, такие как поиск с итеративным углублением (с. 133), являются полными в том смысле, что позволяют найти любую достижимую цель, но если доступные правила логического вывода неадекватны, то цель становится недостижимои; это означает, что не существует доказательства, в котором могли бы применяться только эти правила логического вывода. Например, если мы откажемся от использования правила удаления двухсторонней импликации, то не сможем довести до конца доказательство, изложенное в предыдушем разделе.
А в настояшем разделе представлено единственное правило логического вывода, правило резолюции, позволяющее получить алгоритм логического вывода, который становится полным в сочетании с любым полным алгоритмом поиска. Начнем с использования простой версии правила резолюции в мире вампуса.
Рассмотрим шаги, ведущие вверх на рис. 7.3, ас агент возврашается из квадрата [2, 1] в квадрат [1, 11, а затем переходит в квадрат [1, 21, где он чувствует неприятный запах, но не ощущает ветерка. Введем следующие дополнительные факты в базу знаний: К„г Вз,г Км: Вз,г е:з (Рз,з 'г Рг,г х Рз з) С помощью того же процесса, который привел к получению высказывания кьь приведенного выше, мы теперь можем сделать заключение об отсутствии ям в квадратах [2, 2] и [1, 3] (напомним, что в отношении квадрата [1, 1] уже известно, что в нем нет ям): Кзз: Рг г Кзз . 'Рз з Кроме того, можно применить к высказыванию кз правило удаления двухсторонней импликации, после чего применить к полученному результату в сочетании с высказыванием к, правило отделения, чтобы выяснить тот факт, что по меньшей мере водном из квадратов [1, 1], [2, 21 или [3, 1] есть яма: Кзз: Рз з з' Рг г зг Рз з Именно здесь возникают условия, позволяющие впервые использовать правило РезолюЦии (пРавило УстРанениЯ пРотивоРечиЯ): литеРал — Р,, в высказывании Кз и противоположный литералу Р,, в высказывании К„, устраняется, что приводит к получению следующего высказывания: Яззг Рз,г зз Рз,з Соответствуюший ход рассуждения можно выразить словами таким образом: если по меньшей мере водном из квадратов [1, 1), [2, 2] или [3, 1] имеется яма, но ее нет в квадрате [2, 2], то яма должна быть, по крайней мере, в квадрате [1, 1] 307 Глава 7.
Логические агенты или [3,1]. Аналогичным образом, устраняется литерал †,Р,, в высказывании и„ пРотивоположный литеРалУ Р, „ в высказывании Дгм что пРивоДит к полУчению следующего высказывания: Вы: Ркг Соответствующий ход рассуждений можно выразить словами таким образом: если по меньшей мере в одном из квадратов [1, 1] или «3, 1] есть яма, но ее нет в квадрате [1, 1], то она находится в квадрате [3, 1] .
Эти два последних этапа логического вывода представляют собой примеры применения 'дк правила логического вывода, называемого правилом единичной резолюции: ч[я, т Г,ч...чт,,чсгыч...ч где каждое нз выражений Г представляет собой литерал, а выражения г', и гл являются 'ж взаимно обрап~ыми литералами (т.е. такими литералами, что один из них является отрицанием другого). Таким образом, в правиле единичной резолюции берется Ж выражение (дизъюнкция лнтерзлов) и еше один литерал, после чего формируется новое выражение. Обратите внимание на то, что этот единственный литерал может рассматриваться как дизьюикция из одного литерала, называемая также 'в. единичным вырзжепиель Правило единичной резолюции может быть также обобшено до правила полной Ъ. резолюции: тгч ..чль Г~ч...чГ-чтг;ч.чгхчглгч,чмгчтгч...чав где г"„и гл, — взаимно обратные литералы.
Если бы мы имели дело только с выражениями, имеющими длину два, то могли бы записать данное правило следующим образом: Это означает, что в правиле резолюции берутся два выражения и вырабатывается новое выражение, содержащее все литералы двух первоначальных выражений, за исключением двух взаимно обратных литералов. Например, может иметь место такой логический вывод: Р ч Рз, Рк ч -~Ржг РЗ г ч Ржз Процесс применения правила резолюции связан с необходимостью выполнения еще одного формального требования: результирующее высказывание должно содержать только по одной копии каждого литерала".
Операция удаления дополнительных копий литералов называется 'а. факторизацией. Например, после удаления про- " Если некоторое выражение рассматривается как множество лнтералов, то такое правило сокрагдення применяется автоматически. Использование лля логических выражений системы обозначений в виде множеств позволяет сделать правило резолюции более понятным, но за счет введения дополнительных обозначений. 308 Часть П1. Знания и рассуждения тивоположныхдругдругулитералов в выражениях (А м В) и (А м ~В) будет получено выражение (А г А), которое следует сократить до А.
Непротиворечивость правила резолюции можно легко доказать, рассматривая литерал гг. Если литерал (г является истинным, то литерал т; является ложным, и поэтомувыражениет, м ... ч тз, м гп,„ы ... г т„должнобытьистинным,поскольку дано, что истинно выражение т, м ., м гп„. Если литерал (г является ложным, то должно быть истинным выражение Р, ч ..,м (,, г (,„м.,.м („ поскольку дано, что истинно выражение (, м ... г („.