ШАБЛОНЫ ФОРМИРОВАНИЯ РАССУЖДЕНИЙ В ПРОПОЗИЦИОНАЛЬНОЙ ЛОГИКЕ
В данном разделе рассматриваются стандартные шаблоны логического вывода, которые могут применяться для формирования цепочек заключений, ведущих к желаемой цели. Эти шаблоны логического вывода называются правилами логического вывода. Наиболее широко известное правило называется правилом отделения (Modus Ponens — модус поненс) и записывается следующим образом:
а => Р, а (3
Эта запись означает, что если даны любые высказывания в форме а => Р и а, то из них можно вывести высказывание р. Например, если дано (WumpusAhead А
WumpusAlive) => Shoot и (WumpusAhead л WumpusAlive), то можно вывести высказывание Shoot.
Еще одним полезным правилом логического вывода является правило удаления связки "И", в котором утверждается, что из конъюнкции можно вывести любой из ее конъюнктов:
а л Р а
Например, из высказывания (WumpusAhead л WumpusAlive) можно вывести высказывание WumpusAlive.
Рассматривая возможные истинностные значения а и (3, можно легко показать, что правило отделения и правило удаления связки "И" являются непротиворечивыми не только применительно к данным примерам, но и ко всем возможным высказываниям. Это означает, что данные правила могут использоваться во всех конкретных случаях, в которых они могут потребоваться, вырабатывая непротиворечивые логические выводы без необходимости перебирать все модели.
В качестве правил логического вывода можно также применять все логические эквивалентности, приведенные в листинге 7.4. Например, из эквивалентности двухсторонней импликации и двух импликаций можно получить следующие два правила логического вывода (первое из них называется правилом удаления двухсторонней импликации):
_а <=> (3 (а (3) л (ft а)
(а => ft) л (ft => а) а <=> ft
Но не все правила логического вывода действуют в обоих направлениях, как это. Например, нельзя применить правило отделения в противоположном направлении, чтобы получить высказывания а => Р и а из высказывания р.
Рассмотрим, как можно использовать эти правила логического вывода и эквивалентности в мире вампуса. Начнем с базы знаний, содержащей высказывания R±—R5, и покажем, как доказать высказывание -iPi,2, т.е. утверждение, что в квадрате [1,2] нет ямы. Вначале применим правило удаления двухсторонней импликации к высказыванию R2, чтобы получить следующее:
Re: (Bl.l => (Pi,2 v P2,l)) Л ((Pi,2 v P2,i) => Bi,i)
Затем применим к высказыванию R6 правило удаления связки "И" и получим:
Rt. ( (Pi,2 v Р2Л) => Bi,i)
Из логической эквивалентности отрицаний следует:
Яв: => -.(Pi,2 v P2,i) )
Теперь можно применить правило отделения к высказыванию й8ик высказыванию я4 с данными восприятия (т.е. -Blil), чтобы получить следующее:
Rs: -i(Pi,2 v P2,i)
Наконец, применим правило де Моргана, позволяющее получить такое заключение:
Rio: -iPi,2 Л -iP2,i
Это означает, что ни в квадрате [ 1, 2 ], ни в квадрате [2,1] нет ямы.
Приведенный выше процесс логического вывода (последовательность применения правил логического вывода) называется доказательством. Процесс формирования доказательств полностью аналогичен процессу обнаружения решений в задачах поиска. В действительности, если можно было бы составить функцию определения преемника для выработки всех возможных вариантов применения правил логического вывода, это позволило бы использовать для формирования доказательств все алгоритмы поиска, приведенные в главах 3 и 4. Таким образом, вместо трудоемкого перебора моделей может применяться более эффективный способ логического вывода — формирование доказательств. Поиск может проходить в прямом направлении, от первоначальной базы знаний, и осуществляться путем использования правил логического вывода для получения целевого высказывания, или же этот поиск может проходить в обратном направлении, от целевого высказывания, в попытке найти цепочку правил логического вывода, ведущую от первоначальной базы знаний. Ниже в этом разделе рассматриваются два семейства алгоритмов, в которых используются оба эти подхода.
Из того факта, что задача логического вывода в пропозициональной логике является NP-полной, следует, что в наихудшем случае поиск доказательств может оказаться не более эффективным по сравнению с перебором моделей. Однако во многих практических случаях поиск доказательства может быть чрезвычайно эффективным просто потому, что в нем могут игнорироваться не относящиеся к делу (нерелевантные) высказывания, независимо от того, насколько велико их количество. Например, в приведенном выше доказательстве, ведущем к высказыванию -лР1/2 л -iP2,i, не упоминались высказывания В2Л, Р1Л, Р2/2 или Рзл. Их можно было не рассматривать, поскольку целевое высказывание, pli2, присутствует только в высказывании Р4; остальные высказывания из состава Р4 присутствуют только в Р4 и R2, поэтому Ru R3 и R5 не имеют никакого отношения к доказательству. Те же рассуждения останутся справедливыми, если в базу знаний будет введено на миллион больше высказываний; с другой стороны, в этом случае простой алгоритм перебора строк в истинностной таблице был бы буквально подавлен из-за экспоненциального взрыва, вызванного стремительным увеличением количества моделей.
Это свойство логических систем фактически вытекает из гораздо более фундаментального свойства, называемого монотонностью. Согласно этому свойству, множество высказываний, которые могут быть получены путем логического вывода, возрастает лишь по мере добавления к базе знаний новой информации10. Для любых высказываний а и (3 справедливо следующее:
если KB И а, то KB л (3 И а
Например, предположим, что база знаний содержит дополнительное утверждение (3, согласно которому в этом экземпляре мира вампуса имеется точно восемь ям. Эти знания могут помочь агенту прийти к дополнительным заключениям, но не способны поставить под сомнение какое-либо уже сделанное заключение а, в частности вывод о том, что в квадрате [1,2] нет ямы. Монотонность означает, что правила логического вывода могут применяться каждый раз, когда в базе знаний обнаруживаются подходящие предпосылки, — полученное заключение будет следствием из данного правила, независимо от того, что еще находится в базе знаний.