Учет отношения равенства
Ни в одном из методов логического вывода, описанных до сих пор в этой главе, не учитывалось отношение равенства. Для решения этой задачи может быть принято три различных подхода. Первый подход состоит в аксиоматизации равенства — включении в базу знаний высказываний, касающихся отношения равенства. При этом необходимо описать, что отношение равенства является рефлексивным, симметричным и транзитивным, а также сформулировать утверждение, что мы можем в любом предикате или функции заменять равные литералы равными. Таким образом, требуются три базовые аксиомы и еще по одной аксиоме для каждого предиката и функции, как показано ниже.
При наличии в базе знаний таких высказываний любая стандартная процедура логического вывода, такая как резолюция, позволяет решать задачи, требующие формирования рассуждений с учетом отношения равенства, например находить решения математических уравнений.
Еще один способ учета отношения равенства состоит в использовании дополнительного правила логического вывода. В простейшем правиле, правиле демодуляции, берется единичное выражение х=у, после чего терм у подставляется вместо любого терма, который унифицируется с термом х в каком-то другом выражении. Более формально эту идею можно представить, как описано ниже.
• Демодуляция. Для любых термов х, у и z, где Unify (х, z) =0 и mn[z] -литерал, содержащий z, справедливо следующее:
х = у, л?1 v ... v mn[z] т1 v ... v л?п[Subst (0,у) ]
Демодуляция обычно используется для упрощения выражений с помощью коллекции утверждений, таких как х+0=х, х1=х и т.д. Это правило может быть также дополнено, чтобы можно было учитывать неединичные выражения, в которых появляется литерал со знаком равенства, как показано ниже.
Subst (0,1 V ... V 4 V Л71 v ... v Л7п[у])
В отличие от демодуляции, парамодуляция позволяет получить полную процедуру логического вывода для логики первого порядка с отношением равенства.
В третьем подходе формирование логических рассуждений с учетом равенства полностью осуществляется с помощью расширенного алгоритма унификации. Это означает, что термы рассматриваются как унифицируемые, если можно доказать, что они становятся равными при некоторой подстановке; здесь выражение "можно доказать" допускает включение в определенном объеме рассуждений о равенстве. Например, термы 1 + 2 и 2 + 1 обычно не рассматриваются как унифицируемые, но алгоритм унификации, в котором известно, что х+у=у+х, способен унифицировать их с помощью пустой подстановки. .Унификация с учетом равенства (equational unification) такого рода может выполняться с помощью эффективных алгоритмов, разработанных с учетом данных конкретных используемых аксиом (коммутативность, ассоциативность и т.д.), а не с помощью явного логического вывода на основе этих аксиом. Программы автоматического доказательства теорем с использованием этого метода очень близки к системам логического программирования в ограничениях, описанным в разделе 9.4.
Стратегии резолюции
Как известно, повторные применения правила логического вывода на основе резолюции позволяют в конечном итоге найти доказательство, если оно существует, а в этом подразделе рассматриваются стратегии, позволяющие находить доказательства не методом перебора, а более эффективно.
Преимущественное использование единичных выражений
В этой стратегии преимущество отдается таким операциям резолюции, в которых одним из высказываний является единственный литерал (известный также как единичное выражение — unit clause). В основе этой стратегии лежит такая идея, что если осуществляются попытки получения пустого выражения, то может оказаться целесообразным отдавать предпочтение таким операциям логического вывода, в которых вырабатываются более короткие выражения. Применение операции резолюции к единичному высказыванию (такому как Р) в сочетании с любым другим высказыванием (таким как -.Р v -,Q v R) всегда приводит к получению выражения (в данном случае -iQ v р), более короткого, чем это другое высказывание. Когда стратегия с преимущественным использованием единичных выражений была впервые оп-
• Парамодуляция. Для любых термов х, у и z, где Unify (х, z) =0, справедливо следующее: li У ... v Ik v х = у, mi v ... У mn[z] робована в пропозициональном логическом выводе в 1964 году, она привела к резкому ускорению работы, обеспечив возможность доказывать теоремы, с которыми не удавалось справиться без использования этого метода предпочтения. Тем не менее метод предпочтения единичных выражений, отдельно взятый, не позволяет уменьшить коэффициент ветвления в задачах средних размеров до такой степени, чтобы можно было обеспечить возможность их решения с помощью резолюции. Несмотря на это, он представляет собой полезный эвристический метод, который может успешно использоваться в сочетании с другими стратегиями.
Единичная резолюция (unit resolution) — это ограниченная форма резолюции, в которой на каждом этапе резолюции должно участвовать единичное выражение. В общем случае метод единичной резолюции является неполным, но становится полным при его применении к хорновским базам знаний. Процесс доказательства по методу единичной резолюции применительно к хорновским базам знаний напоминает прямой логический вывод.