4.7. ПРИМЕРЫ СВЕДЕНИЯ, ЗАДАЧИ К СОВОКУПНОСТИ ПОДЗАДАЧ

Задача символического интегрирования

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

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

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

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

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

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

Это правило служит оправданием следующего сведения задачи к подзадачам:

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

Остальные операторы просто осуществляют подстановку одного интегрального выражения в другое и, таким образом, порождают «ИЛИ» вершины. Эти операторы основаны на следующих процессах:

Алгебраические подстановки

Пример

Тригонометрические подстановки

Пример

Деление числителя на знаменатель

Пример

Дополнение до полного квадрата

Пример

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

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

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

Пример решения. На рис. 4.9 показан «И/ИЛИ» граф перебора, образованный в результате процесса, подобного

рассмотренному выше. Задача состоит в интегрировании выражения

Вершины графа — это описания задач, и в каждой из них указан интеграл.

Рис. 4.9. (см. скан) «И/ИЛИ» граф перебора для задачи интегрирования.

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

основании этого решающего графа и табличных интегралов устанавливаем, что

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

Доказательство теорем в планиметрии

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

Требуется доказать:

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

Рис. 4.10. Чертеж к рассматри ваемому примеру геометрической теоремы.

Мы будем представлять такого типа задачи в виде выражения, имеющего форму где — то утверждение, которое предстоит доказать, множество посылок. Тогда наш пример описывается следующим выражением:

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

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

(см. скан)

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

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

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

члены указанного множества соответствуют истинным утверждениям.

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

Для того чтобы эта задача нам пригодилась, нужно положить

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

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

Продолжая аналогичным образом этот процесс, мы приходим к решающему графу типа «И/ИЛИ», изображенному на рис. 4.11. Из-за ограниченности запаса элементарных задач (хорошо соответствующих нашему примеру, но недостаточных в общем случае) в этом процессе не возникает никаких лишних множеств вершин типа «И». Читатель мог бы посмотреть, к чему привело бы добавление еще нескольких элементарных задач, таких, как

Важным средством контроля числа порождаемых вершин в «И/ИЛИ» графах служит использование моделей. Под моделью мы здесь понимаем некоторую конкретную интерпретацию общего логического утверждения. Утверждения, которые нам предстоит доказать, часто представляют собой общие утверждения, охватывающие большое число частных случаев. Любой из этих частных случаев мог бы использоваться в качестве модели общего утверждения. Если это общее утверждение в действительности можно доказать, то тем более любой частный случай, очевидно, будет истинным в соответствующей модели.

В качестве примера рассмотрим только что доказанную теорему:

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

Рис. 4.11. «И/ИЛИ» решающий граф для рассматриваемого доказательства теоремы.

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

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

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

Проиллюстрируем использование модели для задачи

Мы предполагаем, что программа доказательства теорем имеет доступ к чертежу на рис. 4.12. Эту задачу следовало бы решать прямым путем посредством введения посылки и формулировки подзадачи доказательства этой посылки.

Рис. 4.12. Чертеж для геометрической задачи. Дано: Доказать:

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

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

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

Рис. 4.13. Пример, требующий построения вспомогательного отрезка. Дано: Доказать:

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

Обычно эти осложнения удается предусмотреть и в результате получить значительное возрастание эффективности поиска решения при использовании чертежа. Гелернтер и др. (1960) показали, что использование чертежа в программе - доказательства геометрических теорем уменьшает в среднем число дочерних вершин с 1000 до 5 на одну родительскую вершину.

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

Устройство доказательства теорем может обращаться к чертежу на рис. 4.13.

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

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

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