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

 
Пропозициональная логика Печать

В данном разделе рассматриваются стандартные шаблоны логического вывода, которые могут применяться для формирования цепочек заключений, ведущих к желаемой цели. Эти шаблоны логического вывода называются правилами логического вывода. Наиболее широко известное правило называется правилом отделения (Modus Ponens — модус поненс) и записывается следующим образом:

Image

 

 

Эта запись означает, что если даны любые высказывания в форме α => β и а, то из них можно вывести высказывание β. Например, если дано (WumpusAhead ^ WumpusAlive) => Shoot и (WumpusAhead л WumpusAlive), то можно вывести высказывание Shoot.

Еще одним полезным правилом логического вывода является правило удаления связки "И", в котором утверждается, что из конъюнкции можно вывести любой из ее конъюнктов:

Image

 

 

Например, из высказывания (WumpusAhead ^ WumpusAlive) можно вывести высказывание WumpusAlive. Рассматривая возможные истинностные значения α и β, можно легко показать, что правило отделения и правило удаления связки "И" являются непротиворечивыми не только применительно к данным примерам, но и ко всем возможным высказываниям. Это означает, что данные правила могут использоваться во всех конкретных случаях, в которых они могут потребоваться, вырабатывая непротиворечивые логические выводы без необходимости перебирать все модели.

В качестве правил логического вывода можно также применять все логические эквивалентности, приведенные в листинге. Например, из эквивалентности двухсторонней импликации и двух импликаций можно получить следующие два правила логического вывода (первое из них называется правилом удаления двухсторонней импликации):

 

Image

 

 

Но не все правила логического вывода действуют в обоих направлениях, как это. Например, нельзя применить правило отделения в противоположном направлении, чтобы получить высказывания α => β и а из высказывания β.

Рассмотрим, как можно использовать эти правила логического вывода и эквивалентности в мире вампуса. Начнем с базы знаний, содержащей высказывания R1—R5, и покажем, как доказать высказывание ¬P1,2, т.е. утверждение, что в квадрате [1,2] нет ямы. Вначале применим правило удаления двухсторонней импликации к высказыванию R2, чтобы получить следующее:

R6: (B1,1 => (P1,2 v P2,1)) ^ ((P1,2 v P2,1) => B1,1)

Затем применим к высказыванию R6 правило удаления связки "И" и получим:

R7: ((P1,2 v P2,1) => B1,1)

Из логической эквивалентности отрицаний следует:

R8: (¬B1,1 => ¬(P1,2 v P2,1))

Теперь можно применить правило отделения к высказыванию R8 и к высказыванию R4 с данными восприятия (т.е. ¬B1,1), чтобы получить следующее:

R9: ¬(P1,2 v P2,1)

Наконец, применим правило де Моргана, позволяющее получить такое заключение:

R10: ¬P1,2 ^ ¬P2,1

Это означает, что ни в квадрате [1,2],ни в квадрате [2,1] нет ямы.

Приведенный выше процесс логического вывода (последовательность применения правил логического вывода) называется доказательством. Процесс формирования доказательств полностью аналогичен процессу обнаружения решений в задачах поиска. В действительности, если можно было бы составить функцию определения преемника для выработки всех возможных вариантов применения правил логического вывода, это позволило бы использовать для формирования доказательств все алгоритмы поиска. Таким образом, вместо трудоемкого перебора моделей может применяться более эффективный способ логического вывода — формирование доказательств. Поиск может проходить в прямом направлении, от первоначальной базы знаний, и осуществляться путем использования правил логического вывода для получения целевого высказывания, или же этот поиск может проходить в обратном направлении, от целевого высказывания, в попытке найти цепочку правил логического вывода, ведущую от первоначальной базы знаний. Ниже в этом разделе рассматриваются два семейства алгоритмов, в которых используются оба эти подхода.

Из того факта, что задача логического вывода в пропозициональной логике является NP-полной, следует, что в наихудшем случае поиск доказательств может оказаться не более эффективным по сравнению с перебором моделей. Однако во многих практических случаях поиск доказательства может быть чрезвычайно эффективным просто потому, что в нем могут игнорироваться не относящиеся к делу (нерелевантные) высказывания, независимо от того, насколько велико их количество.

Например, в приведенном выше доказательстве, ведущем к высказыванию ¬P1,2 ^ ¬P2,1 не упоминались высказывания B2,1, P1,1, P2,2 или P3,1. Их можно было не рассматривать, поскольку целевое высказывание, P1,2, присутствует только в высказывании R4; остальные высказывания из состава R4 присутствуют только в R4 и R2, поэтому R1, R3 и R5 не имеют никакого отношения к доказательству. Те же рассуждения останутся справедливыми, если в базу знаний будет введено на миллион больше высказываний; с другой стороны, в этом случае простой алгоритм перебора строк в истинностной таблице был бы буквально подавлен из-за экспоненциального взрыва, вызванного стремительным увеличением количества моделей.

Это свойство логических систем фактически вытекает из гораздо более фундаментального свойства, называемого монотонностью. Согласно этому свойству, множество высказываний, которые могут быть получены путем логического вывода, возрастает лишь по мере добавления к базе знаний новой информации. Для любых высказываний α и β справедливо следующее:

если KB ≠ α, то KB ^ β ≠ α

Например, предположим, что база знаний содержит дополнительное утверждение β, согласно которому в этом экземпляре мира вампуса имеется точно восемь ям. Эти знания могут помочь агенту прийти к дополнительным заключениям, но не способны поставить под сомнение какое-либо уже сделанное заключение α, в частности вывод о том, что в квадрате [1,2] нет ямы. Монотонность означает, что правила логического вывода могут применяться каждый раз, когда в базе знаний обнаруживаются подходящие предпосылки, — полученное заключение будет следствием из данного правила, независимо от того, что еще находится в базе знаний.