Intel_Nils (526801), страница 43
Текст из файла (страница 43)
Доказательство, представленное на рис. 7.1, будет справедливо и.в случае, если вместо константы а взять переменную. Можно показать (Лакхэм и Нильсон, 197!), что в процессе извлечения ответа всегда можно заменять любые сколемовы функции, возникающие при отрицании предположения, новыми переменными. В модифицированном доказательстве в эти новые переменные не будет делаться никаких подстановок, так что они пройдут через доказательство без изменения и появятся в окончательном ответном утверждении.
Резольвенциями в модифицированном доказательстве по-прежнему будут лишь резольвен. .ции, определяемые множествами унификации, соответствующими множествам унификации, появляющимся в ходе первоначального опровержения. В процессе некоторых резольвенций переменные могут быть переименованы, так что, возможно, некоторая переменная, использованная на месте сколемовой функции, окажется переименованной и станет, таким образом, «родоначальником» новых переменных в окончательном ответном утверждении.
Продемонстрируем на двух простых примерах некоторые явления, связанные с этой особенностью. При мер 3. Пусть 5 состоит из единственной аксиомы (в форме предложения) Р (Ь, гв, га) ~/ Р (а, и, и). Нам нужно доказать предположение ()х1г2")у) Р(х, а, у). Дерево опровержения изображено на рис. 7.8, а. В предложении, происходящем из отрицания нашего предположения, содержится сколемова функция п(х). На рис. 7.8, б изображено дерево модифицированного доказательства, в котором вместо сколемовой функции д(х) стоит переменная й Мы получаем доказательство ответного утверждения Р (а, (, г) ~/ Р (Ь, г, г), совпадающего (с точностью до наименования переменных) с нашей аксиомой.
Этот пример показывает, каким образом по-являются в ответном утверждении новые переменные, введенные 7.4. Лредиоложеиия с ивовтором всеобщности 2!7' при переименовании в процесс резольвенции переменных в одном предложении. П р и мер 4. Допустим, что нам нужно доказать то же самое. предположение, что и в предыдущем примере, но теперь исходи — РР(хту(х),у) Р(Ь, ея ч р(а,иеи) Р(ь,амит Р(х)РУ) ий Р(х,Цф ч Р(х$Я Р(аси,и) Р(й,ш,и() Ч Р(а,(,!) ч Р(х,(,Р) Р(аЩ Ч Р(Ь,т,х) Р в с, 7.8.
Деревья доквэвтельства для ярвмерв 3. из аксиомы Р(х, и, г) х/ Р(а, и, и). Дерево опровержения изображено на рис. 7.9, а. В предложении, происходящем из отрицания предположения, содержится сколемова функция д(х). На рис. 7,9, б изображено дерево модифицированного доказательства, в котором вместо сколемовой функции Р(х] 218 Гл. 7.
Прииенения исчисления нредикатое к решению задач использована переменная о. Мы получаем доказательство ответного утверждения Р(з, гв, х) ~/ Р(а, ге, ге), совпадающего (с точностью до наименований переменных) с исходной аксиомой. Внимательный анализ унифицирующих под- Р вг и)> Рани з.д(а),г) нц р(а,ш,р) Ч Р(жю,р) Р(а и„и) -я(а,гли) ч р(,ю, Р(глас) ч Р(а,ы,ьх Рис 7.9. Деревья доказательства для врииера 4.
становок в этом примере показывает, что, хотя резольвенции в модифицированном дереве и ограничены соответствующими множествами унификации, подстановки, используемые в модифицированном дереве, могут носить более общий характер по сравнению с подстановками в первоначальном дереве опровержения. В заключение перечислим этапы процесса извлечения ответа: 219 7.5. Пример автоматического написании нрограммы 1.
В ходе некоторого процесса поиска (перебора) строим граф опровержения на основе резольвенций и выделяем в нем множества унификации. 2. Вместо сколемовых функций, которые появляются в предложениях, происходящих из отрицания предположения, подставляем новые переменные. ' 3. Предложения, происходящие из отрицания предположения, превращаем в тавтологии, приписывая к ним их же отрицания.
4. Следуя структуре первоначального графа опровержения, строим граф модифицированного доказательства. В каждой резольвенции модифицированного графа используем множество унификации, определяемое множеством унификации, используемым при соответствующей резольвенции в графе опровержения.
5. Предложение, находящееся в корневой вершине модифицированного графа, представляет собой ответное утверждение, извлеченное в ходе описываемого процесса. Очевидно, что ответное утверждение зависит от того опровержения, из которого оно было извлечено. Возможно, для одной и той же задачи существует несколько различных опровержений.
Из каждого такого опровержения мы могли бы извлечь ответ, и хотя некоторые из ответов могут совпасть, тем ие менее некоторые утверждения, составляющие ответ, могут оказаться более общими, чем другие. Обычно у нас нет возможности установить, является ли ответное утверждение, извлеченное из данного доказательства, наиболее общим. Мы могли бы, конечно, продолжать поиск доказательств до тех пор, пока не найдем доказательство, дающее достаточно общий ответ.
Но вследствие неразрешимости исчисления предикатов не всегда можно установить, нашли ли мы все возможные доказательства для п.п. формулы й7 исходя из множества 5. Эта трудность представляет, по-видимому, лишь теоретический интерес. В приводимых ниже примерах получаемые ответы вполне удовлетворительны. 7 з. пРимеР АптомАтическОГО нАписАния пРОГРАммы При соответствующей формализации описанный выше процесс извлечения ответа можно применять для автоматического построения простых программ для вычислительной машины. При существующем уровне развития таких методов приемы автоматического доказательства теорем пригодны для написания лишь простейших программ.
Мы проиллюстрируем этот подход на примере. Общая же проблема автоматического синтеза программы пока еше выходит за рамки возможностей всех имеющихся в настоящее время подходов. 220 Гл. 7. Применения исчисления нрсдикатов к реиинию задач Предположим, что мы хотим написать программу, в которой в качестве входной переменной берется х, а на выходе получается значение у, удовлетворяющее какому-то соотношению )с(х,у). Мы считаем, что некоторым множеством аксиом определена интерпретация предикатной буквы )с.
Другие аксиомы задают элементарные функции, из которых мы будем конструировать нашу программу (создавая композиции функций). С помощью процесса извлечения ответа система доказательства теорем построит требуемую программу, если она сможет доказать, что предположение (з!гну) тс(х, !7) логически следует из указанных аксиом.
После того как доказательство-будет найдено, в ответном утверждении будет предположенное у как композиция элементарных функций. Эта композиция функций тогда и будет программой. Для того чтобы писать интересные программы, мы должны располагать элементарными функциями, допускающими условные ветвления и либо итерации, либо рекурсии. Такие языки программирования, как 1!ЯР '), дают возможность писать рекурсивные программы. Для формализации действия функций„ допускающих условные ветвления (таких, как функция сопб в языке ПЗР), требуется либо возможность работать с отношением равенства, либо наличие специальных правил вывода. В настоящей книге мы не рассматриваем вопрос отношения равенства; пока еще неясно, какой именно из предлагаемых методов работы с равенством приемлем (и приемлем ли хоть один из них вообще). В некоторых случаях можно обойтн эту трудность и создать рекурсивные программы с ветвлением при проверке выполненности условий окончания.
Используемые в этих случаях приемы лучше всего пояснить на конкретном примере. Допустим, что мы хотим составить программу, сортирующую входной список чисел. Выходом должен быть другой, список, содержащий те же самые числа, расположенные в порядке их убывания. Мы будем строить программу из элементарных функций саг, сбг, сопз и тетке. Первые три из них являются элементарными функциями языка программирования 1)ЯР. Они определяются следующим образом: саг(х) имеет в качестве своего значения первый элемент списка х; сбг(х) имеет в качестве своего значения ту часть списка х, которая остается после удаления из него первого элемента; сопз (х,д) имеет в качестве своего значения список, получаемый в результате размещения перед списком у элемента х.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
