ЛМвИИ (1086253), страница 10

Файл №1086253 ЛМвИИ (Учебник - Логические методы в искусственном интеллекте (2,3 и 5 глава)) 10 страницаЛМвИИ (1086253) страница 102018-01-12СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

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

Если это не удается, то взять вкачестве допущения (дополнительной гипотезы) отрицание последнего консеквента ивывести противоречие.• Если главным знаком формулы является конъюнкция, то сначала доказываются вкачестве теорем члены конъюнкции. Например, доказать формулу А^В:1. А - теорема;2. В - теорема;3. А^В - из 1 и 2 по П1 (см. ниже).4. ├А^В по определению вывода на основе 1 — 3.Для приведенного выше примера будем иметь две гипотезы:c→d и ¬d.Заметим сразу, что правила (первого рода), приведенные в §1.5 правомерны и длялогики предикатов первого порядка, только надо иметь в виду, что литеры в этих правилахпредставляют предикатные формулы. Специфика же для логики предикатов первого порядкапривносит дополнительные правила, связанные с квантификацией переменных.

Не будем вы-.писывать эти формулы вновь, но будем иметь в виду, что при анализе предикатных формулссылка на правило с меткой Пi соответствует правилу Вi. Здесь же мы выпишем правила,специфические для логики предикатов первого порядка:П14. Отрицание квантора существования: ¬∃хА(х)├∀х¬А(х)П15. Удаление квантора общности: ∀xA(x)├A(t), где А(t) - результат правильнойподстановки терма t вместо x;П16. Введение квантора существования: A(t)├∃xA(x), где A(t) - результат правильнойподстановки терма t вмесго х;П17. Введение квантора общности: А(х)├∀yA(y), где А(y) - результат правильнойподстановки переменной y вместо x.П18. Удаление квантора существования: ∃уА(у)├А(x), где А(х) - результат правильнойподстановки переменной х вместо y в A(y);П19.

Правило дедукции: (Г, А├В) ├ (Г├А→В),П20. Доказательство от противного: (Г, ¬A├B^¬B)├(Г├A);П21. Сведение к абсурду: (Г, ¬А├В^¬В)├(Г├¬А).Правила П1- П18 являются правилами первого рода, правила П19 - П21 - правилавторого рода.Приведем пример использования правил для доказательства выводимости.

Для началазавершим приведенный пример. Итак, доказать (вывести) теорему(c→d)→(¬d→¬c).1. c→d - гипотеза;2. ¬d - гипотеза;3. ¬c - из 1 и 2 по П7.Получили множество формул {c→d, ¬d}, из которого последовал вывод ¬с, т.е.4. {c→d, ¬d}├¬с;5. (c→d├(¬d→¬c) из 4 по П19;6. ├(c→d)→(¬d→¬c) из 5 по П19.Следует сделать существенное замечание по поводу применения правил П13 - П18. Впрямом выводе необходимо отслеживать правильность подстановок переменных, связанных исвободных. Это в значительной степени усложняет доказательство выводимости и, главное,делает проблематичным использование для машинной реализации.

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

фактически опишем, как получать дизъюнкты).Формула вида Q1x1...Qn xn (M), где каждые Qi xi есть либо ∀xi , либо ∃хi , a M -формула,не содержащая кванторов, называется формулой в предваренной нормальной форме.При преобразовании формулы в предваренную нормальную форму можновоспользоваться следующими основными равносильностями:¬∀xP(x) ≡ ∃x¬P(x),(2.1)¬∃хР(х) ≡ ∀х¬Р(х),(2.2)¬∀x¬P(x) ≡ ∃xP(x),(2.3)¬∃х¬Р(х) ≡ ∀хР(х),(2.4)Пусть R - формула, не содержащая переменной х, тогда∀xR ≡ R,(2.5)∃xR ≡ R,(2.6)∀xP(x)vR ≡ ∀x(P(x)vR),(2.7)∀xP(x)^R ≡ ∀x(P(x)^R),(2.8)∃xP(x)vR ≡ ∃x(P(x)vR),(2.9)∃xP(x)^R ≡ ∃x(P(x)^R).(2.10)Законы (2.7), (2.9) и (2.8), (2.10) можно обобщить законами:(Qx)P(x)vR ≡ (Qx)(P(x)vR),(2.9а)(Qx)P(x)^R ≡ (Qx)(P(x)^R),(2.10a)∀xP(x)^∀xR(x) ≡ ∀x(P(x)^R(x)),(2.11)∃xP(x)v∃xR(x) ≡ ∃x(P(x)vR(x)),(2.12)∀xP(x) ≡ ∀yP(y),(2.1З)∃xP(x) ≡ ∃yP(y).(2.14)Формулы (13) и (14) имеют место при условии, что x и у принимают свои значения изодной и той же области.∀xP(x)v∀xR(x) ≢ ∀x(P(x)vR(x)),(2.15)∃xP(x)^∃хR(x) ≢ ∃x(P(x)^R(x)),(2.16)Поскольку каждая связанная переменная в формуле может рассматриваться как местодля подстановки, то следует в этих формулах одно из вхождений х переименовать, например, наz.

Пусть выбрана переменная z, которая не встречается в Р(x), тогда формулы (2.15) и (2.16)принимают вид:∀xP(x)v∀xR(x) ≡ ∀x∀z(P(x)vR(z)),(2.17)∃xP(x)^∃xR(x) ≡ ∃x∃z(P(x)^R(z)),(2.18)В общем случае имеем Q1x1...Qn xn(Q1x)P(x)v(Q2x)R(x) ≡ (Q1x)(Q2z)(P(x)vR(z)),(2.17a)(Q1x)P(x)^(Q2x)R(x) ≡ (Q1x)(Q2z)(P(x)^R(z)),(2.18a)∃x∀yP(x, y) ≢ ∃y∀xP(x, y),(2.19)∃x∀yP(x, y) ≢ ∀y∃xP(x, y).(2.20)Далее, та часть формул, которая не имеет кванторов, приводится к конъюнктивнойнормальной форме с использованием алгебраических преобразований для операций ¬, ^(&), v,→, ↔.Приведем алгоритм преобразования формул в предваренную нормальную форму.Шаг 1.

Исключаем логические связки → и ↔, используя законыP↔R ≡ (P→R)^(R→P),P→R ≡ ¬PvR.Шаг 2. Используем законы▪ двойного отрицания: ¬(¬P) ≡ P;▪ законы де Моргана:¬(PvR) ≡ ¬P^¬R,¬(P^R) ≡ ¬Pv¬R;▪ для внесения отрицания внутрь формулы используем:¬∀xP(x) ≡ ∃x¬P(x),¬∃хР(х) ≡ ^∀¬Р(х).Шаг 3. Переименование связанных переменных.Шаг 4. Используем законы (2.9а), (2.10а), (2.11), (2.12), (2.17a) и (2.18a).Шаг 5. Используем закон дистрибутивности, заменяя формулы вида(А^В)vC на (AvC)^(BvC);Av(B^C) на (AvB)^(AvC).И, наконец, чтобы избавиться от кванторов, используется процедура сколемизации,которая состоит в следующем: кванторы просматриваются слева направо до первого кванторасуществования ∃, при этом• если в кванторной приставке Q1x1...Qnxn квантор ∃xi не имеет левее себя кванторов ∀xj,то везде в формуле М переменная xi заменяется на некоторую неопределеннуюконстанту;• если в кванторной приставке квантор ∃xi стоит правее кванторов ∀xj1, …, ∀xjK (k<n), товезде в формуле M переменная хi заменяется на некоторую неопределеннуюфункцию fiC (xj1, …, xjK),• после исключения всех кванторов существования кванторы общности простоотбрасываются.

Считается, что все оставшиеся переменные связаны кванторамиобщности, поэтому их отбрасывание не влечет неоднозначностей в понимании формул.Элементарные дизъюнкции, полученные в результате выполнения описанных вышепроцедур, называются дизъюнктами.Примеры.1. Пусть задано множество X целых чисел x , y ∈ X и введем предикат Р(у, y),устанавливающий отношение "больше" между двумя числами.

Тогда на заданном множестведля ∀x существует y такое, что у>х, т.е. справедлива истинность предиката Р(y, х): ∀x∃yP(y, x).В соответствии с приведенным выше алгоритмом сколемизации имеем: P(fC(x), ). Тогдана основании веденного в примере определения предиката сколемовская функция в частностиможет иметь вид: fC(х)=х+1.2.

Получить дизъюнкты для формулы∃x(∃yP(x, y)v∃zQ(x, z)→∃vR(x,v)).Избавимся от импликации:∃x(¬(∃yP(x, y)v∃zQ(x, z))v∃vR(x, v)) = ∃x(¬∃yP(x, y)^¬∃zQ(x, z)v∃vR(x, v) =∃x(∀y¬P(x, y)^∀z¬Q(x, z)v∃vR(x, v))Вынесем кванторы в начало формулы:∃x∀y, z∃v(¬P(x, y)^¬Q(x, z)vR(x, v)).Отметим, что это один из множества допустимых вариантов вынесения кванторов.Здесь возможно получение кванторной приставки ∃x∀z, y∃v и даже ∃x, v∀y, zПолученную на предыдущем шаге формулу приводим к конъюнктивной нормальнойформе:∃x∀y, z∃v((¬P(x, y)vR(x, v)) ^ (¬Q(x, z)vR(x, v))).И, наконец, выполняем сколемизацию:(¬P(aC, y)vR(aC, fC(y, z)))^(¬Q(aC, z)vR(aC, fC(y, z))).

В результате получаем двадизъюнкта, которые обычно записываются через запятую:(¬P(aC, y)vR(aC, fC(y, z))) и (¬Q(aC, z)vR(aC, fC(y, z))).2. Получить дизъюнкты для формулы:∀x∃yP(x, y)^¬∃y∀zR(y, z) = ∀x∃yP(x, y)^∀y∃z¬R(y, z) =∀x∃yP(x, y)^∀v∃z¬R(v, z) = ∀x∃y∀v∃z(P(x, y)^¬R(v, z)) = P(x, f1C(x))^¬R(v, f2C(x, y)).В результате имеем два дизъюнктаP(x, f1C(x)) и R(v, f2C(x, y)).2.5. Теорема Эрбрана.Если формула в языке первого порядка невыполнима, т.е. не имеет интерпретации, тоневыполнимым является и множество дизъюнктов, полученное из этой формулы (т.е.

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

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

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

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

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