Часть 1.

Люгер, Дж.Ф.

Искусственный интеллект. Часть 5-6. 2001.

Люгер, Джордж, Ф. Искусственный интеллект: стратегии и методы решения сложных проблем, 4-е издание. : Пер. с англ. - М.: Издательский дом "Вильяме", 2003. - 864 с.-С. 519-775.

Часть V

Дополнительные вопросы решения задач

искусственного интеллекта

Точность - это не истина... - Генри Матисс (Henri Matisse)

Время настоящее и время прошедшее - это лишь настоящее для времени будущего, а время будущее содержится в прошедшем...

- Т. С. Элиот (Т. S. Eliot), Бернт Нортон

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

- Кристофер Александер (Christopher Alexander)

Автоматические рассуждения и естественный язык

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

519

к части III обсуждались преимущества и недостатки слабых методов решения задач (weak method). Проблема использования таких методов обусловлена сложностью пространства поиска и трудностью описания конкретных знаний о мире с помощью общего представления. Несмотря на успешное развитие экспертных систем и сильных методов решения задач, во многих случаях требуются более общие подходы. На самом деле стратегии управления в самих экспертных системах основаны на использовании слабых методов. Многообещающие результаты по созданию могут быть получены в области автоматических рассуждений и доказательства теорем (automated reasoning). Эти приемы нашли свое применение во многих важных областях, включая разработку интегрированных сетей, верификацию и доказательство корректности программ, а также, косвенно, при создании языка программирования PROLOG. В главе 12 рассматриваются вопросы, связанные с автоматическими рассуждениями.

Сложность понимания естественных языков при решении задач искусственного интеллекта объясняется многими причинами. В частности, для использования языка необходимы большой объем знаний, способностей и опыта. Успешное понимание языка требует осмысления естественного мира, знания человеческой психологии и социальных аспектов. Для этого нужна реализация логических рассуждений и интерпретация метафор. Из-за сложности и многогранности человеческого языка на первое место выходит проблема исследования представления знаний. Попытки таких исследований увенчались успехом лишь частично. На основе знаний были успешно разработаны программы, понимающие естественный язык в отдельных предметных областях. Возможность создания систем, решающих проблему понимания естественного языка, до сих пор является предметом споров.

Методы представления, описанные в главе 6, в том числе семантические сети, сценарии и фреймы, играют важную роль в решении задачи понимания естественного языка. В последнее время для решения этой задачи привлекаются методы корреляционного анализа языковых шаблонов. Языковые конструкции - это не случайный набор звуков или слов. Их можно моделировать на основе байесовского подхода. В главе 13 будут рассмотрены синтаксические, семантические и стохастические методы понимания естественного языка.

С широким распространением технологий World Wide Web и интенсивным использованием механизмов поиска вопрос понимания естественного языка стал еще важнее. Общий поиск полезной информации в неструктурированном тексте, возможность резюмирования информации, или "понимания" текста, - это важнейшие новые технологии. Теоретические основы программных средств, базирующихся на символьном представлении и стохастическом распознавании образов, представлены в главе 13.

И, наконец, в части VI будут рассмотрены многие структуры данных, используемые при решении задач понимания естественного языка. В разделах 14.7 и 15.11 описаны семантические сети и фреймовые системы, а в разделе 14.9 - рекурсивный семантический сетевой анализатор. В главе 16 обсуждаются некоторые существующие проблемы в понимании языка, обучении и решении сложных задач.

520

Глава 12. Автоматические рассуждения

Как это получается, - спросил этот проницательный человек, - когда мне приходит идея, я могу выйти за ее рамки и связать с другими, не содержащимися в ней, как будто эти идеи неразрывно связаны с первоначальной ?

- Иммануил Кант (Immanuel Kant), Prolegomena to a Future Metaphysics

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

- Симон (Simon), Decision-Making and Administrative Organization, 1944

Доказательство - это искусство, а не наука... - Вое (Wos), Automated Reasoning, 1984

12.0. Введение в слабые методы доказательства теорем

В [Wos и др., 1984] сказано, что система автоматического доказательства "применяет однозначные описания для представления информации, точные правила вывода для формирования заключений и внимательно сформулированные стратегии для управления этими правилами". Авторы добавляют, что применение стратегий к правилам вывода для получения новой информации - это искусство. "Хороший выбор представления подразумевает использование обозначений, повышающих вероятность решения проблемы, и включение полезной, хотя и не самой необходимой, информации. Хорошие правила вывода- это правила, удачно использующие выбранное представление. Хорошие стратегии- это принципы управления правилами вывода, повышающие эффективность программы автоматических рассуждений."

Отсюда следует, что для построения систем автоматических рассуждений используются слабые методы решения проблем. Они строятся на таком однородном представлении, как теория предикатов первого порядка (глава 2), теория хорновских выражений (раздел 12.3) или операторов разрешения (раздел 12.2). Правила вывода должны быть

521 (ПРОПУСК с.522)

выражение (BvB)®B вместо В можно подставить ¬А и получить выражение.

Замена позволяет использовать вместо выражения его определение или эквивалентную форму. Например, при логической эквивалентности выражений ¬AvB и А®В выражение ¬Av¬A можно заменить А® ¬А.

Открепление - это правило вывода, которое в главе 2 было названо правилом модус поненс.

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

Метод подстановки напрямую применяется для текущей задачи, чтобы привести ее

к известным аксиомам и теоремам.

Если этот метод не приводит к успешному доказательству, используются все возможные открепления и замены, и для каждого из результатов снова применяется метод подстановки. Если получить доказательство теоремы не удается, то все эти результаты добавляются в список подзадач (subproblem list).

Затем для поиска новой подзадачи, решение которой обеспечивает доказательство

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

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

Эти четыре метода применяются до тех пор, пока не будет найдено решение, не исчерпается список подзадач, память или время, выделенные для решения задачи. Таким образом, система LT выполняет поиск в ширину в пространстве задач.

В исполняемой программе подстановка, замена и открепление выполняются в рамках процесса проверки соответствия (matching process). Допустим, необходимо доказать утверждение р® (q ® р). В процессе проверки соответствия сначала выявляется одна из аксиом p ® {qvp) как наиболее соответствующая в терминах различия для данной области определения (в данном случае в обоих выражениях совпадает основной логический оператор ®). Затем при проверке соответствия устанавливается идентичность левых операндов основного логического оператора обоих выражений. И, наконец, определяется различие правых операндов. На основе различия между операторами ® и v можно предложить очевидную замену для доказательства теоремы. Процесс проверки соответствия помогает управлять поиском при реализации всех подстановок, замен и откреплений. Он гораздо более эффективен, чем простой метод проб и ошибок, что обеспечивает успешное решение задач с помощью программы LT.

Рассмотрим эффективность проверки соответствия на примере доказательства теоремы 2.02 из книги [Whitehead и Russell, 1950]: p®(q®p). В процессе проверки соответствия в качестве замены находится аксиома р® (qvp). Подстановка ¬q вместо q приводит к доказательству теоремы. Проверка соответствия, управление подстановкой и правила замещения приводят к прямому доказательству теоремы без привлечения поиска в пространстве других аксиом или теорем.

Глава 12. Автоматические рассуждения 523

Для второго примера постараемся с помощью программы LT доказать утверждение

(AvA) ®A - в процессе проверки соответствия выявляется наилучшая аксиома из

пяти возможных.

(¬Av¬A) ® ¬A - подстановка ¬А вместо А.

(А®¬А) ® ¬А - замена v или ¬ на ®.

(p®¬p) ® ¬p - подстановка р вместо А.

Что и требовалось доказать.

Программа LT доказывает эту теорему на основе пяти аксиом примерно за десять секунд. Реальное доказательство выполняется за два этапа и не требует поиска. На первом этапе в процессе проверки соответствия выбирается самая подходящая аксиома, поскольку ее форма наиболее близка к утверждению, которое требуется доказать: выражение ® предложение. Затем вместо А подставляется ¬А. Этим определяется второй (и последний) этап, который приводит к замене v на ®. Программа LT не только является первым примером системы автоматических рассуждений, но и демонстрирует роль стратегий поиска и эвристик в средствах автоматического доказательства теорем. Во многих случаях LT за несколько шагов приходит к таким решениям, которые с большим трудом можно найти только путем полного перебора. Некоторые теоремы не решаются с помощью программы LT, поэтому авторы программы внесли некоторые предложения по ее улучшению.

Примерно в это же время исследователи из технологического института Карнеги (Carnegie Institute of Technology), а также специалисты из Йельского университета [Moore и Anderson, 1954] начали высказывать свои идеи о способах решения логических задач. И хотя их основной целью было изучить процессы человеческого мышления, решающие этот класс задач, они сравнили принципы решения задач человеком с подходами, реализованными в компьютерных программах наподобие LT. Это положило начало новой научной области, получившей современное название психологии обработки информации (information processing psychology). Данная наука пытается объяснить наблюдаемое поведение организмов с помощью примитивной программы обработки информации, моделирующей такое поведение [Newell и др., 1958]. Это исследование также стало одной из первых работ в области науки о мышлении - когнитологии (cognitive science), о которой речь пойдет в разделе 16.2 [Luger, 1994].

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

Рассмотрим простейший пример. Если начальное утверждение имеет вид p®q, а целью является ¬pvq, то различие состоит в том, что в исходном выражении участвует

символ ®, а в целевом - v (а также в исходном утверждении есть выражение р, а в целевом - ¬р). Таблица отличий должна содержать различные способы замены ® на v,

а также удаления отрицания. Такие преобразования необходимо поочередно применять до полного устранения отличий и доказательства теорем.

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

524

В среднем столбце табл. 12.1 [Newell и Simon, 19636] представлены двенадцать правил преобразования для решения логических задач. В правом столбце приводятся рекомендации по их применению.

В табл. 12.2 представлено доказательство, сгенерированное человеком [Newell и Simon, 19636]. При этом человеку, не имеющему опыта в решении задач формальной логики, были предоставлены правила преобразования из табл. 1.2.1. Требовалось преобразовать выражение (R?¬P)•( ¬R?Q) к виду ¬ (Q•P). В обозначениях из главы 2 символ

~ обозначает ¬, • обозначает ?,а? - ® В табл. 12.1 символ ® или « обозначает корректную замену. В правом столбце табл. 12.2 указаны правила из табл. 12.1, применяемые на каждом этапе доказательства.

525

В работе [Newell и Simon, 19636] стратегии решения задач человеком названы процессом уменьшения различий, а общий процесс использования преобразований для уменьшения различий в конкретной задаче - анализом целей и средств. Алгоритм выполнения этого анализа получил название системы решения общих задач GPS (General Problem Solver).

На рис. 12.1 показаны схема функционирования и таблица связей для GPS. Требуется преобразовать выражение А в выражение В. Для этого сначала необходимо найти различие D между А и В. Во втором блоке первой строки решается подзадача - уменьшение D. Третий блок указывает на то, что процедура уменьшения различия является рекурсивной. Уменьшение различий выполняется во второй строке, где для D выбирается оператор О. На самом деле список операторов формируется на основе таблицы связей. Операторы из этого списка последовательно проходят тест применимости (feasibility test). В третьей строке на рис. 12.1 используется нужный оператор и уменьшается D.

Используемая в GPS модель решения задач основана на двух компонентах. Первый - описанная выше общая процедура сравнения двух состояний и уменьшения их различий. Второй - таблица связей (table of connections), описывающая взаимосвязи между существующими различиями и конкретными преобразованиями, применяемыми для их уменьшения. Таблица связей для 12 преобразований, описанных в табл. 12.1, показана на рис. 12.1. Для уменьшения различий в алгебраической форме при решении задач наподобие ханойских башен или моделировании более сложных игр, таких как шахматы, могут применяться другие таблицы связей. Многочисленные применения системы GPS описаны в [Ernst и Newell, 1969].

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

Система GPS послужила толчком для развития исследований во многих направлениях. Одним из них стало использование методов искусственного интеллекта для анализа человеческого поведения в процессе решения задач. В частности, используемые в GPS методы анализа целей и средств были заменены системой логического вывода, представляющей собой более точную модель обработки информации человеком (глава 16). В современных экспертных системах правила вывода используются вместо отдельных элементов таблицы отличий GPS.

526

Тест на применимость (предварительный) для описанной логической задачи:

Совпадает ли основной логический оператор (т.е. А'В -» В хуже, чем PvQ)?

Не слишком ли велико выражение (т.е. (А\/В)ш(А\/С) -> Av{B'C) хуже, чем P'Q)7

Не является ли оператор слишком простым (т.е. А-^А'А применимо к любому выражению)?

Удовлетворяются ли второстепенные условия (например, правило 8 применимо только для

основного выражения)?

Методы GPS получили свое развитие и в других интересных направлениях. Так, вместо таблицы отличий в системах STRIPS и ABSTRDPS стали использовать таблицы операций (operator table) для планирования (planning). Планирование - это важный аспект управления роботами. Чтобы решить задачу, например, перейти в другую комнату и принести некоторый предмет, компьютер должен разработать план, определяющий действия робота. Сначала необходимо положить предмет, который робот держит "в руках", затем подойти к двери, выйти из комнаты, найти нужную комнату, войти в нее, подойти к объекту и т.д. При

527

формировании планов для системы STRIPS (Stanford Research Institute Problem Solver) используется таблица операций, выступающая аналогом таблицы отличий GPS [Fikes и Nilsson, 1971, 1972], [Sacerdotti, 1974]. Каждой операции (примитивному действию робота) в этой таблице соответствует набор предусловий, аналогичных тесту применимости из рис. 12.1. Таблица операций также содержит списки добавления и удаления, с помощью которых модифицируется модель "мира" после выполнения операций. Система планирования, подобная STRIPS, была описана в разделе 7.4, а ее реализация на языке PROLOG будет рассмотрена в разделе 14.5.

Итак, первыми моделями автоматических рассуждений в области искусственного интеллекта являются системы Logic Theorist (LT) и General Problem Solver (GPS). В этих программах реализованы слабые методы решения задач, использовано унифицированное представление, набор правил вывода и методы или стратегии применения этих правил. Эти же компоненты применяются в разрешающих процедурах доказательства теорем (resolution proof procedure) - более современном и мощном аппарате автоматических рассуждений.

12.2. Доказательство теорем методом резолюции

12.2.1. Введение

Резолюция - это один из приемов доказательства теорем в области исчисления высказываний или предикатов, относящийся к сфере искусственного интеллекта с середины 60-х годов прошлого столетия [Bledsoe, 1977], [Robinson, 1965], [Kowalski, 19796]. Резолюция - это правило вывода, используемое для построения опровержений (refutation) (подраздел 12.2.3). Важным практическим применением метода резолюции, в частности при создании систем опровержения, является современное поколение интерпретаторов языка PROLOG (рис. 12.2).

Принцип резолюции (или разрешения), введенный в работе [Robinson, 1965], описывает способ обнаружения противоречий в базе данных дизъюнктивных выражений при минимальном использовании подстановок. Опровержение разрешения - это способ доказательства теоремы, основанный на формулировке обратного утверждения и добавлении отрицательного высказывания к множеству известных аксиом, которые по предположению считаются истинными. Затем правило резолюции используется для доказательства того, что такое предположение ведет к противоречию (доказательство от обратного). Поскольку в процессе доказательства теоремы показывается, что обратное утверждение несовместимо с существующим набором аксиом, исходное утверждение должно быть истинным. В этом и состоит доказательство теорем.

Процесс доказательства от обратного состоит из следующих этапов.

Предположения или аксиомы приводятся к дизъюнктивной форме (clause form)

(подраздел 12.2.2).

К набору аксиом добавляется отрицание доказываемого утверждения в дизъюнктивной форме.

Выполняется совместное разрешение этих дизъюнктов, в результате чего получаются новые основанные на них дизъюнктивные выражения (подраздел 12.2.3).

Генерируется пустое выражение, означающее противоречие.

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

о том, что отрицание отрицания - истинно (подраздел 12.2.4).

528

Резолюция - это согласованное правило вывода (см. главу 2). Однако оно не является полным. Резолюция является полной в смысле опровержения, т.е. если в наборе высказываний имеется противоречие, то на основе этого набора всегда можно сгенерировать пустое или нулевое выражение. Этот вопрос более подробно обсуждается при описании существующих стратегий построения опровержений в подразделе 12.2.4. Для доказательства от обратного требуется, чтобы аксиомы и отрицание исходного утверждения были приведены к нормальной дизъюнктивной форме (clause form). В дизъюнктивной форме логическая база данных представляется в виде набора дизъюнкций, или литералов (literal). Литерал - это простейшее выражение или его отрицание.

Наиболее типичная форма резолюции, получившая название бинарной резолюции (binary resolution), применяется к двум выражениям, одно из которых является литералом, а другое - его отрицанием. Если литералы содержат переменные, то их необходимо унифицировать и привести к эквивалентному виду. Затем генерируется новое выражение, состоящее из дизъюнктов всех предикатов этих двух выражений, за исключением этого литерала и его отрицания, которые считаются "вычеркнутыми".

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

Докажем, что утверждение "Фидо смертен" следует из утверждений "Фидо - собака", "Собаки - это животные" и "Все животные смертны". Преобразовывая эти предположения в предикатную форму и применяя правило отделения, получим следующее.

Собаки - это животные: "(X)(dog(X) ® animal(X)).

Фидо - собака: dog(fido).

На основе правила отделения и подстановки [fido/X] получим: animal(fido).

Все животные смертны: "(Y)(animal(Y)® die(Y)).

На основе правила отделения и подстановки {fido/Y} получим: die(fido).

По принципу резолюции эти предикаты необходимо преобразовать в дизъюнктивную форму.

Предикатная форма Дизъюнктивная форма

"(X)(dog(X)->an/ma/(X)) ¬dog(X) v animal(X)

dog{fido) dog(fido)

"(Y)(animal(Y)^die(Y)) ¬animal(Y) v die(Y)

Запишем отрицание целевого утверждения "Фидо смертен".

¬die(fido) ¬die(fido)

Выполняя резолюцию с использованием обратных литералов, получим новые дизъюнктивные выражения, представленные на рис. 12.2. Этот процесс зачастую называют созданием конфликта (clashing).

Символ ? на рис. 12.2 означает пустой дизъюнкт или противоречие. Он символизирует конфликт предиката и его отрицания, т.е. наличие двух противоречивых высказываний в пространстве дизъюнктов. Последовательность подстановок (операций унификации),

Глава 12. Автоматические рассуждения 529

применяемая для приведения предикатов к эквивалентной форме, позволяет определить значения переменных, при которых целевое высказывание истинно. Например, определяя, смертно ли некоторое существо, следует построить отрицание в виде - ¬($(Z)die(Z), а не ¬die(fido). Подстановка {fidolZ} на рис. 12.2 означает, что Фидо - представитель животного мира, который смертен. Более подробно этот пример будет рассмотрен в последующих разделах.

12.2.2. Построение дизъюнктивной формы для опровержения разрешения

Метод резолюции требует преобразования всех операторов базы данных, описывающих ситуацию, к стандартной дизъюнктивной форме. Это связано с тем, что резолюция - это операция над парой дизъюнктов, приводящая к созданию новых дизъюнктов. Такая форма представления базы данных называется конъюнкцией дизъюнктов (conjunction of disjuncts). Это конъюнкция, поскольку по предположению все выражения в базе данных одновременно являются истинными. В то же время - это дизъюнкция, поскольку каждое выражение описывается с помощью оператора дизъюнкции. Таким образом, всю базу данных, представленную на рис. 12.2, можно описать в следующей форме.

К этому выражению следует добавить (с помощью конъюнкции) отрицание целевого выражения, в данном случае ¬die(fido). Таким образом, база данных описывается как набор дизъюнктов, а операторы конъюнкции можно опустить.

530 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

Рассмотрим алгоритм, представляющий собой последовательность преобразований по приведению набора предикатов к дизъюнктивной форме. В [Chang и Lee, 1973] показано, что такие преобразования можно использовать для приведения любого множества выражений в области теории предикатов к набору дизъюнктов, противоречивому в том и только в том случае, если исходное множество выражений является противоречивым. Такая дизъюнктивная форма не является строго эквивалентной исходному множеству предикатов, поскольку в ней могут быть утрачены некоторые аспекты интерпретации. Это связано с тем, что сколемизация ограничивает возможные подстановки для переменных, связанных квантором существования [Chang и Lee, 1973]. Однако при этом сохраняется значение истинности выражений. Следовательно, если в исходном множестве предикатов есть противоречие, то оно остается и в дизъюнктивной форме. Такие преобразования не нарушают полноты доказательства опровержения.

Проиллюстрируем процесс приведения к конъюнктивной нормальной форме на конкретном примере и дадим краткое пояснение каждому из шагов. Эти пояснения не претендуют на роль доказательства эквивалентности преобразований для теории предикатов в целом.

В следующих выражениях согласно принятым в главе 2 соглашениям прописными буквами обозначены переменные (IV, X, У и Z), строчными буквами из середины алфавита (I, тип) - константы и граничные значения, а начальными строчными буквами (а, b, с, d и е) - имена предикатов. Для улучшения читабельности выражений используется два типа скобок: круглые и квадратные. В качестве примера рассмотрим выражение, где X, У и Z - переменные, а I- константа.

1. Сначала исключим оператор ® с использованием эквивалентной формы, приведен

ной в главе 2: a®b=¬avb. После этого преобразования выражение (i) примет вид

2. Теперь выполним преобразование операторов отрицания. Для этого можно вос

пользоваться формулами, описанными в главе 2, например такими.

Используя эти тождества, формулу (ii) можно привести к виду

3. Теперь переименуем все переменные таким образом, чтобы переменные, ограниченные

различными кванторами, имели различные имена. (Эта операция называется стандартизацией переменных.) Как было указано в главе 2, имя переменной - это лишь обозначение "знакоместа". Оно не влияет ни на истинность выражения, ни на общность высказывания. Воспользуемся на этом шаге следующим преобразованием

Поскольку в (ill) содержится два вхождения переменной X, переименуем ее следующим образом

Глава 12. Автоматические рассуждения 531

4. Переместим все кванторы влево, не изменяя порядок их следования. Это можно

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

именами переменных. Формула (iv) примет вид

На этом шаге получено выражение в предваренной, или пренексной нормальной форме (prenex normal form), поскольку все кванторы вынесены в начало предложения.

5. Теперь исключим все кванторы существования с помощью процесса сколемизации

(skolemization). В выражении (v) используется квантор существования для переменной Y. Если выражение содержит переменную, связанную квантором существования, например ($Z)(foo(..., Z, ...)), значит, существует значение переменной Z, при котором выражение foo истинно. Сколемизация позволяет определить такое значение. При этом сколемизация необязательно показывает, как получить это значение. Она лишь является методом присвоения имени значению, которое должно существовать. Если искомым значением является к, то указанное выражение можно записать в виде foo(..., к, ...). Итак, ($(X)(dog(X)) можно заменить выражением dog(fido), где имя fido взято из области определения X для обозначения отдельного экземпляра X. При этом fido называется сколемовской константой (skolem constant). Если предикат имеет несколько аргументов, и переменная, связанная квантором существования, следует за переменными, связанными квантором всеобщности, то она должна быть функцией этих переменных. Это отражено в процессе сколемизации. Рассмотрим выражение

Оно означает, что у каждого человека есть мать. Каждый человек - это переменная X, а существование матери - функция от конкретно взятого человека X. В результате сколемизации получим

Это означает, что у каждого X есть мать (значение т для этого X). Вот другой пример. Выражение

в результате сколемизации можно привести к виду

Связанные квантором существования переменные У и Z находятся под квантором всеобщности переменной X (справа от нее), но не под квантором всеобщности переменной W. Поэтому каждую из этих переменных можно заменить сколемовской функцией от X. Заменяя переменную Y сколемовской функцией f(X), a Z - g(X), формулу (v) преобразуем к виду

После сколемизации можно перейти к п. б, в котором просто удаляется префикс.

6. Исключим все кванторы всеобщности. К этому моменту (после п. 5) остались лишь

переменные, связанные кванторами всеобщности, и все конфликты переменных

устранены (в п. 3). Следовательно, все кванторы можно опустить, поскольку любая

процедура доказательства предполагает выполнение утверждения для всех переменных. Формула (vi) примет вид

532 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

7. Теперь представим это выражение в виде конъюнкции дизъюнктов. Для этого вос

пользуемся свойствами ассоциативности и дистрибутивности операций ? и v. На

помним (глава 2), что

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

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

Окончательно выражение (vii) примет вид

8. Теперь выделим каждый конъюнкт в отдельное выражение. Предложение (viii) будет представлено в виде двух выражений

9. И, наконец, снова разделим переменные, т.е. присвоим переменным в каждом вы

ражении, сгенерированном в п. 8, различные имена. Это делается на основе приве

денного в главе 2 тождества

которое в свою очередь следует из того, что имена переменных - это лишь обозначения знакомест. Теперь, вводя новые имена переменных U и V, преобразуем формулы (ixa) и (ixb) к виду

Значение такой стандартизации станет понятно только после описания процедуры унификации в процессе резолюции. Она сводится к поиску наиболее общей унифицированной формы, обеспечивающей эквивалентность предикатов в двух выражениях, а затем ее подстановке вместо всех переменных с одинаковыми именами в рамках одного выражения. Так, если имена некоторых переменных совпадают, то в процессе унификации они могут быть переименованы с последующей (возможной) потерей общности решений.

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

12.2.3. Процедура доказательства на основе бинарной резолюции

Процедура опровержения разрешения (resolution refutation) дает ответ на запрос или

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

Глава 12. Автоматические рассуждения 533

ставленному нулевым выражением (?). Противоречие возникает при попарной резолюции выражений из базы данных. Если резолюция не приводит к противоречию напрямую, то полученное в результате выражение - резольвента (resolvent) - добавляется в базу данных выражений, и процесс продолжается.

Прежде чем показать, как происходит процесс резолюции в исчислении предикатов, рассмотрим пример из области исчисления высказываний (без переменных). Рассмотрим два родительских выражения р 1 и р2 из области исчисления высказываний

содержащих два литерала аi и bj при которых ¬аi= bj, где 1

Таким образом, резольвента состоит из дизъюнкции всех литералов двух родительских выражений за исключением литералов а и b.

Простое рассуждение позволит выйти за рамки принципа резолюции. Допустим, что av¬b и b v c - два истинных выражения. Заметим, что одно из значений b или ¬b обязательно истинно, а второе - ложно (bv¬b - это тавтология). Следовательно, значение одного из литералов в выражении

должнобыть истинно. Выражение a v c - это резольвента двух родительских выражений

Рассмотрим теперь пример из области исчисления высказываний. Требуется получить значение а на основе следующих аксиом (естественно, |?m=m®| для всех предложений / и т):

Приведем первую аксиому к дизъюнктивной форме.

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

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

534 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

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

Алгоритм резолюции в исчислении предикатов во многом аналогичен этому же процессу для исчисления высказываний за исключением следующих моментов.

Литерал и его отрицание в родительских выражениях дают резольвенту только в том

случае, если они унифицированы для некоторой подстановки о. Затем о применяется

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

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

связывание переменных, при котором исходный запрос является истинным. Этот процесс, получивший название извлечения ответа (answer extraction), будет описан ниже.

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

Не сложно заметить, что при простой резолюции эти выражения можно свести лишь к эквивалентной форме или тавтологии, а не к противоречию. То есть никакая подстановка не сделает их противоречивыми.

Глава 12. Автоматические рассуждения 535

В подобной ситуации можно применить факторизацию выражений (factoring). Если подмножество литералов в некотором выражении имеет наиболее общий унификатор (подраздел 2.3.2), то это выражение можно заменить новым выражением, получившим название фактора (factor). Фактор - это исходное выражение, к которому применена подстановка наиболее общего унификатора, а затем удалены оставшиеся литералы. Например, два литерала в выражении p(X) v p(f{Y)) можно унифицировать с помощью подстановки {f(Y)/X}. Выполним подстановку в обоих литералах и получим выражение P(f{Y)) v p(f{Y)), а затем заменим это выражение его фактором p{f(Y)). Любая система опровержения разрешения, включающая факторизацию, является полной в смысле опровержения. Стандартизацию переменных (выполняемую в п. 3 подраздела 12.2.2) можно интерпретировать как простое применение факторизации. Факторизацию также можно рассматривать как часть процесса вывода в процедуре гиперрезолюции (hyper resolution), описанной в подразделе 12.4.2.

Приведем пример опровержения разрешения из области исчисления предикатов. Рассмотрим следующую историю "счастливого студента".

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

Сначала запишем эти предложения в предикатной форме.

Любой студент, который сдает экзамен по истории и выигрывает в лотерею, - счастлив:

Известно, что любой удачливый или старательный студент может сдать все экзамены:

Джон не относится к числу старательных студентов, но достаточно удачлив:

Любой удачливый студент выигрывает в лотерею:

Приведем эти четыре высказывания предикатов к дизъюнктивной форме (подраздел 12.2.2).

Добавим к этим выражениям отрицание заключения в дизъюнктивной форме.

Граф опровержения разрешения, показанный на рис. 12.4, отражает процесс получения противоречия и, следовательно, доказывает, что Джон счастлив.

536 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

В качестве последнего примера рассмотрим задачу "интересной жизни".

Все небедные и умные люди счастливы. Человек, читающий книги, - неглуп. Джон умеет читать и является состоятельным человеком. Счастливые люди живут интересной жизнью. Можно ли указать человека, живущего интересной жизнью?

Предполагается, что

Тогда получим

Отрицание заключения имеет вид

Эти предикатные выражения для задачи "интересной жизни" приводятся к дизъюнктивной форме следующим образом.

Глава 12. Автоматические рассуждения 537

Граф опровержения для этого примера показан на рис. 12.5.

12.2.4. Стратегии и методы упрощения резолюции

На рис. 12.6 показано отличное от представленного на рис. 12.5 дерево доказательства для того же пространства поиска. Эти доказательства чем-то схожи, например, для резолюции они оба требуют выполнения пяти действий. Кроме того, в обоих доказательствах с помощью подстановки унификации получено, что Джон относится к числу людей, живущих "интересной жизнью".

Однако такое сходство не обязательно. При определении системы резолюции (подраздел 12.2.3) порядок комбинации дизъюнктивных выражений не устанавливался. Это очень важный момент: если в пространстве дизъюнктов существует N выражений, то имеется N2 способов их комбинации даже на первом уровне. Результирующий набор выражений тоже достаточно велик. Даже если 20% комбинаций приводят к формированию новых выражений, то на следующем этапе число возможных комбинаций станет еще больше. Для больших задач такой экспоненциальный рост достаточно быстро приводит к чрезмерной громоздкости вычислений.

538 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

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

Прежде чем приступить к описанию этих стратегий, необходимо сделать несколько пояснений. Во-первых, основываясь на определении невыполнимости выражения из главы 2, назовем набор дизъюнктивных выражений невыполнимым (a set of clauses is unsat-isfiable), если не существует интерпретации, доказывающей выполнимость этого набора. Во-вторых, правило вывода будем считать полным в смысле опровержения (refutation complete), если невыполнимость набора дизъюнктивных выражений может быть доказана с помощью одного этого правила. Этим свойством обладает процедура резолюции с факторизацией [Chang и Lee, 1973]. И, наконец, стратегия является полной, если на ее основе с помощью полного в смысле опровержения правила вывода можно гарантированно найти опровержение для невыполнимого набора дизъюнктивных выражений. Примером полной стратегии является поиск в ширину (breadth-first).

Стратегия поиска в ширину

Приведенный выше анализ сложности полного перебора дизъюнктивных выражений основывается на поиске в ширину. На первом этапе выполняется бинарная резолюция всех дизъюнктов в пространстве выражений. На следующем этапе в пространство поиска к исходным выражениям добавляются дизъюнктивные выражения, сгенерированные при резолюции дизъюнктов. На n-м этапе обрабатываются все выражения, полученные ранее, а также исходное множество дизъюнктов.

Глава 12. Автоматические рассуждения 539

Такая стратегия приводит к очень быстрому разрастанию пространства поиска, поэтому не пригодна для решения больших задач. Однако она обладает интересным свойством. Подобно поиску в ширину, эта стратегия гарантирует нахождение кратчайшего пути к решению, поскольку на каждом этапе работает только с одним уровнем и не предполагает никакого углубления. Кроме того, данная стратегия является полной, поскольку, если ее использовать достаточно долго, она гарантированно обнаружит опровержение, если таковое существует. Следовательно, стратегия поиска в ширину является достаточно адекватной для небольших задач, подобных рассмотренным выше. На рис. 12.7 приводится иллюстрация стратегии поиска в ширину для задачи "интересной жизни".

Рис. 12.7. Полное пространство состояний для задачи "интересной жизни", полученное при использовании стратеги поиска в ширину (для двух уровней)

Стратегия "множества поддержки"

Стратегия "множества поддержки" - это отличная стратегия поиска в больших пространствах дизъюнктивных выражений [Wos и Robinson, 1968]. Для некоторого набора исходных дизъюнктивных выражений S можно указать подмножество Г, называемое множеством поддержки. Для реализации этой стратегии необходимо, чтобы одна из резольвент в каждом опровержении имела предка из множества поддержки. Можно доказать, что если S - невыполнимый набор дизъюнктов, a S-T- выполнимый, то стратегия множества поддержки является полной в смысле опровержения [Wos и др., 1984].

Если исходный набор дизъюнктов является согласованным, то этим требованиям удовлетворяет любое множество поддержки, включающее отрицание исходного запроса. Эта стратегия основывается на том, что добавление отрицания доказываемого выражения приводит к противоречивости пространства возможных дизъюнктов. Множество поддержки ускоряет процесс резолюции для пар выражений, в которых одно представляет собой отрицание цели или полученное на его основе дизъюнктивное выражение.

На рис. 12.5 приведен пример применения стратегии "множества поддержки" для решения задачи "интересной жизни". Поскольку множество поддержки опровержения существует при наличии самого опровержения, оно может составлять основу полной стратегии. Одним из способов реализации такой стратегии является выполнение поиска в ширину для всех возможных множеств поддержки опровержения. Естественно, это гораздо более эффективный путь, чем поиск в ширину в пространстве всех дизъюнктивных

540

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

Стратегия предпочтения единичного выражения

Заметим, что в приведенных выше примерах резолюции противоречие возникает при появлении выражения, не содержащего литералов. Следовательно, каждый раз при получении результирующего выражения с меньшим числом литералов мы приближаемся к генерации выражения, не содержащего литералов вообще. В частности, получение выражения, состоящего из одного литерала или так называемого единичного выражения (unit clause), гарантирует, что резольвента будет меньше, чем наибольшее родительское выражение. Стратегия предпочтения единичного выражения предполагает максимальное использование единичных выражений в процессе резолюции. На рис. 12.8 эта стратегия проиллюстрирована для задачи "интересной жизни". Совместное применение стратегии предпочтения единичного выражения и стратегии "множества поддержки" позволяет получить более эффективную полную стратегию.

Стратегия единичного разрешения - это близкая стратегия, требующая, чтобы одна из резольвент всегда представляла собой единичное выражение. Это более строгое требование, чем требования, выдвигаемые стратегией предпочтения единичного выражения. Можно показать, что стратегия единичного разрешения не является полной. Для этого можно использовать тот же пример, что и для демонстрации неполноты стратегии линейной входной формы.

Глава 12. Автоматические рассуждения 541

Стратегия линейной входной формы

Стратегия линейной входной формы предполагает прямое использование отрицания цели и исходных аксиом. Она сводится к получению нового дизъюнктивного выражения за счет резолюции отрицания цели с одной из аксиом. Полученный результат разрешается с одной из аксиом для создания нового выражения, которое в свою очередь разрешается с одной из аксиом. Этот процесс продолжается до получения пустого дизъюнкта.

На каждом этапе резолюция выполняется для вновь полученного выражения и аксиомы, сформулированной для исходного утверждения задачи. Ранее полученные выражения никогда не используются для резолюции, как и не используются две аксиомы вместе. Стратегия линейной входной формы не является полной, в чем несложно убедиться на примере следующего набора из четырех дизъюнктивных выражений (который, очевидно, является невыполнимым). Независимо от того, какое из дизъюнктивных выражений выбрано в качестве отрицания цели, стратегия линейного входа не приводит к противоречию.

¬a v ¬b

a v ¬b

¬a v b

a v b

Другие стратегии и методы упрощения

Автор не ставил перед собой задачу исчерпывающего анализа всех стратегий или большинства сложных приемов доказательства теорем на основе логического вывода и принципа резолюции. Они описаны в других источниках, в частности в работах [Wos, 1984] и [Wos, 1988]. Наша задача- познакомить читателя с основными средствами, разработанными для этой области исследований, и показать, как их можно использовать для решения задач. Процедура резолюции - это один из приемов, применяемых в слабых методах решения задач.

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

Используемые в этой главе примеры тривиально малы и содержат все необходимые для решения задачи дизъюнкты (и не только необходимые). Такая ситуация в реальных задачах встречается довольно редко. Выше было рассмотрено несколько простых стратегий борьбы с этой комбинаторной сложностью. В завершение этого подраздела приведем несколько важных соображений, относящихся к разработке систем решения задач на основе резолюции. В разделе 12.3 будет показано, как с помощью системы опровержения разрешения при комбинировании стратегий поиска можно обеспечить "семантику" для логического программирования (logic programming), в частности, для разработки интерпретаторов для языка PROLOG.

При управлении поиском очень полезно комбинировать стратегии, например, стратегию "множества поддержки" со стратегией предпочтения единичного выражения. Эвристики поиска можно также встраивать в правила вывода (сортируя литералы слева направо). Такое упорядочение наиболее эффективно для усечения пространства поиска. Подобное неявное использование стратегий играет важную роль в программировании на языке PROLOG (раздел 12.3).

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

542 Часть V. Дополнительные вопросы решения задач искусственного интеллекта

решений, поскольку это дает большую свободу их использования при резолюции. Так, резолюцию дизъюнктивных выражений, требующую специализации за счет связывания переменных, например{john/Х}, необходимо отложить на максимально позднее время. С другой стороны, если решение требует связывания конкретных переменных, как при выяснении, инфицирован ли Джон стафилококком, подстановки [john/Person] и [staph/lnfectlon] позволяют ограничить пространство поиска и повысить вероятность и скорость нахождения решения.

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

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

Еще одним типом выражений, не несущих новой информации, являются так называемые категоризированные (subsumed) выражения - частный случай уже существующего более общего выражения. Например, выражение p(john) не информативно в пространстве, где уже существует выражение VX(p(X)). В этом случае p(john) можно опустить без потери общности. Это даже полезно, поскольку количество выражений в пространстве уменьшается. Аналогично выражение р(Х) относится к категории p(X) v q(X). Частная информация ничего не добавляет к уже существующей общей.

И, наконец, включение процедур (procedural attachment) позволяет без дальнейшего поиска оценить или обработать любое выражение, которое может дать новую информацию. Оно основано на принципах арифметики и состоит в сравнении атомов или выражений либо "запуске" любой другой детерминистской процедуры, добавляющей в процессе решения задачи конкретную информацию или ограничения. Например, можно использовать процедуру для вычисления связывания переменной при наличии для этого достаточной информации. Такое связывание переменной ограничивает возможные варианты резолюции и приводит к усечению пространства поиска.

Теперь рассмотрим, как в процессе опровержения можно извлекать ответы.

12.2.5. Извлечение ответов в процессе опровержения

Примеры, для которых гипотеза истинна, представляют собой подстановки для поиска опровержения. Следовательно, сохраняя информацию о подстановках унификации, сделанных при опровержении разрешения, можно получить данные для корректного ответа. В этом подразделе будут рассмотрены три таких примера и метод "учета" для извлечения ответов из опровержения разрешения.

Метод записи ответов очень прост. Берется исходное подлежащее доказательству заключение и к нему добавляется каждая подстановка унификации, сделанная в процессе резолюции. Таким образом, исходное заключение становится "учетчиком" всех сделанных в процессе резолюции подстановок унификации. При компьютерной реализации это может потребовать увеличения числа указателей, если при поиске опровержения существует несколько вариантов выбора. Для получения альтернативного пути решения пона-

Глава 12. Автоматические рассуждения 543

добится механизм управления, например возврата. Однако при аккуратной реализации эту дополнительную информацию можно сохранить.

Рассмотрим несколько примеров. На рис. 12.5, иллюстрирующем доказательство существования человека, живущего интересной жизнью, использованы подстановки унификации, представленные на рис. 12.9. Если сохранить исходную цель и применить к этому выражению все подстановки опровержения, мы получим ответ на вопрос, кто этот человек, живущий интересной жизнью.

На рис. 12.9 показано, что с помощью опровержения разрешения можно не только доказать, что утверждение "никто не живет интересной жизнью" ложно, но и определить, что "счастливым" человеком является Джон. Это общий результат, в котором подстановки унификации, приводящие к опровержению, совпадают с выражениями, позволяющими получить значения, при которых исходное требование является истинным.

Рассмотрим еще один пример, связанный с простой историей.

Собака Фидо идет туда, куда идет ее хозяин Джон. Джон - в библиотеке. Где Фидо?

Сначала представим эту историю в виде выражений исчисления предикатов и сведем их к дизъюнктивной форме. Предикаты имеют вид

at(john, X)®at(fido, X), at(john, library).

Дизъюнктивные выражения

¬at(john, Y) v at(fido, Y), at(john, library).

Отрицание заключения имеет вид -¬at(fido, Z).

Это означает, что Фидо - нигде.

На рис. 12.10 показан процесс извлечения ответа. Литерал, отслеживающий подстановки унификации, - это исходный запрос "Где Фидо?"

at(fido,Z).

Еще раз подчеркнем, что подстановка унификации, приводящая к противоречию, содержит информацию об условиях выполнения исходного запроса: "Фидо в библиотеке".

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

У каждого человека есть родитель. Родитель родителя - это дедушка. Требуется доказать, что у конкретного человека Джона есть родитель.

Следующие предложения описывают факты и взаимоотношения этой ситуации. Во-первых, "У каждого человека есть родитель":

("X)($ Y)p(X, Y). "Родитель родителя - это дедушка":

($X)($Y)("Z)p(X, Y) ? (Y, Z)® gp(X, Z)

544 Часть V. Дополнительные вопросы решения задач искусственного интеллекта