Прямой и обратный логический вывод
Благодаря такой полноте алгоритм резолюции становится очень важным методом логического вывода. Однако во многих практических ситуациях вся мощь правила резолюции не требуется. Реальные базы знаний часто содержат только выражения в ограниченной форме, называемые хорновскими выражениями. Хорновское выражение представляет собой дизъюнкцию литералов, среди которых положительным является не больше чем один. Например, выражение (-iL1#1 v -Breeze v B1#1), где Llfl означает, что местонахождением агента является квадрат [1,1], представляет собой хорновское выражение, тогда как выражение {-уВ1Л v р1#2 v Р2/1) таковым не является.
Офаничение, согласно которому только один литерал выражения должен быть положительным, может на первый взгляд показаться немного надуманным и бесперспективным, но фактически является очень важным по трем описанным ниже причинам.
1. Каждое хорновское выражение может быть записано как импликация, пред-
посылкой которой является конъюнкция положительных литералов, а заклю-
чением— один положительный литерал (см. упр. 7.12). Например, хорнов-
ское выражение (-пЬ1Л v -iBreeze v в1Л) может быть записано как им-
пликация (Llfl л Breeze) => в1Л. В этой последней форме данное
высказывание становится более легким для чтения: в нем утверждается, что
если агент находится в квадрате [1,1] и чувствует ветерок, то ветерок чувст-
вуется в квадрате [1,1]. Людям проще читать и писать в такой форме выска-
зывания, касающиеся многих областей знаний.
Хорновские выражения, подобные этому, имеющие точно один положительный литерал, называются определенными выражениями. Такой положительный литерал называется головой выражения, а отрицательные литералы образуют Sv тело выражения. Определенное выражение без отрицательных литералов просто утверждает справедливость некоторого высказывания; такую конструкцию иногда называют фактом. Определенные выражения образуют основу для логического программирования, которое рассматривается в главе 9. Хорновское выражение без положительных литералов может быть записано как импликация, заключением которой является литерал False. Например, выражение (-11,1 v -*iWli2), согласно которому вампус не может находиться одновременно в квадратах [1,1] и [1,2], эквивалентно выражению wltl л wli2 => False. В мире баз данных такие высказывания называются ограничениями целостности и используются для обнаружения ошибок в данных. В приведенных ниже алгоритмах для простоты предполагается, что база знаний содержит только определенные выражения и не содержит ограничений целостности. Такие базы знаний мы будем называть находящимися в хорновской пэорме.
2. Логический вывод с использованием хорновских выражений может осуществляться с помощью алгоритма прямого логического вывода и обратного логического вывода, которые рассматриваются ниже. Оба эти алгоритма являются очень естественными в том смысле, что этапы логического вывода являются для людей очевидными и за ними можно легко проследить.
3. Получение логических следствий с помощью хорновских выражений может осуществляться за время, линейно зависящее от размера базы знаний.
Этот последний факт становится особенно приятным сюрпризом. Он означает, что процедура логического вывода оказывается весьма недорогостоящей применительно ко многим пропозициональным базам знаний, которые встречаются на практике.
Алгоритм прямого логического вывода PL-FC-Entails? (KB, q) определяет, следует ли единственный пропозициональный символ q (запрос) из базы знаний, представленной в форме хорновских выражений. Он начинает работу с известных фактов (положительных литералов) в базе знаний. Если известны все предпосылки некоторой импликации, то ее заключение добавляется к множеству известных фактов. Например, если известно, что имеют место факты ь1Л и Breeze, а в базе знаний имеется выражение (Ь1Л л Breeze) => в1л, то к ней можно добавить факт В1Л. Этот процесс продолжается до тех пор, пока к базе знаний не добавляется запрос q или становится невозможным осуществление дальнейшего логического вывода. Этот подробный алгоритм приведен в листинге 7.6; главное, что следует о нем помнить, — то, что он действует за время, определяемое линейной зависимостью.
Листинг 7.6. Алгоритм прямого логического вывода для пропозициональной логики. В списке agenda ("повестка дня") отслеживаются символы, в отношении которых известно, что они истинны, но которые еще не "обработаны". В таблице count отслеживается информация о том, какое количество предпосылок каждой импликации еще не известно. Каждый раз, когда обрабатывается новый символ р из списка символов agenda, "стоящих на повестке дня", количество предпосылок в таблице count сокращается на единицу для каждой импликации, в которой появляется предпосылка р. (Такие импликации могут обнаруживаться за постоянное время, если индексация базы знаний KB выполнена должным образом.) После того как количество неизвестных предпосылок для некоторой импликации достигает нуля, все эти предпосылки становятся известными, поэтому заключение этой импликации может быть добавлено к списку agenda. Наконец, необходимо следить за тем, какие символы уже были обработаны; символ, выведенный логическим путем, не следует добавлять к списку agenda, если он уже был обработан ранее. Это позволяет избежать излишней работы, а также предотвратить возникновение бесконечных циклов, которые могут быть вызваны наличием таких импликаций, как р => QuQ => р
function PL-FC-Entails?(KB, q) returns значение true или false inputs: KB, база знаний - множество пропозициональных хорновских выражений q, запрос - пропозициональный символ local variables: count, таблица, индексированная по высказываниям,
первоначально имеющая размер, соответствующий количеству предпосылок inferred, таблица, индексированная по символам, в которой каждая запись первоначально имеет значение false agenda, список символов, первоначально включает символы, известные как истинные в базе знаний KB
while список agenda не пуст do р <— Pop(agenda) unless inferred[p] do
inferred[p] <— true
for each хорновское выражение с в котором присутствует предпосылка р do уменьшить на единицу значение count[с] if count[c] = 0 then do
if Head[с] = q then return true Push(Head[c], agenda)
return false
Лучший способ понять этот алгоритм состоит в том, чтобы рассмотреть пример и иллюстрацию. На рис. 7.7, а показана простая база знаний из хорновских выражений, содержащая выражения А и В как известные факты. На рис. 7.7, б приведена та же база знаний, изображенная в виде графа AND-OR. В графах AND-OR кратные дуги, соединенные кривой линией, обозначают конъюнкцию (в них необходимо доказать истинность каждой дуги), а кратные дуги, не соединенные друг с другом, обозначают дизъюнкцию (достаточно доказать истинность любой из этих дуг). На этом графе можно легко проверить, как действует алгоритм прямого логического вывода. Устанавливаются значения известных листовых узлов (в данном случае Л и в), а процесс логического вывода распространяется вверх по графу до тех пор, пока это возможно. При появлении любой конъюнкции процесс распространения останавливается и ожидает до тех пор, пока все конъюнкты не становятся известными, и только после этого продолжается дальше. Рекомендуем читателю подробно проработать этот пример.
Можно легко убедиться в том, что алгоритм прямого логического вывода является непротиворечивым: каждый этап логического вывода по сути представляет собой применение правила отделения. Кроме того, алгоритм прямого логического вывода является полным: в нем может быть получено каждое атомарное высказывание, которое следует из базы знаний. Проще всего в этом можно убедиться, рассмотрев заключительное состояние таблицы inferred (после того, как этот алгоритм достигает фиксированной точки, в которой становятся невозможными какие-либо новые этапы логического вывода). Эта таблица содержит значение true для каждого символа, выведенного логическим путем в течение этого процесса, и false — для всех других символов. Эта таблица может рассматриваться как логическая модель; более того, "JSk каждое определенное выражение в первоначальной базе знаний KB является истинным в данной модели. Чтобы убедиться в этом, предположим обратное, а именно, что некоторое выражение ax А ... А ак => Ъ из базы знаний является ложным в этой модели. Тогда в этой модели выражение ах л ... л ак должно быть истинным и в ней же выражение Ъ должно быть ложным. Но это противоречит нашему предположению о том, что алгоритм достиг фиксированной точки! Поэтому можно сделать вывод, что множество атомарных высказываний, полученное логическим путем к моменту достижения фиксированной точки, определяет модель первоначальной базы знаний КВ. Более того, любое атомарное высказывание д, которое следует из базы знаний KB, должно быть истинным во всех ее моделях, а также, в частности, в данной модели. Итак, любое высказывание д, которое следует из базы знаний, должно быть выведено логически данным алгоритмом.
Прямой логический вывод представляет собой пример применения общего понятия формирования логических рассуждений, управляемых данными, т.е. рассуждений, в которых фокус внимания вначале сосредоточен на известных данных. Прямой логический вывод может использоваться в любом агенте для получения заключений на основе поступающих результатов восприятия, часто даже без учета какого-либо конкретного запроса. Например, агент для мира вампуса может сообщать с помощью операции Tell результаты своих восприятий базе знаний с использованием инкрементного алгоритма прямого логического вывода, в котором новые факты могут добавляться к "повестке дня" для инициализации новых процессов логического вывода. У людей формирование рассуждений, управляемых данными, в определенной степени происходит по мере поступления новой информации. Например, находясь дома и услышав, что пошел дождь, человек, который собирался на пикник, может решить, что придется его отменить. Но такое решение вряд ли будет принято, если он узнает, что оказался мокрым семнадцатый лепесток самой крупной розы в саду его соседа; люди держат процессы прямого логического вывода под тщательным контролем, поскольку в противном случае их просто затопил бы поток логических заключений, не имеющих ничего общего с реальностью.
Алгоритм обратного логического вывода, как указывает само его название, действует в обратном направлении от запроса. Если удается сразу же узнать, что высказывание, содержащееся в запросе д, является истинным, то не нужно выполнять никакой работы. В противном случае алгоритм находит те импликации в базе знаний, из которых следует д. Если можно доказать, что все предпосылки одной из этих импликаций являются истинными (с помощью обратного логического вывода), то высказывание дтакже является истинным. Будучи применен к запросу Q, показанному на рис. 7.7, этот алгоритм будет проходить вниз по графу до тех пор, пока не достигнет множества известных фактов, которые образуют основу для доказательства. Разработку подробного алгоритма оставляем читателю в качестве упражнения; как и в случае алгоритма прямого логического вывода, эффективная реализация этого алгоритма выполняет свою работу за линейное время.
Обратный логический вывод представляет собой одну из форм рассуждения, направляемого целями. Такая форма является полезной при получении ответов на конкретные вопросы, наподобие следующих: "Что теперь мне следует делать?" и "Где же находятся мои ключи?" Зачастую стоимость обратного логического вывода намного меньше по сравнению со стоимостью, линейно зависящей от размера базы знаний, поскольку в этом процессе затрагиваются только факты, непосредственно относящиеся к делу. Вообще говоря, агент должен разделять работу между процессами прямого и обратного формирования рассуждений, ограничивая прямое формирование рассуждений выработкой фактов, которые, по всей вероятности, будут относиться к запросам, подлежащим решению с помощью обратного логического вывода.
В данном разделе рассматриваются два семейства эффективных алгоритмов пропозиционального логического вывода, основанного на проверке по модели: один подход основан на поиске с возвратами, а другой — на поиске с восхождением к вершине. Указанные алгоритмы входят в состав основного "инструментария" пропозициональной логики. Этот раздел может быть пропущен при первом чтении настоящей главы.
Рассматриваемые здесь алгоритмы предназначены для проверки выполнимости. Выше уже отмечалась связь между поиском модели, обеспечивающей выполнимость логического высказывания, и поиском решения задачи удовлетворения ограничения, поэтому, скорее всего, нет ничего удивительного в том, что эти два семейства алгоритмов весьма напоминают алгоритмы поиска с возвратами, описанные в разделе 5.2, и алгоритмы локального поиска, которые представлены в разделе 5.3. Тем не менее приведенные здесь алгоритмы являются чрезвычайно важными сами по себе, поскольку в компьютерных науках существует очень много комбинаторных задач, которые можно свести к проверке выполнимости пропозиционального высказывания. Любое усовершенствование алгоритмов проверки выполнимости влечет за собой колоссальные последствия, связанные с повышением нашей способности справляться со всеми сложными задачами в целом.
Полный алгоритм поиска с возвратами
Первый рассматриваемый здесь алгоритм часто называют алгоритмом Дэвиса-Патнем в честь авторов оригинальной статьи, в которой он был опубликован, Мартина Дэвиса и Хилари Патнем [336]. Затем этот алгоритм фактически стал одной из версий, описанных Дэвисом, Логеманом и Лавлендом [335], поэтому мы будем называть его DPLL по первым буквам фамилий всех четырех авторов. Алгоритм DPLL принимает на входе некоторое высказывание в конъюнктивной нормальной форме — высказывание, представленное как множество выражений. Как и алгоритмы Backtracking-Search и TT-Entails?, он фактически выполняет рекурсивный перебор в глубину всех возможных моделей. Но в этом алгоритме реализованы три описанных ниже усовершенствования, и этим он отличается от простой схемы, применяемой в алгоритме TT-Entails?.
• Раннее завершение. Алгоритм обнаруживает, должно ли данное высказывание быть истинным или ложным, даже с помощью частично завершенной модели. Выражение является истинным, если истинен любой его литерал, даже притом что для других литералов еще не определены истинностные значения; поэтому об истинности всего высказывания в целом можно судить еще до того, как модель будет составлена полностью. Например, высказывание (A v В) л (A v С) является истинным, если истинен литерал А, независимо от значений литералов В и С.