12.6. Эвристики

12.6.0. Простые эвристики

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

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

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

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

12.6.1. Аналогии

При решении задач путем аналогии замечается соответствие между задачей А и ранее решенной задачей В, и с помощью этого соответствия определяется путь решения задачи А. Однако каждому школьнику известно, что существование аналогии еще не означает, что решение задачи В „похоже" на решение задачи А, но если можно показать, что предложенное решение верно, то не важно, как оно возникло. Практическое применение математиками аналогии довольно полно исследовал Пойа (1954). Есть ли возможность приспособить этот мощный метод к механическому решению задач?

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

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

работающую на принципе резолюции, цель которой — показать, что определенные утверждения следуют из очень большой базы данных Прямой способ доказательства состоит в том, чтобы определить Т как отрицание доказываемого утверждения и затем, получив пустое предложение убедиться, что множество невыполнимо. Во многих интересных случаях (например, в диалоговых дедуктивных системах) база данных будет очень большой и в ней будет такое неизвестное подмножество что окажется невыполнимым. Может случиться так, что хотя задача опровержения осуществима, попытки опровергнуть непосредственно приведут к необходимости рассматривать много „непродуктивных" выводов, которые не окончатся пустыми предложениями но отнимут время. Поэтому желательно было бы знать какой-нибудь способ обнаружения нужного подмножества прежде чем начинать резолюцию. Предположим, что у нас есть решенная ранее задача Т. Иными словами, устройство доказательства теорем „знает", что существует такое подмножество множества что невыполнимо и известен вывод из пустого предложения Можно ли установить отображение предложений, участвовавших в опровержении Т, в предложения из при котором невыполнимо? Если ответ на этот вопрос утвердительный, значит, существует способ обнаружить прежде, чем проводить резолюции для опровержения Т по аналогии с опровержением Т. В этом смысле программу ZORBA можно считать устройством рассуждений по аналогии. Для изложения принципов работы программы ZORBA понадобятся два новых понятия.

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

Семантический шаблон атомного высказывания — это просто высказывание, в котором имена предиката и его аргументов

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

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

Теперь мы готовы приступить к обсуждению нашего примера. В табл. 12.5 приведены предложения базы данных и отрицания доказываемых утверждений. Задача состоит в том, чтобы доказать, что не предварительно ответив на вопрос: Для ответа на последний вопрос было взято отрицание нет нигде" в табл. 12.5), и оно было опровергнуто:

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

Первый шаг — найти отображение задачи Т в Т. Используя определенные выше семантические шаблоны, образуем множества

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

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

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

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

Теперь найдем образы предложений. В опровержении (124) участвуют предложения

Отображение можно применить к атомам только одного из них, а именно С. Это дает образ

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

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

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

Отображение можно применить ко всем остальным предложениям, участвовавшим в опровержении (124), и это позволяет получить новые образы:

Таблица 12.6

Затем в базе данных разыскивают предложения, описания которых пересекаются с описаниями их образов, и отбирают подходящие аналоги (табл. 12.6).

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

Ясно, что не является наименьшим невыполнимым множеством, так что, хотя применение аналогии сделало опровержение более эффективным, все же максимум эффекта не достигнут. Так обычно и бывает.

Клинг (1971) использовал программу ZORBA для предварительного выбора предложений из большой базы данных, предназначенной для доказательства некоторых теорем современной алгебры. Он сообщает о весьма эффективном выборе данных, так как в большинстве случаев множество содержало только одно или два ненужных предложения. Нет возможности оценить, насколько хороша „вообще" такая конкретная реализация рассуждений по аналогии, поскольку не ясно, как определить множество задач, которое хотелось бы считать достаточно общим. В самом деле, мы не можем сказать, насколько полезны аналогии в наших рассуждениях, даже как-то введя количественную меру их „полезности". Ясно, что иногда метод аналогий работает хорошо; вместе с тем можно было бы построить бесспорные примеры неэффективного применения аналогий. Похоже, здесь есть два слабых места. Во-первых, пара задач, образующих аналогию, должна быть представлена программе пользователем (человеком). Точности ради отметим, что Клинг дал метод уточнения аналогии после того, как она предложена. Способности, возможно, как раз и заключаются в умении обнаруживать аналогии при решении задач. Вторую слабость можно считать более технической. В разобранном выше примере было только одно отображение и потому только одна аналогия. В общем случае может быть очень много отображений и аналогий. Методы работы с аналогиями разработаны и изучены недостаточно, чтобы можно было сказать что-нибудь существенное о правилах, ограничивающих поиск лишь полезными аналогиями. Не похоже, что такие вопросы будут поддаваться логическому анализу. Как и при сравнении различных эвристических методов и методов очищения, по-видимому, нужна информация, извлеченная из тщательно построенных экспериментов в области решения задач.