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

Файл №526801 Intel_Nils (Intel_Nils) 47 страницаIntel_Nils (526801) страница 472013-09-29СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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. Они называются базовыми предложениями этого доказательства. Вершина графа, у которой нет следующих за ней вершин, называется корневой вершиной. Она соответствует предложению, доказанному этим графом.

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

Тип файла
DJVU-файл
Размер
2,05 Mb
Материал
Тип материала
Высшее учебное заведение

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

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6418
Авторов
на СтудИзбе
307
Средний доход
с одного платного файла
Обучение Подробнее