ЛМвИИ (1086253), страница 7
Текст из файла (страница 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 в рамках логики высказываний.
Это объясняется тем,что исчисление высказываний ограничивается структурой предложений в терминах простыхвысказываний, а приведенные рассуждения требуют анализа структуры предложений в смыслесвязи субъекта и предиката, как это делается в грамматике.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
