Часть 2.

Требуется найти значение W, при котором gp(john, W) или $(W)(gp(john, И/)). Отрицанием цели является предложение ¬$(W)(gp(john, W)) или

¬gp(john, W).

В процессе приведения указанных выше предикатов к дизъюнктивной форме для опровержения разрешения квантор существования в первом предикате "У каждого человека есть родитель" требует построения сколемовской функции. В данном случае она строится достаточно просто: нужно взять конкретное значение X и найти для него родителя. Функцию нахождения предка для X назовем ра(Х). Для Джона это будет его отец или мать. Для данной задачи дизъюнктивная форма предикатов будет иметь вид:

р(Х, ра(Х)),

¬p(W, Y)v¬P(Y, Z) v gp(W, Z),

¬gp(john, V).

Процессы опровержения разрешения и извлечения ответов для этой задачи представлены на рис. 12.11. Отметим, что подстановки унификации при извлечении ответа имеют вид

gp(john, pa(pa(john))).

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

Описанный выше общий процесс извлечения ответа может использоваться в любых процедурах опровержения, где применяются подстановки унификации, показанные на рис. 12.9 и 12.10, или сколемовские функции, показанные на рис. 12.11. Этот процесс позволяет находить ответы. Метод действительно очень прост: экземпляры (подстановки унификации), приводящие к противоречию, в то же время обеспечивают истинность отрицания заключения (исходного запроса). Хотя в этом подразделе не доказывается применимость метода для любой задачи, работоспособность этого процесса проиллюстрирована на нескольких примерах. Более подробное описание процесса извлечения ответов можно найти в [Nilsson, 1980] и [Wos и др., 1984].

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

12.3. Язык PROLOG и автоматические рассуждения

12.3.1. Введение

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

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

a v ¬b v c v ¬d,

где а, b, с, d - литералы. В процессе резолюции можно использовать стратегию поиска для получения пустого дизъюнкта. Стратегию можно применять ко всем литералам, и выбор конкретного литерала зависит от выбора самой стратегии. Используемые для резолюции стратегии являются слабыми эвристиками. Они не подразумевают глубоких знаний о конкретной предметной области задачи.

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

а?b ? ¬c ? d.

Это выражение можно интерпретировать так: "Проверить, истинно ли выражение а, а также b и d, и ложно ли выражение с". Это правило служит для решения а и предоставляет

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

соответствующую эвристическую информацию. На самом деле проще всего обеспечить ложное значение общего предиката с помощью подцели to, поскольку наименее ресурсоемким по времени является следующий порядок выполнения операций: "Проверить значение to, посмотреть, ложно ли с, а затем проверить d". Существует неявная эвристика: сначала нужно проверить простейший способ получения ложного значения, а если он не сработает, перейти к остальной (возможно, более сложной) части решения. Эксперты могут разработать процедуры и взаимоотношения, которые не только сами являются истинными, но и содержат информацию о том, как воспользоваться этой истиной. При решении большинства интересных задач эти эвристики не стоит игнорировать [Kowalski, 19796].

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

12.3.2. Логическое программирование и язык PROLOG

Чтобы понять математические основы языка PROLOG, введем определение логического программирования (logic programming). Затем добавим к нему точную стратегию поиска для получения аппроксимации этой стратегии поиска, которую иногда называют процедурной семантикой (procedural semantics) языка PROLOG. Для полноты описания языка PROLOG будет рассмотрено использование оператора not и предположения о замкнутости мира (closed world assumption).

Рассмотрим базу данных дизъюнктивных выражений, подготовленную для опровержения разрешения (раздел 12.2). Если ограничить это множество выражениями, содержащими не более одного положительного литерала (а также 0 или более отрицательных литералов), получим пространство дизъюнктов с некоторыми интересными свойствами. Во-первых, задачи, описываемые с помощью этого набора дизъюнктов, сохраняют свойство невыполнимости (unsatisfiability) для опровержения разрешений, т.е. являются полными в смысле опровержения (раздел 12.2). Во-вторых, важным преимуществом ограничения нашего представления этим подклассом всех дизъюнктов является наличие очень эффективной стратегии поиска опровержения, основанной на использовании линейной входной формы, предпочтении единичного выражения и сведении целевого выражения слева направо с помощью поиска в глубину. При эффективной реализации рекурсии (конечных рекурсивных вызовов) эта стратегия гарантирует нахождение опровержения, если пространство дизъюнктов обладает свойством невыполнимости [van Emden и Kowalski, 1976]. Хорновское выражение содержит не более одного положительного литерала, т.е. может быть записано в форме

а v¬b, v ¬b2 v... v ¬bn,

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

а?b1 ? b 2 ?... ? bN.

Прежде чем обсудить стратегию поиска, дадим формальное определение подмножеству хорновских выражений (Horn clause). Это подмножество вместе со стратегией недетерминистского приведения целевого выражения называется логической программой (logic program).

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

ОПРЕДЕЛЕНИЕ

ЛОГИЧЕСКАЯ ПРОГРАММА

Логическая программа - это множество выражений, связанных квантором всеобщности, записанных в форме исчисления предикатов первого порядка вида

Здесь а и Ь, - положительные литералы, которые иногда называют атомарными целями. При этом а - это заголовок выражения, а конъюнкция Ь/ - его тело. Такие предложения называются хорновскими выражениями (Horn clause) теории предикатов первого порядка. Они могут быть записаны в трех формах: когда исходное дизъюнктивное выражение не содержит положительных литералов, когда оно не содержит отрицательных литералов и когда оно содержит один положительный и один или несколько отрицательных литералов. Эти варианты обозначены цифрами 1,2 и 3 соответственно.

?b1 ? b2 ? b3 ? ... ?bn- это так называемое беззаголовочное выражение или проверяемые цели.

a1?

a2?

.

.

an?

называются фактами (fact).

3. а?b1 ?... ? bп называется отношением правила.

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

И, наконец, на основе закона де Моргана эта запись приводится к виду

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

Следует отметить, что порой невозможно преобразовать дизъюнктивные выражения из произвольного пространства к хорновской форме. Некоторые выражения не могут быть записаны в такой форме, например p v q. Для создания хорновского выражения в исходном предложении должно содержаться не более одного положительного литерала. Если этот критерий не выполняется, то может понадобиться пересмотреть исходную предикатную форму описания проблемы. Как будет видно из дальнейшего, преимуществом хорновской формы представления является возможность реализации эффективной стратегии опровержений.

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

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

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

которое используется для приведения целевого выражения путем унификации а1 и а, с помощью подстановки ?. Новое целевое выражение принимает вид

Такой процесс недетерминированного приведения целевого выражения продолжается до тех пор, пока целевое множество не окажется пустым.

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

Согласно абстрактной спецификации логическая программа должна обладать ясной семантикой, свойственной системам опровержения разрешения. В работе [van Emden и Kowalski, 1976] показано, что минимальной интерпретацией, при которой логическая программа истинна, является сама интерпретация этой программы. Поэтому в практических языках программирования, таких как PROLOG, в процессе работы программы можно вычислить только подмножество связанных с ней интерпретаций [Shapiro, 1987].

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

Опишем работу интерпретатора более формально. Пусть имеется цель

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

и программа Р. Интерпретатор PROLOG последовательно выбирает первое дизъюнктивное выражение из Р, заголовок которого унифицирует at. Затем это выражение используется для приведения целей. Если

приводящее выражение для унификации ?, то целевое выражение принимает вид

Затем интерпретатор PROLOG пытается выполнить приведение крайней слева цели b1, используя первое выражение программы Р, унифицирующее Ь\. Предположим,

при подстановке унификации ф. Тогда целевое выражение приводится к виду

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

Если целевое выражение приводится к нулевому предложению (D), то приводящая к этому композиция подстановок унификации

обеспечивает интерпретацию, при которой исходное целевое выражение истинно. Помимо возврата в соответствии с порядком следования выражений в программе, последовательный язык PROLOG допускает использование выражения cut или !. Как описано в подразделе 14.1.5, выражение cut можно поместить в дизъюнктивное выражение в качестве самой цели. Тогда интерпретатор, достигнув этого выражения, фиксирует текущий путь выполнения программы и подмножество подстановок унификации, сделанных после выбора выражения, содержащего cut. При этом само выбранное дизъюнктивное выражение становится единственным средством приведения целевого выражения. Если процесс приведения завершится неудачно после выражения cut, то все дизъюнктивное выражение считается ложным.

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

Подводя итог описанию последовательного языка PROLOG, следует сравнить его с моделью опровержения разрешения из раздела 12.2.

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

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

2.1. Целевые выражения

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

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

2.2. Факты

a1?

a2?

.

.

an? -

это отдельные выражения, используемые для резолюции.

2.3. Хорновские правила или аксиомы

позволяют выполнять приведение для соответствующих подцелей.

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

входной формы (методики предпочтения фактов и использования отрицания цели и

ее дочерних резольвент, описанной в подразделе 12.2.4) и применении принципа

поиска выражений для резолюции в глубину (с возвратом) и слева направо система

доказательства теорем на основе резолюции работает как интерпретатор языка

PROLOG. Поскольку эта стратегия является полной в смысле опровержения, она

гарантирует нахождение решения (т.е. исключает отсечение интерпретаций за счет

использования выражения cut).

И, наконец, композиция подстановок унификации в процессе доказательства обеспечивает интерпретацию (ответ), для которой целевое выражение является истинным. Это точно соответствует процессу извлечения ответа, описанному в подразделе 12.2.5.

Важным свойством современных интерпретаторов языка PROLOG является неявное использование в его реализации предположения о замкнутости пространства (closed world assumption). В теории предикатов доказательство ¬р(Х) эквивалентно доказательству того, что р(Х) логически ложно, т.е. выражение р(Х) ложно для каждой интерпретации, для которой набор аксиом является истинным. Интерпретатор языка PROLOG на основе алгоритма унификации из главы 2 дает более частный результат, чем общий принцип опровержения разрешения, описанный в разделе 12.2. Вместо проверки всех интерпретаций он тестирует только те выражения, которые содержатся в базе данных в явной форме. Сформулируем эти ограничения, чтобы четко увидеть неявную ограниченность языка PROLOG.

Предположим, что для каждого предиката р и каждой переменной X из р множество аь а2, ..., а„ составляет область определения X. Работа интерпретатора PROLOG в процессе унификации основывается на следующих принципах.

Аксиома об уникальности имен. Для всех элементов области определения ai <> ajесли

эти значения не идентичны. Следовательно разноименные элементы различаются.

Аксиома замкнутости мира (closed world).

Это означает, что возможными реализациями отношения являются только те выражения, которые содержатся в описании задачи.

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

3. Аксиома о замыкании области определения (domain closure).

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

Эти три аксиомы неявно реализованы в интерпретаторе языка PROLOG, что подтверждается ограниченностью множества возможных интерпретаций PROLOG.

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

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

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

12.4. Дополнительные вопросы автоматических рассуждений

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

12.4.1. Единое представление для реализации слабых методов решения

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

Формат представления правила "если..., то..." зачастую более информативен для использования правила отделения или реализации поиска в продукционной системе, чем один из подобных синтаксических вариантов. Кроме того, такой формат позволяет эффективно использовать это правило. Допустим, требуется представить абдуктивный вывод (abductive inference) (раздел 8.0) утверждения "если двигатель не заводится и фары не включаются, то, возможно, сел аккумулятор". С помощью этого правила можно проверить аккумулятор.

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

При записи этого правила в дизъюнктивной форме теряется эвристическая информация о способе его применения. Если записать это правило в предикатной форме ¬turn_over ? ¬lights® battery, то его дизъюнктивная форма будет иметь вид turn_over v lights v battery. Это выражение можно записывать по-разному, причем каждая форма записи может представлять отдельную импликацию.

и т.д.

Чтобы сохранить эвристическую информацию в процессе автоматических рассуждений, некоторые исследователи разработали методы рассуждений, предполагающие кодирование эвристик путем формирования правил по аналогии с разработкой отношений человеком-экспертом [Nilsson, 1980], [Bundy, 1988]. Этот подход уже был рассмотрен в разделе 3.3, а его реализация на языке PROLOG описана в разделе 12.3. Экспертные системы на основе правил также позволяют программисту контролировать поиск с помощью структуры правил. Эта идея будет развита в следующих двух примерах, в которых сохраняется форма импликации, и эта информация используется для управления поиском на графе.

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

Факт:

(a v(b ? c)).

Правила (аксиомы):

(а®(d ? e)),

(b ® 0)

(c ® (g v h)).

Цель:

? e v f.

Доказательство утверждения e v f показано на рис. 12.12. Обратите внимание на использование связки И для отношения v и связки ИЛИ для отношения л в пространстве поиска на основе данных. Если известно, что а или b ? с - истинно, то необходимо проводить рассуждения с помощью обоих дизъюнктов, чтобы гарантировать сохранение истинности. Поэтому эти два пути соединяются. С другой стороны, если b не - истинны, то можно продолжать исследовать любой из этих конъюнктов. В процессе проверки соответствия любое промежуточное состояние, например с, заменяется заключением правила, в частности, g v h, предпосылка которого соответствует этому состоянию. Исследование обоих состояний е и 1 на рис. 12.12 приводит к достижению цели e v f .

Аналогичным образом можно использовать проверку соответствия правил на графе И/ИЛИ при рассуждениях на основе цели. Если в описании цели содержится символ v, как в примере на рис. 12.13, то каждую альтернативу можно исследовать независимо. Если целевое выражение представляет собой конъюнкцию, то необходимо обрабатывать оба конъюнкта.

Цель

(a v (b ? c)).

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

Правила (аксиомы):

(f ? d)®a,

(е®(b?с)),

(g ® d).

Факт:

Хотя эти примеры взяты из исчисления высказываний, в теории предикатов поиск выполняется аналогично. После подстановок унификации для литералов можно применять правила вывода и осуществлять поиск по различным ветвям пространства. Естественно, подстановки унификации должны быть согласованными по различным ветвям И пространства поиска.

В этом подразделе предложены методы решения, позволяющие сохранить эвристическую информацию в представлении данных для слабых методов решения задач. Таким образом, в экспертных системах программист может задавать в рамках правила эвристическую информацию. Экспертные системы основаны на описаниях в форме правил, т.е. учитывают для управления поиском порядок правил или порядок следования предпосылок в рамках одного правила. При таком подходе отсутствует возможность применения однородных процедур поиска на полном наборе правил, таких как метод резолюции. Однако правило отделения все же можно использовать, что подтверждается графами, приведенными на рис. 12.12 и 12.13. Продукционные системы, основанные на поиске в глубину, в ширину или "жадном" алгоритме поиска, представляют собой пример архитектуры для реализации систем правил (см. примеры в главах 4, 5, 7, 14 и 15).

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

12.4.2. Альтернативные правила вывода

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

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

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

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

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

Продемонстрируем применение процедуры гиперрезолюции на примере следующего набора дизъюнктивных выражений.

С помощью гиперрезолюции заключение можно получить за один шаг.

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

Заключение этого правила - часть окончательного результата. Заметим, что в процессе отсутствуют промежуточные результаты типа

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

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

Важным и сложным вопросом в разработке механизмов доказательства теорем является контроль равенства. Особенно сложные задачи возникают в областях, где большинство фактов и взаимосвязей имеют несколько представлений, например, могут быть получены путем применения свойств ассоциативности и коммутативности выражений. Такой областью является математика. Вот простой пример. Арифметическое выражение 3+(4+5) может быть представлено во многих различных формах, в том числе 3+((4+0)+5). Такие выражения сложны для использования подстановок, унификации и проверки равенства с другими выражениями в рамках автоматического решения математических задач.

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

и новое выражение

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

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

age{grandfather{sarah), 86).

В данном случае проблема равенства связана с именами понятий. Как предпочтительнее классифицировать человека: как отца отца father(father(X)) или дедушку grandfather(X)? Подобным образом можно указать канонические имена для всех членов семьи, в частности определить, что брат отца brother(father(Y)) - это дядя uncle(Y). Указав канонические имена, под которыми должна храниться информация, можно разработать демодуляторы, в частности equal, приводящие всю новую информацию к выбранной форме. Заметим, что демодуляторы - это всегда единичные выражения.

Парамодуляция - это обобщение подстановки равенства на уровне термов. Например, пусть дано выражение

older(mother(Y), Y) и отношение равенства

equal(mother(sarah), kate).

Тогда можно выполнить парамодуляцию и получить older(kate, sarah).

Заметим, что проверка соответствия и замены {sarah/Y} и {mother(sarah)/kate} выполняется на уровне термов. Основное различие между процедурами демодуляции и парамодуляции состоит в том, что последняя допускает нетривиальную замену переменных в обоих аргументах равенства предикатов. При демодуляции замена выполняется с помощью демодулятора. Для получения окончательного вида выражения можно использовать несколько демодуляторов. Парамодуляция выполняется лишь один раз для любой ситуации.

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

12.4.3. Стратегии поиска и их использование

Иногда предметная область приложения диктует специальные требования к правилам вывода и эвристикам по их использованию. Выше уже рассматривался вопрос использования демодуляторов для реализации равнозначных подстановок. В естественной дедуктивной системе (natural deduction system), описанной в работе [Bledsoe, 1971], использованы две важные стратегии доказательства теорем на основе резолюции, получившие название стратегий расщепления (split) и приведения (reduce).

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

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

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

двух соотношений s ? A и s ? B. Или доказательство истинности некоторого свойства выражения ¬ (A ? B) аналогично доказательству этого свойства для ¬А и для ¬S. Разделяя доказательства больших теорем на фрагменты меньшего объема, можно ограничить пространство поиска. В работе [Bledsoe, 1971] используются также подстановки равенства.

Как неоднократно отмечалось в предыдущих главах, корректное использование стратегий - это, скорее, искусство, требующее хорошего знания области приложения, а также соответствующего представления и правил вывода. В заключение этой главы приведем несколько общих правил, которые при осмысленном использовании могут оказаться очень эффективными, но, как и всякое правило, имеют свои исключения. Эти рекомендации обобщают опыт многих исследователей, работающих в этой области [Bledsoe, 1971], [Nilsson, 1980], [Wos и др., 1984], [Wos, 1988], а также собственные представления автора книги о слабых методах решения задач. Приведем эти рекомендации без дополнительных комментариев.

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

Прежде чем применять общие правила вывода, разбивайте задачу на подзадачи.

По возможности используйте предикаты равенства.

Применяйте демодуляторы для создания канонических форм.

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

Реализуйте стратегии, сохраняющие "полноту".

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

В процесс резолюции старайтесь использовать единичные выражения.

Выполняйте категоризацию новых выражений.

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

задач из данной области.

12.5. Резюме и дополнительная литература

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

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

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

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

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

Любознательному читателю можно порекомендовать ознакомиться с соответствующей литературой. В частности, работа [Chang и Lee, 1973] - это очень доступная книга, рассчитанная на неподготовленного читателя. Формальные основы описанного подхода изложены в [Loveland, 1978]. Множество ранних классических работ в этой области собраны в [Siekmann и Wrightson, 1983a, 19836]. Важные результаты в области автоматических рассуждений изложены в работах [Nilsson, 1980], [Genesereth и Nilsson, 1987], [Kowalski, 19796], [Lloyd, 1984], [Wos и др., 1984, 1988], [Robinson, 1965], [Bledsoe, 1977]. Важный вклад в методику доказательства теорем внесла работа [Воуег и Moore, 1979]. К ранним работам в этой области относятся [Feigenbaum и Feldman, 1963] и [Newell и Simon, 1972].

В течение последних двадцати пяти лет все новые результаты в области автоматических рассуждений докладывались на конференции CADE (Conference on Automated Deduction). В настоящее время много работ посвящены проверке соответствия моделей, разработке систем верификации и представления иерархических знаний [McAllester, 1999], [Ganzinger и др., 1999]. Продолжают свои исследования Ларри Вое (Larry Wos) и его коллеги из Аргонской национальной лаборатории. В частности, работа [Veroff, 1997] по теории автоматических рассуждений посвящена Восу. Стоит отметить также работы [Bundy, 1983, 1988], выполненные в Эдинбургском университете, а также [Kaufmann и др., 2000], выполненную в университете штата Техас.