Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 113
Текст из файла (страница 113)
Знания и рассуждения ° Множество выражений, известное как множество поддержки (или яоя — кег оГ ьцрроп), в котором определяются важные факты о данной задаче. На каждом этапе резолюции операция резолюции применяется к одному из элементов множества поддержки и к другой аксиоме, поэтому поиск сосредоточивается на множестве поддержки.
° Множество полезных аксиом (изаЫе ах!огп), которое выходит за пределы множества поддержки. Эти аксиомы предоставляют фоновые знания о проблемной области. Определение границы межлу тем, что должно войти в состав задачи (и поэтому в множество яоя) и что относится к фоновым знаниям (и поэтому должно войти в число полезных аксиом), передается на усмотрение пользователя. ° Множество уравнений, известных как правила перезаписи (ге)уг)гез), или демодуляторы (оепзог)ц!агогя). Хотя демодуляторы представля)от собой уравнения, они всегда применяются в направлении слева направо, поэтому определяют каноническую форму, в которой должны быть представлены все упрощенные термы.
Например, демодулятор хьо=х указывает, что любой терм в форме х+ О должен быть заменен термом х. ° Множество параметров и выражений, который определяет стратегию управления. В частности, пользователь задает эвристическую функцию для управ- леши поиском и функцию фцльтрац)ш для устранения некоторых подцелей как не представляющих интереса. Программа Оггег действует по принципу постоянного применения правила резолюции к одному из элементов множества поддержки и к одной из полезных аксиом. В отличие от системы Рго!оя, в этой программе используется определенная форма поиска по первому наилучшему совпадению. Ее эвристическая функция измеряет "вес" каждого выражения с учетом того, что наиболее предпочтительными являются выражения с наименьшими весами. Задача точной формулировки эвристической функции возлагается на пользователя, но, вообще говоря, вес любого выражения должен коррелировать с его размером или сложностью. Единичные выражения оцениваются как имеющие наименьший вес, поэтому такой метод поиска может рассматриваться как обобщение стратегии с преимущественным использованием единичных выражений.
На каждом этапе программа Оьсег перемещает выРажение "с наименьшим весом" из множества поддержки в список полезных аксиом и добавляет в множество поддержки некоторые непосредственные следствия применения операции резолюции к выражению с наименьшим весом и к элементам списка полезных аксиом. Программа Огсег ОСтанаВЛИваетСя, ЕсЛи Обнаруживает противоречие или если возникает такая ситуация, что в множестве поддержки не остается больше выражений.
Алгоритм работы этой программы показан более подробно в листинге 9.5. Листинг 9.5. Набросок структуры программы автоматического доказательства теорем оееег. Эвристическое управление прнменястся прн выборе выражения "с наименьшим весом" н в функции рз ьеег, которая устраняет ю рассмотрения такие выраженпя, которые не представляют интереса ргосеГ)пге Ос сея ! яся, ияаЫе) кпрпсвз яоя, множество поддержки — выражения, определяющие решаемую задачу (глобальная переменная) 425 Глава 9. Логический вывод в логике первого порядка ияаЬ1е, множество фоновых знаний, которые потенциально могут быть релевантнымн для данной задачи гереае с1аияе ь- элемент множества яоя с наименьшим весом переместить выражение с1аияе нз множество яоя в множество ияаЬ1е Ргосеяя(?птег(с1аияе, ияаЬ1е), яоя) ипсг1 яоя = [) ог обнаружится опровержение гипссфоп 1плег(с1аияе, ияаЬ1е) гесигпв множество выражений с1аияея применить правило резолюции к выражению с1аияе и каждому элементу множества ияаЬ1е возвратить полученное множество с1аияея после применения функции РЬ1еег ргосейиге Ргосевя(с1аияея, яоя) гог еасн с1аияе фп с1аияея йо с1аияе ь- Яжвр11ву(с1аияе) выполнить слияние идентичных литералов отбооснть выраженке с1аияе, если оно представляет собой тавтологию яоя о- [с1аияе 1 яоя) фв с1аияе не имеет литералов, то обнаружено опровержение ЬЕ с1аияе имеет один литерал, то искать единичное опровержение Расширение системы Рге1оя Ец(е один способ создания средства автоматического доказательства теорем состоит в тОм, )тоб) | на шть с комдив~тора Рго[оя и дополнить его в целях получения непротиворечивого и полного средства формирования рассуждений для полной логики первого порядка.
Именно этот подход был принят при создании программы РТТР (Рго1ой Тес)шо)оду Тйеогеш Ргочег) [1463]. Как описано ниже, программа РТТР включает пять суп(ественных дополнений к системе Рго)оя, позволяюших восстановить полноту и выразительность алгоритма обратного логического вывода. ° В процедуру унификации снова вводится проверка вхождения для того, чтобы эта процедура стала непротиворечивой. ° Поиск в глубину заменяется поиском с итеративным углублением.
Это позволяет добиться того, чтобы стратегия поиска стала полной, а увеличение продолжительности поиска измерялось лишь постоянной зависимостью от времени. ° Разрешается применение отрицаемых литералов (таких как р(х) ). В этой реализации имеется две отдельные процедуры; в одной из них предпринимается попытка доказать Р, а в другой — доказать — р. ° Выражение с п атомами хранится в виде и различных правил.
Например, при наличии в базе знаний выражения л е= В л С должно быть также предусмотрено хранение в ней этого выражения, представленноп) как — В ~ С л А и как 426 Часть Н!. Знания и рассуждения — С е= В л А. Применение такого метода, известного под названием 'в. блокирование (1ос)()пя), означает, что текущая цель требует унификации только с головой каждого выражения, и вместе с тем позволяет должным образом учитывать отрицание. ° Логический вывод сделан полным (даже для нехорновских выражений) путем добавления правила резолюции с линейным входным выражением: если текушая цель унифицируется с отрицанием одной из целей в стеке, то данная цель может рассматриваться как решенная.
В этом состоит один из способов рассуждения от противного. Предположим, что первоначальной целью было высказывание Р и что эта цель свелась в результате примЕНЕНИЯ РЯда этапов логического вывода к цели — Р. Тем самым установлено, что — Р =-> Р, а это выражение логически эквивалентно Р. Несмотря на этп изменения, программа РТТР сохраняет свойства, благодаря которым обеспечивается высокое быстродействие системы Рго(оя. Операции унификации все еще осу(цествля)отея посредством непосредственной модификации переменных, а отмена связывания выполняется путем разгрузки контрольного стека во время возврата.
Стратегия поиска все еше основана на резолюции с применением входных выражений, а это означает, что в каждой операции резолюции участвует одно из выражений, содер»га)цихся в первоначальной формулировке задачи (а не какое-то произвош)ое выраже~ше). Такой подход по~полает осуществить компиляцию всех выражений из первоначальной формулировки залачп. Основным недостатком программы РТТ1' является то, что пользователь должен отказаться от любых попыток взять на себя управление поиском решений.
Каждое правило логического вывода в этой системе использустся и в его первоначальной, и в контрапозитивной форме, Это может привести к выполнению таких операций поиска, которые противоречат здравому смыслу. Например, рассмотрим следующее правило: (Г(х,у) = Г(а,Ь)) с= (х =- а) л (у = Ь) Если бы оно рассматривалось как правило Рго!оя, то применялся бы разумный способ доказательства того, по два терма Г равны. Но в системе РТТР должно быть также сформировано контрапозитивное правило: (х а а) с= (Г(х,у) а Г(а,Ь) ) л (у = Ь) По-видимому, попытка доказать, что любые два терма, х и а, являются разными, привела бы к непроизводительным затратам ресурсов.
Применение средств автоматического доказательства теорем в качестве помощников До сих пор в этой книге любая система формирования рассуждений рассматривалась как независимый агент, который должен был принимать решения и действовать самостоятельно. Еще одно направление использования средств автоматического доказательства теорем состоит в том, что они должны служить в качестве помощников, предоставляя консультации, скажем, математикам.
При эксплуатации подобных систем в режиме помощи математик действует в роли руководителя, очерчивая стратегию определения того, что должно быть сделано в следующую очередь, а затем передавая системе автоматического доказательства теорем просьбу проработать все детали. Это позволяет в определенной степени устранить проблему полураз- 427 Глава 9. Логический вывод в логике первого порядка решимости, поскольку руководитель научной разработки может отменить запрос и опробовать другой подход, если поиск ответа на запрос потребовал слишком много времени.
Любая система автоматического доказательства теорем может также действовать в качестве 7ж средства проверки доказательства; при ее использовании в таком режиме доказательство предоставляется человеком в виде ряда довольно крупных этапов; отдельные операции логического вывода, которые требуются для того, чтобы показать, что каждый из этих этапов является непротиворечивым, определяются системой. В частности, '~. сократовское средство формирования рассуждений [ьосгайс геазопег) представляет собой такую систему автоматического доказательства теорем, в которой функция Аэй является неполной, но эта система всегда позволяет прийти к определенному решению, если ей будет задан правильный ряд вопросов. Таким образом, сократовские средства формирования рассуждений становятся хорошими помошниками, прн условии, что есть руководитель, способный составить правильный ряд вызовов функции Аэй.
Одной из сократовских систем формирования рассуждений для математиков является Опбс [1005]. Области практического использования средств автоматического доказательства теорем Средства автоматического доказательства теорем позволили получить новейшие математические результаты, программа БАм [Беш)-Аигогпагед ма1[зешаг[сз) была первой программой, с помошыо которой удалось доказать одну из лемм в теории решеток [602].
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
