Intel_Nils (526801), страница 47
Текст из файла (страница 47)
(1969). В частности, программа Гарда (в какой-то мере с помощью человека) успешно справилась с задачей пояска первого доказательства одного предположения теории модулярных структур. .Задачи тн. Приведите соображения за или против следующего утверждения: мИспользовенне формальных процедур доказательства будет приносить весьма малую пользу в любой системе решения задач, предназначенной для решеняя значительных, практически важных задач».
7.3. Примените процесс навлечения ответа к дереву опровержения на основе резольвенции, изображенному иа рис. 7.!1, с тем, чтобы получить ответное утверждение Я (х,шегяе(саг(х). зог((сбг(х)))). 7.3. Напишите формулы исчисления предикатов, содержащие переменные состояния, которые задают условия применимости и результаты воздействия .операторов «подойти», «передвинуть», «взобраться» и «схватить», используемых в задаче об обезьяне и бананах иэ разл, 7.6.
Из этих формул и предвкатов, описывающих начальное состояние 5„ получите доказательство иа основе резольвенции того, что обезьяна может схватить бананы, С помощью процесса извлечения ответа найдите выражение для целевого состояния. (Замечание: это упражнение есть просто усложненный вариант примера из равд.
7.7.) 7.4. Робот по перевозке грузов, отправляющийся из фирмы «Универсал пластик ннкорпорейшн», должен отвезти безделушни, браслеты, бусы соответ.ственно в магазины Гамаа, Мейси и Сака. Используя простые операторы типа «перевозить (х,у)» н «разгружать (х)» с соответствующими предварнтельнымн условиями и результатами действия, покажите, как система решения задач в пространстве состояний, опирающаяся иа ясчислеиие предикатов, могла .бы найти последовательность операторов, создающую состояние, удовлетворяющее п.п. формуле АТ(безделушки, Гани) Л АТ(браслеты, Мейсн) Л АТ(бусы, Сак).
Задачи «Т.б. Напяшнте программу для вычислительной машины, реализующую процесс извлечения ответа на основании поданного на ее вход дерева опровержения на основе резольвенций. 7.6. Сформулируйте в виде выражений исчисления предикатов факты и вопросы, содержащиеся в следующей задаче. Воспользуйтесь прянципом резольвенцин с извлечением ответа. Тони, Майкл и Джон принадлежат к Альпинклубу.
Каждый член Альпин. клуба являетсн либо скалолазом, либо гориолыжнином, либо тем и другим. Нн один из скалолазов ие любит дождь, и все горнолыжники любят снег. Майкл не любит все, что любит Тони, и любит все, что не любит Тонн. Тонн любит снег и дождь. Есть ли в этом Альпинклубе хотя бы один член, который является сналолазом, но не валяется горнолыжникомг Кто? Глава 8 МЕТОДЫ ПОИСКА ДОКАЗАТЕЛЬСТВА В ИСЧИСЛЕНИИ ПРЕДИКАТОВ 8.1. СТРАТЕГИИ ПЕРЕБОРА В гл. 6 мы отметили, что непосредственное применение принципа резольвенции соответствовало бгя простой процедуре полного перебора при построении опровержения.
Такой перебор мы начинали бы с множества предложений 5, к которому добавляли бы все резольвенты всех пар предложений в 5 с тем, чтобы образовать множество Я. Затем добавляли бы все резольвенты всех пар предложений в Я с тем, чтобы образовать множества Я(Я(5)) = Я'(5), и т.
д. Этот тип перебора, как правило, непригоден для практики, ибо множества Я(5), Я'(5), ... слишком быстро разрастаются. Практические процедуры доказательства определяются стратегиями перебора, применяемыми для его ускорения. Такие стратегии бывают трех типов: стратегии упрощения, стратегии очищения и стратегии упорядочения. Стратегии упорядочения точнее' двух других стратегий соответствуют методам, применяемым при переборе на графах в пространстве состояний и «И/ИЛИ» графах, В настоящей главе мы кратко обсудим все трн типа стратегий.
8лн СТРАТЕГИИ УПРОЩЕНИЯ Иногда множество предложений удается упростить, исключив из него некоторые предложения или исключив нз предложений определенные литералы. Эти упрощения таковы,'что упрощенное множество предложений выполнимо тогда и только тогда, когда выполнимо исходное множество предложений.
Таким образом, применение стратегий упрощения позволяет снизить скорость роста числа новых предложений. Исключение тавтологий Любое предложение, содержащее литерал и его дополнение (такое предложение называется тавтологией), можно отбросить, так как любое невыполнимое множество, содержащее тавтологию, остается невыполнимым и после ее удаления, и обратно. Так, предложения типа Р(з) Ч В(я) Ч В(у) и РЦ(а)) Ч РЯ(а)) можно отбросить. 8.8.
Стратегии очищения Исключение путем означивания предикатов Иногда появляется возможность означить (выяснить значепие истинности) литералы, и это оказывается удобнее, чем включать соответствующие предложения в Я. Такое означивание часто легко провести для константных частных случаев. Например, если предикатная буква Е обозначает отношение равенства, то означивание константных частных случаев типа .Е(7,3), когда они появляются, провести легко, хотя нам бы не хотелось добавлять к Е полную таблицу. содержащую много константных частных случаев литералов Е(х,у) и Е(х,у). Если какой-нибудь литерал предложения получает значение истинности Т, то все предложения можно отбросить, не нарушая при этом свойства невыполнимости оставшегося множества. Если же какой-нибудь литерал при означивании получает значение истинности Р, то из этого предложения можно исключить данное вхождение литерала. Так, предложение Р(х)~/ Ъ' Я(а) ч т Е(7,3) можно заменить на Р(х) '/11(а), поскольку значение истинности для Е(7, 3) есть Р.
Исключение подслучаев Предложение (Ег) называется подслучаем предложения (Мт), если существует такая подстановка й, что (Ет)о«:-(М,). Напри- мер, Р(х) — подслучай предложения Р(у) ~/ Я(з), Р(х) — подслучай предложения Р(а), Р(х) — подслучай предложения Р (а) Ч чс(в), Р (х) ч7 (7(а) — подслучай предложения Р (7 (а)) ~l Я (а) Ч )7(у). Предложение в Е, являющееся подслучаем другого предложения в 3, можно исключить из 5, не нарушая свойства невыполнимости оставшегося множества. Отбрасывание предложений, являющихся подслучаями других, часто ведет к значительному уменьшению числа резольвенций, необходимых для нахождения доказательства.
Вообще в то время, как тавтологии можно отбрасывать сразу же, как только они появляются в процессе поиска доказательства, предложения, являющиеся подслучаями, можно отбрасывать лишь после того, как каждый «уровень» оказывается завершенным (Ковальский, 1970). 8.8. СТРАТЕГИИ ОЧИЩЕНИЯ Стратегии очищения основаны на тех теоретических результатах в теории доказательства с помощью резольвенций, в которых утверждается, что для нахождения опровержения не 238 Гл. 8. Метода ооиска доказательства в исчислении иоедикатов нужны все резольвенции. Иными словами, достаточно выполнить резольвенции только для предложений, удовлетворяющих определенным требованиям.
Мы будем обозначать через Яс(5) объединение множества 5 и множества всех резольвент всех пар предложений из 5, удовлетворяющих критерию С. Ясно, что 'Яс(5) с= Я(5). Про стратегию очищения, использующую критерий С, говорят, что в ней используется «резольвенция по отношению к С». Для применения такой стратегии мы сначала вычисляем Яо(5), затем Яс(Яс(5))=Яс(5) и т. д. до тех пор, пока при некотором и в Я~~(5) не окажется пустого предложения (обозначаемого п!1).
Потенциальное достоинство стратегии очйщения в том, что на каждом уровне требуется меньше резольвенций. Однако уровень, на котором появляется пустое предложение, обычно возрастает, так что стратегия очищения приводит обычно к узконаправленному, но более глубокому перебору. Стратегия очищения полезна лишь в том случае, если она уменьшает все затраты усилий на перебор, включая усилия, необходимые для проверки выполнимости критерия С. Мы рассмотрим две основные стратегии очищения, снижающие затраты усилий на перебор, а также некоторые их частные случаи.
8Л. ФОРМЫ ДОКАЗАТЕЛЬСТВА С ОТФИЛЬТРОВЫВАНИЕМ ПРЕДШЕСТВУЮЩИХ ВЕРШИН Нашу первую стратегию очищения легко описать в терминах тех типов графов опровержения, которые она образует. Полезно сначала ввести некоторые определения. Графом (или деревом) доказательства на основе резольвенций называется структура, в которой каждая вершина соответствует некоторому предложению. (Для простоты мы часто будем отождествлять вершину этого графа с '.предложением.) Вершины графа, у которых нет предшествующих вершин, называются концевыми вершинами. Если граф изображает доказательство на основе резольвенций некоторого предложения (возможно пД), исходя из множества предложений 5, то концевые вершины соответствуют предложениям из 5. Они называются базовыми предложениями этого доказательства. Вершина графа, у которой нет следующих за ней вершин, называется корневой вершиной. Она соответствует предложению, доказанному этим графом.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
