Прямой и обратный вывод

Благодаря такой полноте алгоритм резолюции становится очень важным методом логического вывода. Однако во многих практических ситуациях вся мощь правила резолюции не требуется. Реальные базы знаний часто содержат только выражения в ограниченной форме, называемые ^ хорновскими выражениями. Хорновское выражение представляет собой дизъюнкцию литералов, среди которых положительным является не больше чем один. Например, выражение (¬L_1,1 v ¬Breezev B_1,1), где L_1,1 означает, что местонахождением агента является квадрат [1,1], представляет собой хорновское выражение, тогда как выражение (¬B_1,1 v P_1,2 v P_2,1) таковым не является.

Ограничение, согласно которому только один литерал выражения должен быть положительным, может на первый взгляд показаться немного надуманным и бесперспективным, но фактически является очень важным по трем описанным ниже причинам.

Каждое хорновское выражение может быть записано как импликация, предпосылкой которой является конъюнкция положительных литералов, а заключением— один положительный литерал. Например, хорновское выражение (¬B_1,1 v P_1,2 v P_2,1) может быть записано как импликация (L_1,1 ^ Breeze) => B_1,1. В этой последней форме данное высказывание становится более легким для чтения: в нем утверждается, что если агент находится в квадрате [1,1] и чувствует ветерок, то ветерок чувствуется в квадрате [1,1]. Людям проще читать и писать в такой форме высказывания, касающиеся многих областей знаний. Хорновские выражения, подобные этому, имеющие точно один положительный литерал, называются определенными выражениями. Такой положительный литерал называется головой выражения, а отрицательные литералы образуют тело выражения. Определенное выражение без отрицательных литералов просто утверждает справедливость некоторого высказывания; такую конструкцию иногда называют фактом. Определенные выражения образуют основу для логического программирования. Хорновское выражение без положительных литералов может быть записано как импликация, заключением которой является литерал False. Например, выражение (¬W1,1 v ¬W1,2), согласно которому вампус не может находиться одновременно в квадратах [1,1] и [1, 2], эквивалентно выражению W_1,1 ^ W_1,2=> False. В мире баз данных такие высказывания называются ограничениями целостности и используются для обнаружения ошибок в данных. В приведенных ниже алгоритмах для простоты предполагается, что база знаний содержит только определенные выражения и не содержит ограничений целостности. Такие базы знаний мы будем называть находящимися вхорновской форме.

Логический вывод с использованием хорновских выражений может осуществляться с помощью алгоритма прямого логического вывода и обратного логического вывода, которые рассматриваются ниже. Оба эти алгоритма являются очень естественными в том смысле, что этапы логического вывода являются для людей очевидными и за ними можно легко проследить.

Получение логических следствий с помощью хорновских выражений может осуществляться за время, линейно зависящее от размера базы знаний.

Этот последний факт становится особенно приятным сюрпризом. Он означает, что процедура логического вывода оказывается весьма недорогостоящей применительно ко многим пропозициональным базам знаний, которые встречаются на практике.

Алгоритм прямого логического вывода PL-FC-Entails? (KB, q) определяет, следует ли единственный пропозициональный символ q (запрос) из базы знаний, представленной в форме хорновских выражений. Он начинает работу с известных фактов (положительных литералов) в базе знаний. Если известны все предпосылки некоторой импликации, то ее заключение добавляется к множеству известных фактов. Об этом говорит сайт https://intellect.icu . Например, если известно, что имеют место факты L_1,1 и Breeze, а в базе знаний имеется выражение (L_1,1 a Breeze) => B_1,1, то к ней можно добавить факт B_1,1. Этот процесс продолжается до тех пор, пока к базе знаний не добавляется запрос q или становится невозможным осуществление дальнейшего логического вывода. Этот подробный алгоритм приведен в листинге; главное, что следует о нем помнить, — то, что он действует за время, определяемое линейной зависимостью.

Алгоритм прямого логического вывода для пропозициональной логики. В списке agenda("повестка дня") отслеживаются символы, в отношении которых известно, что они истинны, но которые еще не "обработаны". В таблице count отслеживается информация о том, какое количество предпосылок каждой импликации еще не известно. Каждый раз, когда обрабатывается новый символ р из списка символовagenda, "стоящих на повестке дня", количество предпосылок в таблице countсокращается на единицу для каждой импликации, в которой появляется предпосылка р. (Такие импликации могут обнаруживаться за постоянное время, если индексация базы знаний KB выполнена должным образом.) После того как количество неизвестных предпосылок для некоторой импликации достигает нуля, все эти предпосылки становятся известными, поэтому заключение этой импликации может быть добавлено к списку agenda. Наконец, необходимо следить за тем, какие символы уже были обработаны; символ, выведенный логическим путем, не следует добавлять к спискуagenda, если он уже был обработан ранее. Это позволяет избежать излишней работы, а также предотвратить возникновение бесконечных циклов, которые могут быть вызваны наличием таких импликаций, как P => Q и Q => Р

function PL-FC-Entails?{KB, q) returns значение true или false

  inputs: KB, база знаний - множество пропозициональных

  хорновских выражений

  q, запрос - пропозициональный символ

  local variables: count, таблица, индексированная по высказываниям,

  первоначально имеющая размер,

  соответствующий количеству предпосылок

  inferred, таблица, индексированная по символам,

    в которой каждая запись первоначально

    имеет значение false

  agenda, список символов, первоначально включает

    символы, известные как истинные

    в базе знаний KB

  while список agenda не пуст do

  р <r- Pop {agenda)

  unless inferred[p] do

  inferred[p] <— true

  for each хорновское выражение с в котором присутствует

    предпосылка р do

    уменьшить на единицу значение count[с]

    if count[с] = 0 then do

    if Head[с] = q then return true

    Push(Head[c], agenda)

  return false

Лучший способ понять этот алгоритм состоит в том, чтобы рассмотреть пример и иллюстрацию. На рисунке, а показана простая база знаний из хорновских выражений, содержащая выражения Айв как известные факты. На рисунке приведена та же база знаний, изображенная в виде ^ графа AND-OR. В графах AND-OR кратные дуги, соединенные кривой линией, обозначают конъюнкцию (в них необходимо доказать истинность каждой дуги), а кратные дуги, не соединенные друг с другом, обозначают дизъюнкцию (достаточно доказать истинность любой из этих дуг). На этом графе можно легко проверить, как действует алгоритм прямого логического вывода. Устанавливаются значения известных листовых узлов (в данном случае Л и в), а процесс логического вывода распространяется вверх по графу до тех пор, пока это возможно. При появлении любой конъюнкции процесс распространения останавливается и ожидает до тех пор, пока все конъюнкты не становятся известными, и только после этого продолжается дальше. Рекомендуем читателю подробно проработать этот пример.

Пример применения алгоритма прямого логического вывода: простая база знаний, состоящая из хорновских выражений (а); соответствующий граф AND-OR (б)

Можно легко убедиться в том, что алгоритм прямого логического вывода являетсянепротиворечивым: каждый этап логического вывода по сути представляет собой применение правила отделения. Кроме того, алгоритм прямого логического вывода является полным: в нем может быть получено каждое атомарное высказывание, которое следует из базы знаний. Проще всего в этом можно убедиться, рассмотрев заключительное состояние таблицы inferred (после того, как этот алгоритм достигаетфиксированной точки, в которой становятся невозможными какие-либо новые этапы логического вывода).

Эта таблица содержит значение true для каждого символа, выведенного логическим путем в течение этого процесса, и false— для всех других символов. Эта таблица может рассматриваться как логическая модель; более того, ^ каждое определенное выражение в первоначальной базе знаний KB является истинным в данной модели. Чтобы убедиться в этом, предположим обратное, а именно, что некоторое выражение а1 л ... л ак => Ь из базы знаний является ложным в этой модели. Тогда в этой модели выражение а1 л ... л ак должно быть истинным и в ней же выражение Ъ должно быть ложным. Но это противоречит нашему предположению о том, что алгоритм достиг фиксированной точки! Поэтому можно сделать вывод, что множество атомарных высказываний, полученное логическим путем к моменту достижения фиксированной точки, определяет модель первоначальной базы знаний кв. Более того, любое атомарное высказывание д, которое следует из базы знаний KB, должно быть истинным во всех ее моделях, а также, в частности, в данной модели. Итак, любое высказывание д, которое следует из базы знаний, должно быть выведено логически данным алгоритмом.

прямой логический вывод представляет собой пример применения общего понятия формирования логических рассуждений, ^ управляемых данными, т.е. рассуждений, в которых фокус внимания вначале сосредоточен на известных данных. Прямой логический вывод может использоваться в любом агенте для получения заключений на основе поступающих результатов восприятия, часто даже без учета какоголибо конкретного запроса. Например, агент для мира вампуса может сообщать с помощью операции Tell результаты своих восприятий базе знаний с использованием инкрементного алгоритма прямого логического вывода, в котором новые факты могут добавляться к "повестке дня" для инициализации новых процессов логического вывода. У людей формирование рассуждений, управляемых данными, в определенной степени происходит по мере поступления новой информации. Например, находясь дома и услышав, что пошел дождь, человек, который собирался на пикник, может решить, что придется его отменить. Но такое решение вряд ли будет принято, если он узнает, что оказался мокрым семнадцатый лепесток самой крупной розы в саду его соседа; люди держат процессы прямого логического вывода под тщательным контролем, поскольку в противном случае их просто затопил бы поток логических заключений, не имеющих ничего общего с реальностью.

Алгоритм обратного логического вывода, как указывает само его название, действует в обратном направлении от запроса. Если удается сразу же узнать, что высказывание, содержащееся в запросе q, является истинным, то не нужно выполнять никакой работы. В противном случае алгоритм находит те импликации в базе знаний, из которых следует g Если можно доказать, что все предпосылки одной из этих импликаций являются истинными (с помощью обратного логического вывода), то высказывание g также является истинным. Будучи применен к запросу Q, показанному на рисунке, этот алгоритм будет проходить вниз по графу до тех пор, пока не достигнет множества известных фактов, которые образуют основу для доказательства. Разработку подробного алгоритма оставляем читателю в качестве упражнения; как и в случае алгоритма прямого логического вывода, эффективная реализация этого алгоритма выполняет свою работу за линейное время.