Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 112
Текст из файла (страница 112)
Для любых термов х, у и х, где г)па ту (х, г) =0 и лЬ [ х]— литерал, содержащий г, справедливо следующее: 421 Глава 9. Логический вывод в логике первого порядка х =, гп1 и ... и пп [х] пп1 и ... и юп„[яаЬвс (в,у) ) Демодуляция обычно используется для упрощения выражений с помощью коллекции утверждений, таких как хьо=х, х'=х и т.д.
Это правило может быть также дополнено, чтобы можно было учитывать неединичные выражения, в которых появляется литерал со знаком равенства, как показано ниже. ° 'сь Парамодуляция. Для любых термов х, уи г, где [)пзгу(х, г) =О, справедливо следующее: Г1ч...ч~.'„чх=у,в1м..чпь[а) эиЪае(О,Г1 ч .. ч Гп и пв у ... ч пъ[у]) В отличие от демодуляции, парамодуляция позволяет получить полную процедуру логического вывода для логики первого порядка с отношением равенства. В третьем подхоле формирование логических рассуждений с учетом равенства полностью осуществляется с помощью расширенного алгоритма унификации. Это означает, что термы рассматриваются как унифицируемые, если можно доказать, что они становятся равными пр(и некоторой подстановке; здесь выражение "можно доказать" допускает включение в определенном объеме рассуждений о равенстве. Например, термы 1+2 и 2~-1 обычно не рассматриваются как унифицируемые, но алгоритм унификации, в котором известно, что х+у=уьх, способен унифицировать их с помощью пустой подстановки.
'ж Унификация с учетом равенства (е(]ца([опа! цп!бсабоп) такого рода может выполняться с помощью эффективных алгоритмов, разработанных с учетом данных конкретных используемых аксиом (коммугативность, ассоциативность и т.д.), а не с помошью явного логического вывода на основе этих аксиом.
Программы автоматического доказательства теорем с использованием этого метола очень близки к системам логического программирования в ограничениях, описанным в разделе 9.4. Стратегии резолюции Как известно, повторные применения правила логического вывода на основе резолюции позволяют в конечном итоге найти доказательство, если оно существует, а в этом подразделе рассматриваются стратегии, позволяющие находить доказательства не методом перебора, а более эффективно. Преимущественное использование единичных выражений В этой стратегии преимущество отдается таким операциям резолюции, в которых одним из высказываний является единственный литерал (известный также как единичное выражение — цпй с]ацзе). В основе этой стратегии лежит такая идея, что если осуществляются попытки получения пустого выражения, то может оказаться целесообразным отдавать предпочтение таким операциям логического вывода, в которых вырабатываются более короткие выражения. Применение операции резолюции к единичному высказыванию (такому как р) в сочетании с любым другим высказыванием (таким как ~Р у Ц у я) всегда приводит к получению выражения (в данном случае 0 у л), более короткого, чем это другое высказывание.
Когда стратегия с преиму(цественным использованием единичных выражений была впервые оп- 422 Часть Ш. Знания и рассуждения робована в пропозициональном логическом выводе в 1964 году, она привела к резкому ускорению работы, обеспечив возможность доказывать теоремы, с которыми не удавалось справиться без использования этого метода предпочтения.
Тем не менее метод предпочтения единичных выражений, отдельно взятый, не позволяет уменьшить коэффициент ветвления в задачах средних размеров до такой степени, чтобы можно было обеспечить возможность их решения с помощью резолюции. Несмотря на это, он представляет собой полезный эвристический метод, который может успешно использоваться в сочетании с другими стратегиями. Ъ. Единичная резолюции (ип)г геао1шьоп) — это ограниченная форма резолюции, в которой на каждом этапе резолюции должно участвовать единичное выражение. Вобщем случае метод единичной резолюции является неполным, но становится полным при его применении к хорновским базам знаний. Процесс доказательства по методу единичной резолюции применительно к хорновским базам знаний напоминает прямой логический вывод.
Множество поддержки Применение метода предпочтений, в котором в первую очередь осуществляется попытка выполнить определенные операции резолюции, вполне оправдано, но, вообще говоря, более эффективный метод может быть основан на том, что следует попытаться полностью устранить некоторые потенциальные этапы резолюции. В стратегии с использованием множества поддержки выполняется именно это. Применение данной стратегии начинается с выявления подмножества высказываний, называемого 'ъ. множеством поддержки (зег о( зцррой). На каждом этапе резолюции высказывание из множества поддержки комбинируется с другим высказыванием, а резольвента добавляется к множеству полдержки.
Если множество поддержки является неболыним по сравнению со всей базой знаний, это позволяет резко сократить пространство поиска. При использовании этого подхода необходимо соблюдать осторожность, поскольку при неправильном выборе множества поддержки алгоритм может стать неполным. Однако, если множество поддержки ~ будет выбрано так, чтобы оставшиеся высказывания, вместе взятые, оставались выполнимыми, то резолюция с помощью множества поддержки становится полной.
Общепринятый подход, основанный на предположении, что первоначальная база знаний является непротиворечивой, состоит в том, чтобы в качестве множества поддержки применялся отрицаемый запрос. (В конце концов, если база знаний не является непротиворечивой, то сам факт, что запрос является следствием из нее, становится избыточным, поскольку из противоречия можно доказать все, что угодно.) Стратегия с использованием множества поддержки имеет дополнительное преимушество в том, что в ней часто вырабатываются деревья доказательства, легко доступные для понимания людей, поскольку само формирование доказательства осуществляется целенаправленно.
Резолюция с входными высказываниями В стратегии Ъ. резолюции с входными высказываниями (шрц1 гезо1цйоп) на каждом этапе резолюции комбинируется одно из входных высказываний (из базы знаний или запроса) с некоторым другим высказыванием. В доказательстве, показанном на рис. 9.7, использовались только этапы резолюции с входными высказываниями и поэтому дерево доказательства имело характерную форму в виде единого "хребта" 423 Глава 9.
Логический вывод в логике первого порядка с отдельными высказываниями, комбинирующимися с этим хребтом. Очевидно, что пространство деревьев доказательства такой формы меньше по сравнению с пространством всех возможных графов доказательства. В хорновских базах знаний как своего рода стратегия резолюции с входными высказываниями может рассматриваться правило отделения, поскольку при использовании этого правила некоторая импликация из первоначальной базы знаний комбинируется с некоторыми другими высказываниями.
Таким образом, нет ничего удивительного в том, что метод резолюции с входными высказываниями является полным применительно к базам знаний, которые нахолятся в хорновской форме, но в общем случае он неполон. Стратегия 'в. линейной резолюции (1)пеаг гезо1цйоп) представляет собой небольшое обобшение, в котором допускается применять в одной операции резолюции высказывания Р и О, если Р находится в первоначальной базе знаний или Р является предком 0 в дереве доказательства. Метод линейной резолюции является полным. Обобщение В методе 'ж обобшения 1лцЬвплзрг)оп) устраняются все высказывания, которые обобшаются некоторым сушествуюшим высказыванием из базы знаний (т.е.
являются более конкретными по сравнению с ним). Например, если в базе знаний есть высказывание Р)х), то нет смысла вводить в нее высказывание Р(А) и еше меньше смысла вводить Р)А) м 0)в). Обобшение позволяет поддерживать небольшие размеры базы знаний и тем сал1ым ограничивать размеры пространства поиска. Средства автоматического доказательства теорем Средства автоматического доказательства теорем (называемые также средствами авгноматизированного формироваоия рассумсдений) отличаются от языков логического программирования в двух отношениях.
Во-первых, большинство языков логического программирования поддерживает только хорновские выражения, тогда как средства автоматического доказательства теорел1 поддерживают полную логику первого порядка. Во-вторых, в программах на таком типичном языке логического програчлшрования, как Рго!о8, переплетаются логика и управление. Например, выбор программистом выражения Л: — В, С вместо А: — С, В может повлиять на выполнение программы.
С другой стороны, в большинстве средств автоматического доказательства теорем синтаксическая форма, выбранная для высказываний, не влияет на результаты. Для средств автоматического доказательства теорем все еше требуется управляющая информации, чтобы они могли функционировать эффективно, но эта информация обычно хранится отдельно от базы знаний, а не входит в состав самого представления знаний. Большинство исследований в области средств автоматического доказательства теорем посвяшено поиску стратегий управления, которые приводят к общему повьппению эффективности, а не только к увеличению быстродействия.
Проект одного из средств автоматического доказательства теорем В этом разделе описана программа автоматического доказательства теорем Ос сел (Огйап)гед Тес)гп)с)цез Гог Т)леогет-ргон)пй апг) Е)Тес)|не Кезеагс)л) )1018]; в этом описании особое внимание будет уделено применяемой в ней стратегии управления. Подготавливая любую задачу для программы Оссег, пользователь должен разделить знания на четыре описанные ниже части. 424 Часть Н1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
