Множество поддержки
Применение метода предпочтений, в котором в первую очередь осуществляется попытка выполнить определенные операции резолюции, вполне оправдано, но, вообще говоря, более эффективный метод может быть основан на том, что следует попытаться полностью устранить некоторые потенциальные этапы резолюции. В стратегии с использованием множества поддержки выполняется именно это. Применение данной стратегии начинается с выявления подмножества высказываний, называемого множеством поддержки (set of support). На каждом этапе резолюции высказывание из множества поддержки комбинируется с другим высказыванием, а резольвента добавляется к множеству поддержки. Если множество поддержки является небольшим по сравнению со всей базой знаний, это позволяет резко сократить пространство поиска.
При использовании этого подхода необходимо соблюдать осторожность, поскольку при неправильном выборе множества поддержки алгоритм может стать неполным. Однако, если множество поддержки S будет выбрано так, чтобы оставшиеся высказывания, вместе взятые, оставались выполнимыми, то резолюция с помощью множества поддержки становится полной. Общепринятый подход, основанный на предположении, что первоначальная база знаний является непротиворечивой, состоит в том, чтобы в качестве множества поддержки применялся отрицаемый запрос. (В конце концов, если база знаний не является непротиворечивой, то сам факт, что запрос является следствием из нее, становится избыточным, поскольку из противоречия можно доказать все, что угодно.) Стратегия с использованием множества поддержки имеет дополнительное преимущество в том, что в ней часто вырабатываются деревья доказательства, легко доступные для понимания людей, поскольку само формирование доказательства осуществляется целенаправленно.
Резолюция с входными высказываниями
В стратегии резолюции с входными высказываниями (input resolution) на каждом этапе резолюции комбинируется одно из входных высказываний (из базы знаний или запроса) с некоторым другим высказыванием. В доказательстве, показанном на рис. 9.7, использовались только этапы резолюции с входными высказываниями и поэтому дерево доказательства имело характерную форму в виде единого "хребта" с отдельными высказываниями, комбинирующимися с этим хребтом. Очевидно, что пространство деревьев доказательства такой формы меньше по сравнению с пространством всех возможных графов доказательства. В хорновских базах знаний как своего рода стратегия резолюции с входными высказываниями может рассматриваться правило отделения, поскольку при использовании этого правила некоторая импликация из первоначальной базы знаний комбинируется с некоторыми другими высказываниями. Таким образом, нет ничего удивительного в том, что метод резолюции с входными высказываниями является полным применительно к базам знаний, которые находятся в хорновской форме, но в общем случае он неполон. Стратегия линейной резолюции (linear resolution) представляет собой небольшое обобщение, в котором допускается применять в одной операции резолюции высказывания р и Q, если р находится в первоначальной базе знаний или Р является предком Q в дереве доказательства. Метод линейной резолюции является полным.
Обобщение
В методе обобщения (subsumption) устраняются все высказывания, которые обобщаются некоторым существующим высказыванием из базы знаний (т.е. являются более конкретными по сравнению с ним). Например, если в базе знаний есть высказывание Р(х), то нет смысла вводить в нее высказывание Р(А) и еще меньше смысла вводить Р(А) v Q(B). Обобщение позволяет поддерживать небольшие размеры базы знаний и тем самым ограничивать размеры пространства поиска.
Средства автоматического доказательства теорем
Средства автоматического доказательства теорем (называемые также средствами автоматизированного формирования рассуждений) отличаются от языков логического программирования в двух отношениях. Во-первых, большинство языков логического программирования поддерживает только хорновские выражения, тогда как средства автоматического доказательства теорем поддерживают полную логику первого порядка. Во-вторых, в программах на таком типичном языке логического программирования, как Prolog, переплетаются логика и управление. Например, выбор программистом выражения А : - в, С вместо А : - С, в может повлиять на выполнение программы. С другой стороны, в большинстве средств автоматического доказательства теорем синтаксическая форма, выбранная для высказываний, не влияет на результаты. Для средств автоматического доказательства теорем все еще требуется управляющая информации, чтобы они могли функционировать эффективно, но эта информация обычно хранится отдельно от базы знаний, а не входит в состав самого представления знаний. Большинство исследований в области средств автоматического доказательства теорем посвящено поиску стратегий управления, которые приводят к общему повышению эффективности, а не только к увеличению быстродействия.
Проект одного из средств автоматического доказательства теорем
В этом разделе описана программа автоматического доказательства теорем Otter (Organized Techniques for Theorem-proving and Effective Research) [1018]; в этом описании особое внимание будет уделено применяемой в ней стратегии управления. Подготавливая любую задачу для программы Otter, пользователь должен разделить знания на четыре описанные ниже части.
• Множество выражений, известное как множество поддержки (или sos — set of support), в котором определяются важные факты о данной задаче. На каждом этапе резолюции операция резолюции применяется к одному из элементов множества поддержки и к другой аксиоме, поэтому поиск сосредоточивается на множестве поддержки.
• Множество полезных аксиом (usable axiom), которое выходит за пределы множества поддержки. Эти аксиомы предоставляют фоновые знания о проблемной области. Определение границы между тем, что должно войти в состав задачи (и поэтому в множество sos) и что относится к фоновым знаниям (и поэтому должно войти в число полезных аксиом), передается на усмотрение пользователя.
• Множество уравнений, известных как правила перезаписи (rewrites), или демодуляторы (demodulators). Хотя демодуляторы представляют собой уравнения, они всегда применяются в направлении слева направо, поэтому определяют каноническую форму, в которой должны быть представлены все упрощенные термы. Например, демодулятор х+0=х указывает, что любой терм в форме х+0 должен быть заменен термом х.
• Множество параметров и выражений, который определяет стратегию управления. В частности, пользователь задает эвристическую функцию для управления поиском и функцию фильтрации для устранения некоторых подцелей как не представляющих интереса.
Программа Otter действует по принципу постоянного применения правила резолюции к одному из элементов множества поддержки и к одной из полезных аксиом. В отличие от системы Prolog, в этой программе используется определенная форма поиска по первому наилучшему совпадению. Ее эвристическая функция измеряет "вес" каждого выражения с учетом того, что наиболее предпочтительными являются выражения с наименьшими весами. Задача точной формулировки эвристической функции возлагается на пользователя, но, вообще говоря, вес любого выражения должен коррелировать с его размером или сложностью. Единичные выражения оцениваются как имеющие наименьший вес, поэтому такой метод поиска может рассматриваться как обобщение стратегии с преимущественным использованием единичных выражений. На каждом этапе программа Otter перемещает выражение "с наименьшим весом" из множества поддержки в список полезных аксиом и добавляет в множество поддержки некоторые непосредственные следствия применения операции резолюции к выражению с наименьшим весом и к элементам списка полезных аксиом. Программа Otter останавливается, если обнаруживает противоречие или если возникает такая ситуация, что в множестве поддержки не остается больше выражений. Алгоритм работы этой программы показан более подробно в листинге 9.5.
Листинг 9.5. Набросок структуры программы автоматического доказательства теорем Otter. Эвристическое управление применяется при выборе выражения "с наименьшим весом" и в функции Filter, которая устраняет из рассмотрения такие выражения, которые не представляют интереса
procedure Otter(sos, usable)
inputs: sos, множество поддержки - выражения, определяющие решаемую задачу (глобальная переменная)
usable, множество фоновых знаний, которые потенциально могут быть релевантными для данной задачи
repeat
clause <г- элемент множества sos с наименьшим весом переместить выражение clause из множество sos
в множество usable Process(Infer{clause, usable), sos) until sos - [] or обнаружится опровержение
function Infer(clause, usable) returns множество выражений clauses
применить правило резолюции к выражению clause и каждому элементу
множества usable возвратить полученное множество clauses после применения
функции Filter
procedure Process(clauses, sos)
for each clause in clauses do
clause <— Simplify(clause)
выполнить слияние идентичных литералов
отбросить выражение clause, если оно представляет
собой тавтологию sos <— [clause \ sos]
if clause не имеет литералов, то обнаружено опровержение if clause имеет один литерал, то искать единичное опровержение