Intel_Nils (526801), страница 41

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 41)

формула В" из некоторого множества 5 п. п. формул. Если Ф' не следует из 5, то, возможно, мы захотим знать, следует ли - Ф' из 5. Конечно, в силу неразрешимости исчисления предикатов не всегда можно установить, следует ли Ф' (или Ф') нз 5. Можно попытаться поискать ответ на каждый из этих вопросов, и, если после затраты некоторых усилий ответ не будет найден или время будет исчерпано, можно лишь заключить, что на вопрос, следует ли )Р (илн. )Р) из 5, нельзя дать ответ (с учетом наших возможностей). Часто, конечно, Одно из доказательств будет найдено, и вопрос окажезся решенным.

В других приложениях нужно знать значение элемента х (если он существует), при котором данная правильно построенная формула %' (содержащая х в качестве переменной) логически следует из некоторого множества 5 п. п. формул. Иными словами, мы хотели бы знать, следует ли логически п. п. формула ((х) Ф'(х), и если да, то каков тот частный случай переменной х, «который существует».

Проблема поиска доказательства п. п. формулы (3х) )Р(х), исходя из 5, является обычной проблемой доказательства в исчислении предикатов, 'но для построения удовлетворяющего частного случая требуется, чтобы метод доказательства был «конструктивным». Заметим, что умение строить удовлетворяющие частные случаи для переменной, относящейся к квантору существования, позволяет ставить вопросы весьма общего свойства. Например, мы могли бы задаться вопросом: «Существует ли решающая последовательность для некоторого случая игры в пятнадцать?» Если можно найти конструктивное доказательство того, что решение существует, то можно указать также само решение.

Мы могли бы задать даже более трудный вопрос: «Существует ли программа, которая будет производить определенные вычисления?» Из конструктивного доказательства ее существования можно было бы извлечь саму программу. (Очевидно, следует помнить, что сложные вопросы, вообще говоря, приводят к сложным доказательствам, возможно настолько сложным, что лоб Гл 1. Применения исчисления яредикатов к решению задач наши автоматические процедуры поиска доказательства их не найдут.) Основная цель настоящей главы — описать процесс, с по- ' мощью которого удовлетворяющий частный случай переменной, относящейся к квантору существования, в некоторой п. п.

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

п. формул исчисления предикатов первого порядка. Хотя та- кой процесс перевода должен быть одной из основных частей законченного решателя задач, мы его не будем здесь рассмат- ривать. Написано несколько программ, позволяющих осуще- ствлять в ограниченных рамках перевод с английского языка на язык исчисления предикатов, но способность работать с ес- тественным языком пока находится в весьма неудовлетвори- тельном состоянии. Можно выделить две главные трудности: (1) выбор отношений, которые следует использовать при пере- воде предложений с английского языка, и (2) однозначное преобразование смысла, вложенного в фразу, в п.

п. формулы, использующие предикатные символы для этих отношений. Часто неоднозначность можно устранить только рассмотрением «кон- текста» фразы, а это сопряжено с трудными и не до конца по- нятыми процессами. Проблема преобразования английского языка в п. п. формулы нисколько не легче, чем, например, проб- лема преобразования английского языка в описания состояний, операторы н т. д. В настоящей книге мы вынуждены оставить без рассмотрения вопросы перевода (сколь ни важны они) и сосредоточить все свое внимание на процессах решения уже сформулированных задач. 7.2. ПРИМЕР Рассмотрим следующую тривиальную задачу: «Если Майкл повсюду ходит за Джоном, а Джон находится в школе, то где Майкл?» Совершенно ясно, что в этой задаче сформулированы два «факта», а затем поставлен вопрос, который, по-видимому, можно вывести из этих двух фактов.

Этн факты легко перево- дятся на язык п. п. формул и дают следующее множество 3 п. п. формул: ()тх)(АТ (Джон, х) )»АТ (Майкл, х)) и АТ (Джон, школа), 7.2. Пример 207 где предикатному символу АТ придана очевидная интерпретация («быть в определенном месте», соответствующая предлогу «в» — дерев.) . На вопрос «Где Майкл?» можно дать ответ, если сначала доказать, что п. п. формула (:-(х) АТ (Майкл, х) следует из 5, и затем найти тот частный случай переменной х, «который существует».

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

7Л. Дерево опровержения для рассматриваемого примера. (Чх) ( АТ (Майкл, х)), или, в форме предложения„просто АТ (Майкл,х), нз 5. После нахождения доказательства мы пытаемся извлечь тот частный случай переменной, относящейся к квантору существования, который служит ответом. В нашем примере легко доказать, что (Эх) АТ (Майкл,х) следует из 5. Легко также показать, что соответствующий ответ можно, извлечь с помощью сравнительно простой процедуры. Доказательство получается обычным путем.

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

7.1. Правильно построенная формула, которую предстоит доказать, называется предположением, а предложения, получающиеся из п. п. фор. мул, содержащихся в 5, называются аксиомами. Заметим, что отрицание п. п. формулы (Зх)АТ (Майкл,х) дает 2сз Гл, 7. Применения исчисления нредикагов к решению задач Теперь из этого дерева опровержения извлечем ответ на вопрос «Где Майкл?» Это осуществляется следующим образом: (1) К каждому предложению, вытекающему из отрицания предположения, добавляется его отрицание. Тогда -АТ(Майкл, х) принимает вид тавтологии ') АТ(Майкл, х) ~/АТ(Майкл,х).

(2) В соответствии со структурой дерева опровержения выполняются те же самые резольвенцииз), что раньше, до тек пор пока в его корне не будет получено некоторое предложение. »Ат(Манил.к) и АТ(май л, А Т(майюкк) А Т(Ллсацх) и АТ(майкл,к( Амми, шкаиз) А Т(майкл, шкалаЗ Р ис 7.2. Модифицированное дерево доказательства для рассматриваемого примера.

В нашем примере этот процесс порождает дерево, показанное на рис. 7.2, с предложением АТ(Майкл, школа) в его корне. (3) Предложение в корне преобразуется в обычную форму исчисления предикатов и используется в качестве - ответного утверждения. Эту п. п, формулу затем можно снова перевести на, скажем, английский язык, как ответ на вопрос. Очевидно, что в нашем примере АТ(Майкл, школа) и является соответствующим ответом задачи. Заметим, что форма ответного утверждения близка к форме предположения.

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

и. формула вида ат'и' ат. з) Смысл слов чте же самые резолзвеннии» мы объясним позже. 7.8. Процесс из«ее«ение ответа цесса и обсудим, как применять его в случаях, когда предположение содержит как кваиторы всеобщности, так и кванторы существования. 73. ПРОЦЕСС ИЗВЛЕЧЕНИЯ ОТВЕТА Извлечение ответа связано с преобразованием графа опровержения (с и!! в его корне) в граф, у которого в корне находится некоторое утверждение, могущее служить ответом. Так как при таком преобразовании каждое предложение, возникающее из отрицания предположения, превращается в тавтологию, то преобразованный граф представляет собой доказательство того, что утверждение, расположенное в его корне, логически следует из аксиом и тавтологий.

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

Характеристики

Список файлов книги