14.2.4. Контекстно-ориентированное доказательство теорем

Мы неоднократно обращали внимание на то, что главный недостаток резолюции — быстро возрастающее, до астрономических чисел, количество порождаемых предложений. В ответах на вопросы это становится очень серьезной трудностью, потому что число предложений в исходной базе данных велико. Фактически примеры Грина были возможны только благодаря тому, что требуемые выводы оказались очень короткими. Один из способов не дать дедуктивным программам тратить время на ненужные для доказательства предложения — это ограничить резолюцию предложениями, „имеющими отношение» к доказательству или похожими на них. Рассмотрим классическую дедукцию:

Все люди могут ошибаться. Сократ человек. Поэтому

Сократ может ошибаться.

Условия выражаются предложениями

и вопрос

принимает форму

Необходимые выводы таковы:

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

Решение Грина состояло в том, чтобы позволить человеку, контролирующему процесс, выделить кандидатов на участие в резолюции. Хотя это, быть может, очень практично, здесь нет никакого достижения в смысле искусственного интеллекта. Другой подход, который мы называем контекстно-ориентированным доказательством теорем, принадлежит Винограду (1972). Он развивает более ранние работы Хьюитта (1969, 1970). Этот метод мы уже исследовали как механизм планирования (гл. 11); теперь обсудим его приложения в вопросно-ответной системе.

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

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

Обладает ли клиент привилегированным налоговым статусом?

В качестве догадки можно попытаться ответить на вопрос

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

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

DEDUCOM также дает пример программы, позволяющей пользователю выбирать стратегию поиска. Принципиальные различия между проектами Винограда и Слейгла (более ранним) в том, что PLANNER как язык гораздо удобнее для заданий, чем Лисп. Возможно, главный результат работы Винограда в том, что он смог продемонстрировать метод перевода с английского языка в программы PLANNER. Об этом пойдет речь в гл. 15. К тому же Лисп оказался с этой точки зрения плохим языком. Это важно потому, что если мы собираемся опираться на контекстно-ориентированные стратегии, пользователь должен иметь возможность формулировать их на языке, естественном для него. Программы „понимания» будут не слишком перспективными, если их пользователям надо будет сначала стать специалистами в языках PLANNER, Лисп, или в любом из множества других языков программирования для искусственного интеллекта.