7.8. БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕЧАНИЯ

Системы, отвечающие на вопросы

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

Первая универсальная система, отвечающая на вопросы, была предложена Рафаэлем (1964а, 19646). Рафаэль сосредоточил внимание на механизмах ассоциации и дедукции и в большой степени пренебрег вопросом перевода с естественного языка. С другой стороны, Бобров (1964а, 19646) построил систему для решения простых алгебраических задач, сформулированных на английском языке. Его система могла переводить задачи с английского языка на язык соответствующих уравнений, которые предстояло решить. Другая универсальная система, отвечающая на вопросы, названная DEDUCOM (не обладающая способностью перевода с английского языка на язык логики), предложена Слейджлом (1965). Грин и Рафаэль (1968) разработали систему, отвечающую на вопросы, в которой применялись логика первого порядка и метод резольвенции. Коулс (1968) написал программу перевода с английского языка на формально-логический язык: эта программа служила дополнением к системе Грина и Рафаэля.

Два хороших обзора работ в области систем, отвечающих на вопросы, сформулированных на естественном языке, написаны Симмонсом (1965, 1970). Бар Хиллел (1969) выделил некоторые трудности, присущие обработке естественных языков, и пришел к выводу о том, что они могут оказаться непреодолимыми.

Процессы извлечения ответа

Хотя вопрос о вычислении частных случаев переменных, относящихся к кванторам существования, подвергался рассмотрению в классической теории доказательства, Грин (1969а) первым указал процедуру для систем, основанных на резольвенции. Рассмотренный в настоящей главе метод извлечения ответа обобщает подход Грина и основан на статье Лакхэма и Нильсона (1971).

Наш пример автоматического написания программы, иллюстрирующий приложения процесса извлечения ответа, представляет собой модификацию примера Грина (19696, приложение С). Вопрос написания программы для вычислительной машины связан с вопросом доказательства правильности программ. По этому последнему вопросу имеется значительное число работ, в том числе работы Маккарти (1962), Флойда (19676) и Манна (1969). Лондон (1970) дает хороший обзор работ по доказательству правильности программ. Несколько отличная (но также основанная на резольвенции) процедура автоматического написания программ описана Уолдингером и Ли (1969). Блестящую и доступную статью о связи между процедурами доказательства и автоматическим написанием программ опубликовали Манна и Уолдингер (1971).

Применения исчисления предикатов к решению задач в пространстве состояний

Идея использования множеств п. п. формул для описания состояний в решателе задач, основанном на введении пространств состояний, разрабатывается в Станфордском исследовательском институте. Процесс, описанный в разд. 7.6 и относящийся к задаче об обезьяне и бананах, выявился в ходе бесед между Ричардом Файксом, Бертрамом Рафаэлем, Джоном Мансоном и автором.

Мы уже отмечали, что техника решения задач в пространстве состояний с помощью формальных методов возникла в основном из заметок Маккарти (1958, 1963) о системе, «дающей советы». Работа по реализации такой системы была предпринята Блэком (1964). Корделл Грин первым разработал систему формального решения задач, опирающуюся на пространство состояний и использующую полную систему вывода (резольвенции) для логики первого порядка. Большая часть его исследований изложена в его диссертации (Грин, 19696) и двух статьях (Грин, 1969а, 1969в). В системе Грина в каждом из предикатов используется «терм состояния», который рассматривался нами в разд. 7.7.

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

Математическое доказательство теорем

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

Задачи

(см. скан)

(см. скан)