Intel_Nils (526801), страница 46
Текст из файла (страница 46)
(Эта упрощенная форма больше всего подходит для решения иллюстративных задач. Читателю предлагается поработать также с четырехоператорным вариантом задачи, который рассматривался в предыдущем разделе.) Действие этих операторов можно описать следующими п. п. формулами: 1. (чх)гз)( ОЬ)ВОХ =1» АТ(ящик, х, передвинуть (х,з))), т. е. «для всех х и з, если обезьяна не находится на ящике в состоянии з, то в состоянии, возникающем в результате 230 Гх 7.
Применения исчисления аредикатое к ресиенаю еадач применения оператора «передвинуть (х)». к состоянию з, ящик будет расположен в точке х. 2. ( чз)(ОМВОХ (взобратьси (з))), т. е. для всех з в состоянии, возникающем в результате применения оператора «взобраться» к состоянию з, обезьяна находится на ящике. 3. (ч'з)[ОНВОХ(з) Л АТ (ящик, с, з)='>НВ (схватить (з))), т, е. для всех з, если обезьяна находится на ящике, а яшик расположен в точке с в состоянии з, то в состоянии, возникающем в результате применения оператора «схватить» к состоянию з, обезьяна будет иметь бананы. В дополнение к этим аксиомам нужно выразить явно другие результаты действия этих трех операторов, например «положение ящика не изменяется, когда обезьяна на него взбирается» илн «в конце этапа перемещения ящика обезьяна еше не будет находиться на яшике».
Поскольку в нашем доказательстве потребуется только первый результат, запишем его формально: 4, (чзскУз) (АТ (ящик, х, д) =)мАТ (ящик, х, взобраться (г)9. Нам понадобится также адекватное описание начального состояния Яе.' 5. ОМВОХ (зо). Теперь поставить вопрос перед нашим формальным решателем задач — это просто сформулировать предположение (Лз) НВ (з).
Далее надо преобразовать приведенные выше аксиомы и отрицание предположения в форму предложений и получить дерево опровержения, изображенное на рис. 7.!2. Ответным утверждением, извлеченным обычным образом из этого дерева, будет утверждение НВ (схватить (взобраться (передвинуть (с, зм)))). Отсюда видно, что искомое состояние достигается с помощью последовательности операторов (передвинуть (с), взобраться, схватить).
Интересно сопоставить этот формальный подход к решению задачи с методом пространства состояний (использующим исчисление предикатов для проверки выполнения условий достижения цели и применимости операторов), рассмотренным в предыдущем разделе. Формальный подход дает то преимушество, что для выполнения операторных вычислений не требуется никакого специального механизма. Вычисления выполняются автоматически с помощью механизма дедукции, воплошенного в доказателе теорем.
Таким образом, не требуется никаких специальных методов перебора в пространстве состояний (или перебора при сведении задачи к подзадачам), кроме тех, которые 7.7. Одна 4ормализаяия для решении задач Ж( используются прн поиске доказательств (их мы будем рассматриватье в следующей главе). Но эта высокая степень единообразна может оказаться также и недостатком формального метода.
В формальную процедуру перебора доказателя теорем нелегко включить специальные эвристики, полезные для упорядочения процесса применения операторов при переборах в пространстве состояний. иа(з) 3) м и в(ахятяяяь(зд ОЛВОХ(з) 'ч' АТ(ящик.щи) О)(ВОЛ(езедратаея(з)) «А Т (яиряс а, язяаразяьея (з]) (ящик, к, амдрятзая(з)) АТ(ящик. с, з) , к,язредяикзят(к,з)) ОУВОХ(з) яй Р к с. 7Л2. Доказательство для задачи об обезьяне я бананах. Другой недостаток формальной процедуры — необходимость явного описания с помощью специальных аксиом тех отношений, которые не изменяются под воздействием операторов.
Так, в нашем примере пришлось сформулировать и использовать тот факт, что положение ящика не изменяется при действии оператора «взобраться». Доказательство того, что определенные отношения в дочерних состояниях по-прежнему удовлетворяются, утомительно и значительно увеличивает затраты усилий при поиске полного доказательства. Проблема, связанная с тем, что на одни отношения операторы воздействуют„ а на другие нет, иногда называется проблемой системы отсчета.
В наших 232 Гл. 7. Применения исчисления 'предичагав и решению задач правилах добавлений — изъятий отражается та точка зрения, что легче назвать формулы, подвергающиеся изменению, и предположить, что все другие остаются неизменными. Слабость формального подхода, изложенного в этом разделе, состоит в том, что такого рода предварительное условие в нем не используется, и поэтому, если нам нужен факт, что некоторое отношение после применения оператора по-прежнему удовлетворяется, то мы должны этот факт явно доказать.
Т.в. БиБлиОГРАФические и истОРические ВАмечАния Системы, отвечающие на вопросы Процесс извлечения из опровержений ответных утверждений позволяет применить формальные методы к задачам получения ответа на вопросы. Вообще говоря, система, отвечающая на вопросы, основана на весьма сложных способах извлечения информации, в которых при ответе на вопросы следует производить логические дедукции, исходя из различных фактов, хранящихся в массиве данных. При создании систем, отвечающих на вопросы, возникает также проблема осуществления перевода с естественного языка, например английского, на формальный язык, такой, как исчисление предикатов, используемый дедуктивной системой.
Первая универсальная система, отвечающая на вопросы„ была предложена Рафаэлем (1964а, 19646). Рафаэль сосредоточил внимание на механизмах ассоциации и дедукции и в большой степени пренебрег вопросом перевода с естественного языка. С другой стороны, Бобров (1964а, 1964б) построил систему для решения простых алгебраических задач, сформулированных на английском языке. Его система могла переводить задачи с английского языка на язык соответствующих уравнений, которые предстояло решить. Другая универсальная система, отвечающая на вопросы, названная РЕИЗСОМ (не обладающая способностью перевода с английского языка на язык логики), предложена Слейджлом (1965). Грин и Рафаэль (1968) разработали систему, отвечающую на вопросы, в которой применялись логика первого порядка н метод резольвенции.
Коулс (1968) написал программу перевода с английского языка на формально-логический язык: эта программа служила дополнением к системе Грина и Рафаэля. Два хороших обзора работ в области систем, отвечающих на вопросы, сформулированных на естественном языке, написаны Симмонсом (1965, 1970).
Бар Хиллел (1969) выделил некоторые трудности, присущие обработке естественных языков, и пришел к выводу о том, что они могут оказаться непреодолимымн. 7.В. Библиограф««ес«ие и и«гори«ес«и« замечания жз Процессы извлечения ответа Хотя вопрос о вычислении частных случаев переменных, относящихся к кванторам существования, подвергался рассмотрению в классической теории доказательства, Грин (1969а) первым указал процедуру для систем, основанных на резольвенцни.
Рассмотренный в настояшей главе метод извлечения ответа обобщает подход Грина и основан на статье Лакхзма н Нильсона (1971). Наш пример автоматического написания программы, иллюстрирующий приложения процесса извлечения ответа, представляет собой модификацию примера Грина (1969б, приложение С). Вопрос написания программы для вычислительной машингя связан с вопросом доказательства правильности программ. По этому последнему вопросу имеется значительное число работ, в том числе работы Маккарти (1962), Флойда (19676) и Манна (1969). Лондон (!970) дает хороший обзор работ по доказательству правильности программ.
Несколько отличная (но также основанная на реэольвенции) процедура автоматического написания программ описана Уолдингером и Ли (1969). Блестящую и доступную статью о связи между процедурами доказательства и автоматическим написанием программ опубликовали Манна и Уолдингер (1971). Применения исчисления предикатов к решению задач в пространстве состояний Идея использования множеств п. п. формул для описания состояний в решателе задач, основанном на введении пространств состояний, разрабатывается в Станфордском исследовательском институте.
Процесс, описанный в равд. 7.6 и относящийся к задаче об обезьяне и бананах„ выявился в ходе бесед между Ричардом Файксом, Бертрамом Рафаэлем, Джоном Мансоном и автором. Мы уже отмечали, что техника решения задач в пространстве состояний с помощью формальных методов возникла в основном из заметок Маккарти (1958, 1963) о системе, «дающей советы», Работа по реализации такой системы была предпринята Блэком (1964). Корделл Грин первым разработал систему формального решения задач, опираюшуюся на пространство состояний и использующую полную систему вывода (резольвенцни) для логики первого порядка. Большая часть его исследований изложена в его диссертации (Грин, 19696) и двух статьях (Грин, 1969а, 1969в).
В системе Грина в каждом из предикатов. используется «терм состояния», который рассматривался нами в равд. 7.7. '2З4 Гл. 7. Применения исчисления предикатов к решению задач Дж. Маккарти продолжил свои исследования, касающнеся требований, предъявляемых к универсальной формальной снстеме решения задач. Особенно он настаивал на необходнмостн включения,элементов логики более высокого (по сравнению с первым) порядка для формализации таких понятий, как ситуации, будущие операторы, действия, стратегии, результаты прнменення стратегий н знание. Этн идеи прекрасно изложены в статье Маккартн н Хзйеса (!969).
Многие вопросы, подннмае.мые Маккарти н Хзйесом, выходят за рамки вопросов, рассматрнваемых в вводном курсе. Математнческое доказательство теорем Одна нз наиболее очевидных областей применения автоматнческнх устройств для доказательства теорем (правда, не рассмотренная в настоящей главе) — доказательство математнче.скнх теорем. Этим занимались Робинсон н Вос (1969)'„а также Гард н др.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
