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

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

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

В рассмотренных в этомразделе примерах на каждом шаге вывода мы ссылались на определенное правило, следствиемчего и стал вывод на данном шаге. Теперь мы можем привести полный перечень правил вывода,который поможет сориентироваться при выборе пути доказательства. Приведенные нижеправила следует трактовать следующим образом: из истинности левой части следует праваячасть. Использован знак следования ├.B1. Введение конъюнкции: А, В├А^ВB2. Удаление конъюнкции: А^В├В; А^В├А;B3. Отрицание конъюнкции (закон Де Моргана): ¬(A^B)├¬Av¬BB4.

Введение дизъюнкции: А├АvB; В├АvВB5. Удаление дизъюнкции: AvB, ¬B├A; AvB, ¬A├BB6. Отрицание дизъюнкции (закон Де Моргана): ¬(AvB)├¬A^¬BB7. Удаление импликации (modus ponens): A→B, A├BВ7'. Удаление импликации (modus tollens): A→B, ¬B├¬AB8. Отрицание импликации: ¬(A→В)├А^¬ВB9. Введение эквивалентности: А→В, В→А├А↔В;B10. Удаление эквивалентности: А↔В├A→В;B11. Введение двойного отрицания: А├¬¬AB12. Удаление двойного отрицания: ¬¬A├AB13. Правило дедукции: (Г, A├B)├(Г├A→B)B14. Доказательство от противного: (Г, ¬A├B^¬B)├(Г├A)B15.

Сведение к абсурду: (Г, А├В^¬В)├(Г├¬A)1.2.3.4.5.6.В правилах B1 - В15 А и В - формулы, а Г- множество формул, возможно пустое.Пример. Обосновать выводимость A→(B→C), A^B├CA→(B→C) - гипотеза;А^В - гипотеза;А - из 1 по В2;В→С - из 1 и 3 по В7;B - из 2 по В2;С — из 4 и 5 по В7.Следовательно, А→(В→С), А^В├C- по определению вывода на основе 1 — 5.1.6. Непрямые методы вывода. Метод резолюции.Метод резолюции - это один из методов доказательства от противного.Метод, введенный Дж.Робинсоном, является теоретической базой для построениябольшинства методов доказательства теорем.

Робинсон пришел к заключению, чтообщепринятые правила вывода, например, правило modus ponens, позволяют человекуинтуитивно проследить за каждым шагом процедуры доказательства. Он открыл более сильноеправило резолюций, которое трудно поддается восприятию, но эффективно реализуется накомпьютере. При использовании правила резолюции можно вывести любое из множестваксиом, представленных во фразовой форме.Не существует по-настоящему эффективных критериев проверки выполнимости КНФ.Метод резолюции позволяет выявить невыполнимость множества дизъюнктов. Действительно,множество дизъюнктов невыполнимо тогда и только тогда, когда пустой дизъюнкт  являетсялогическим следствием из него.

Таким образом невыполнимость множества S можно проверить,порождая логические следствия из S до тех лор, пока не будет получен пустой дизъюнкт.Для порождения логического следствия используем простую схему рассуждений. ПустьА, В и X - формулы. Предположим, что две формулы С1: (AvX) и С2: (Bv¬X) - истинны.

Если Xтоже истинна, то можно заключить, что и В истинна. Наоборот, если X ложна, то можнозаключить, что А истинна. В обоих случаях (AvB) истинна. Получаем правило:{AvX, Bv¬X}├AvB, или в равносильной форме{¬X→A, X→B}├AvB.Мнемоническое правило вывода можно сформулировать следующим образом: еслипара исходных дизъюнктов множества S содержит контрарные литералы (X и ¬Х), то новыйдизъюнкт формируется из оставшихся частей дизъюнктов, не содержащих эти контрарныелитералы.

Этот вновь сформированный дизъюнкт называется резольвентой исходныхдизъюнктов.Общезначимость правила резолюций выражается следующей леммой.Лемма 1. Пусть s1 и s2 - дизъюнкты нормальной формы S, I - литера. ЕслиI ∈ s 1 и ¬ I ∈s 2 , то дизъюнкт r=(s1\{l})v(s2\{¬l}) является логическим следствиемнормальной формы S.Если в процессе вывода новых дизъюнктов мы получаем два однолитерных дизъюнкта,образующих контрарную пару, то резольвентой этих двух дизъюнктов будет пустой дизъюнкт.

Таким образом, выводом пустого дизъюнкта  из множества дизъюнктов S называетсяконечная последовательность дизъюнктов С1, С2, …, СK такая, что любой Сi является илидизъюнкт из S или резольвентой, полученной принципом резолюции, и Q=.Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода,вершинами которого являются или исходные дизъюнкты или резольвенты, а корнем - пустойдизъюнкт.1.2.3.4.Пример. Пусть S = {PvQ, ¬PvQ, Pv¬Q, ¬Pv¬Q}. Пронумеруем исходные дизъюнкты:PvQ.5.

Q.(1, 2).¬PvQ.6. ¬Q. (3, 4).Pv¬Q.7. .(5, 6).¬Pv¬Q.Вывод представлен на рисунке 1.12с помощью дерева вывода.Рис. 1.12. Дерево вывода.Доказательство вывода формулы G из множества посылок F1, F2, …, Fn сводится квыводу противоречивости формулы F1^F2^...^Fn^¬G. Таким образом к исходному множествупосылок (аксиом) необходимо добавить отрицание выводимой формулы (теоремы).

Всевысказывания в задаче необходимо представить в форме дизъюнктов, и используя методрезолюций, вывести пустой дизъюнкт, т.е. доказать невыводимость из множества исходныхдизъюнктов отрицание теоремы. Тогда исходное утверждение должно быть верным. В этом изаключается доказательство от противного.Пример [9]. Если команда А выиграет в футбол, то город А1 торжествует, а есливыиграет команда В, то будет торжествовать город В1. Выиграет или команда A или команда В.Если выиграет команда А, то город В, не торжествует, а если выиграет В, то не будетторжествовать город А,. Следовательно, город В1 будет торжествовать тогда и только тогда,когда не будет торжествовать город А1.В символическом виде имеем:1.

А→А'.4. А→¬В'.2. В→В'.5. В→¬А'.3. AvB.6. В'→¬A'.Приведем высказывания к форме дизъюнктов. Последнее (шестое) высказывание,истинность которого надо доказать, представим в форме отрицания:¬(В'↔¬A') = ¬((¬B'v¬A')^(B'vA') = ¬(¬B'v¬A')v¬(B'vA') = (B'^A')v(¬B'^¬A') = (A'v¬B')^(¬A'vB').Перепишем все высказывания в форме дизъюнктов:1. ¬AvA'.8. A'vB.(1, 3).2. ¬ВvВ'.9. ¬BvA'.(2, 6).3. AvB.10.

A'.(8, 9).4. ¬Av¬B'.l1. Av¬A'.(3, 5).5. ¬Bv¬A'.12. ¬A v ¬A'.(4, 7).6. A'v¬B'.13. ¬A'.(11, 12).7. ¬A'vB'.14. .(10, 13).Задание: докажите это заключение прямыми методами.Упражнения.Звездочками отмечены задания, для которых приведены решения или даны ответы.Записать в символической форме следующие сложные высказывания:a) * если студент поздно ложится спать и на ночь пьет кофе, то утром у него плохоенастроение и болит голова;b) * если деталь не стоит в плане и обеспечена заготовкой, то, если она срочная и плансоставлен правильно, - неверно, что деталь не стоит в плане;c) Иванов сдал экзамен и получил пять неравнозначно тому, что Иванов получил пятьи сдал экзамен;d) если он едет, то он поезд, но это не значит, что если он стоит, то он не поезд;e) если ЭВМ исправна и мы не сделали ошибки, то мы сделали открытие тогда итолько тогда, когда, если ЭВМ неисправна и мы не сделали ошибки, то мы все-такичто- то сделали.2.

* Какие из приведенных ниже высказываний являются отрицанием высказывания "Петяпошел в институт":▪ не Петя пошел в институт;▪ Петя не пошел в институт;▪ Петя пошел не в институт.3. Каково значение истинности сложного высказывания "Речка движется и недвижется"?4. Придумать содержательное описание формул:a) (А↔¬В)→А^С,b) A→(B→(¬AvC));c) A|B→(C⊕D);d) (A→B)↔(A→C).5. Возможна ли ситуация, когда Av¬A ≡ ?.6. Построить таблицы истинности для формул:a) (A→B)v(A→B^A);b) (A↓B)→(A|C);c) (A^(B→A))→¬A;d) (A↔B)⊕C;e) (А|А)|(В|В);f) A→(B→(C→D)).7. * Выразить операции v и ^ через операции ¬ и →.8. Выразить операции ¬, v и ^ через :a) штрих Шеффера;b) стрелку Пирса.9.

Построить тавтологию и противоречие с использованием трех элементарныхвысказываний А, В и С.10. * Написать логическую формулу для заштрихованной области диаграммы Венна:1.11. * Построить формулу от трех переменных:a) которая принимает такое же значение истинности, как и большинство переменных;b) истинную в том и только в том случае, когда совпадает значение ровно двухпеременных.12. Придумать тернарную, т.е. зависящую от трех переменных, логическую операцию.13. Получить ДНФ для-формул:a) * ((x^y)v(x^y)vz)^(x^z);b) (xvy)^(¬xvz);c) * xvy;d) ((x^y)vz)^((x^z)vy);e) ¬(x^y)v¬(x^z);f) ¬(¬(x^y)^z);g) (x→y)^(y→x);h) ((x↔y)⊕z)|(x↓y);14. Получить КНФ для формул:a) * (x^y)vz;b) * x^y;c) (x ^ y)v(¬x ^ z);d) ((x^y)vz)^(¬yv¬z);15. Получить СДНФ для формул:a) * (xvy)^(¬xvz);b) * (x↓y) → (¬y|z);c) (x⊕y)|((xvy)↔(z → x));d) ¬(xvy)v(x^¬y);e) * xv¬xvy;f) x→y;16.

Получить СКНФ для формул:a) * (x^y)^(x^z);b) x↔y;c) * x^y;d) x^y^z;e) * x→(y→x);f) (x|y)→(x|z);g) (x|y)↔(x|z);h) (xvy)^(xvz)v(x^y);i) (xvy)^(¬x^z);j) (x↔y)⊕(x↔z);17. Получить СДНФ, а затем перейти к СКНФ:a) (x→(y→z))→((x→¬z)→(x→¬y));b) * (x → y) → (¬y→¬x);c) (xvyvz) ^ (xv¬z)^¬y;18. * Пусть задана функция f (сложное высказывание) от трех аргументов (элементарныхвысказываний) х, у и z и f(x, y, z)=x. Построить для данной функции СДНФ.19. Получить СКНФ, а затем перейти к СДНФ:a) (x | y) → (z→¬y);b) (x→(y⊕z)) → z;c) (x↔y) | (y | z);d) * (x | y)^(x^y);20. Получить МДНФ для формул:a) * ((x⊕y)↔z)→x;b) * (x⊕y) → ¬(xvy);c) ((A → B)↔(C↔D))v(¬(B → A)^(C ↔ D));d) * (¬Av¬BvC v ¬D)^(¬A v BvCv¬D);e) (x ↔ y)↔(x^z)21. Методом резолюции показать выводимость заключения с из множества гипотез:{m, m→(nvp), n→c, p→c}╞c.ГЛАВА 2.

ЯЗЫК ЛОГИКИ ПРЕДИКАТОВ ПЕРВОГОПОРЯДКА.2.1. Понятие предиката. Определения.Исходные элементы в логике высказываний являются атомами. Из атомов строятсяформулы. Каждый атом представляет собой повествовательное предложение, которое можетбыть истинным или ложным, но не одновременно и то и другое. Каждый атом рассматриваетсякак единое целое.

Структура атома и его состав не анализируется. Формулы могут выражатьразличные сложные мысли. Однако исчисление высказываний недостаточно для выражения,например, таких мыслей:1. 1. "Каждый человек смертен. Сократ- человек. Следовательно, Сократ смертен".2. 2. ''Всякое положительное число есть натуральное число. Число 3 - положительноечисло. Следовательно, 3 есть натуральное число".Каждое из приведенных рассуждений корректно. Однако, если мы введем, положим,для первого умозаключения обозначенияР: Каждый человек смертен,Q: Сократ — человек,R: Сократ - смертен,то R не есть логическое следствие Р и Q в рамках логики высказываний.

Это объясняется тем,что исчисление высказываний ограничивается структурой предложений в терминах простыхвысказываний, а приведенные рассуждения требуют анализа структуры предложений в смыслесвязи субъекта и предиката, как это делается в грамматике.

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

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

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

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