ЛМвИИ (1086253), страница 13
Текст из файла (страница 13)
Модель исследуемого "мира" представляется множеством аксиом, которыепреобразуются в множество дизъюнктов S.2. Для доказательства справедливости теоремы (В) в дан ном "мире" необходимо взять ееотрицание и, преобразовав в форму дизъюнкта (или дизъюнктов), добавить кмножеству S. Если теорема верна (выводима), то новое множество дизъюнктов (вместес отрицанием теоремы) должно быть противоречиво.3. Доказательство противоречивости сводится к доказательству того, что из данногомножества дизъюнктов может быть выведен пустой дизъюнкт.4. Чисто технически метод резолюции состоит из унификаций и получения множестварезольвент до тех пор, пока не будет получена пустая резольвента.5. Для уменьшения числа резольвент (а, следовательно, для повышения эффективностивывода) очень важна стратегия вывода, т.е.
определение того, в какойпоследовательности выбирать дизъюнкты для получения резольвент.6. Если множество дизъюнктов S противоречиво, то пустой дизъюнкт будет найден законечное число шагов. Однако, если множество S непротиворечиво, процессустановления этого факта может быть бесконечным.Пример. Показать выполнимость формулы А.А: ¬∃y∀z[P(z, y)↔¬∃x[P(z, x)^P(x, z)]].Методом резолюции докажем невыполнимость формулы ¬А. Для этого сперваисходную формулу приведем к дизъюнктивной форме.a) Исключим логическую связку ↔:∃y∀z{[P(z, y)→¬∃x[P(z, x)^P(x, z)]]^[¬∃x[P(z, x)^P(x, z)] → P(z, y)]}.b) Исключим логическую связку →:∃y∀z{[¬P(z, y)v¬∃x[P(z, x)^P(x, z)]]^[∃x[P(z, x)^P(x, z)]vP(z, y)]}.c) Внесем внешнее отрицание в скобки:∃y∀z{[¬P(z, y)v∀x[¬P(z, x)v¬P(x, z)]]^[∃x[P(z, x)^P(x, z)]vP(z, y)]}.d) Вынесем за скобки кванторы ∃ и ∀, сделав соответствующую замену переменных:∃y∀z∃v∀x{[¬P(z, y)v[¬P(z, x)v¬P(x, z)]]^[[P(z, v)^P(x, z)]vP(z, y)]}.e) Удалим кванторы существования (сколемизация):{[¬P(z, a)v¬P(z, x)v¬P(x, z)] ^ [P(z, f(z))^P(f(z), z)]vP(z, a)]}.f) Применим к правой скобке дистрибутивный закон:{[¬P(z, a)v¬P(z, x)v¬P(x, z)] ^ [P(z, f(z))vP(z, a)]}.1.2.3.4.5.6.7.Выпишем полученные дизъюнкты, изменив в каждом из них имена переменных:¬P(z1, a)v¬P(z1, x1)v¬P(x1, z1)P(z2, f(z2)) v P(z2, a)P(f(z3), z3) v P(z3, a)Попробуем найти резольвенту для дизъюнктов 1 и 2.
Претендентом на резольвированиеявляется литерал P(z2, a) из дизъюнкта 2. Поэтому для этого построим дизъюнктивнуюформулу ¬P(z1, a)v¬P(z1, x1)v¬P(x1, z1)vP(z2, a). Для этой формулы наиболее общимунификатором являетсяα1 = {a | x1, a | z2, a | z1}.После подстановки в 1 и 2 получим резольвентуР(а, f(а)).Для дизъюнктов 1 и 3 НОУ есть α2 = {a | x1, a | z1, a | z3}. Резольвентой для 1 и 3 являетсяP(f(a), a).Для 1 и 4 НОУ есть α3 = {a | x1, f(a) | z1}. Получим резольвенту¬P(f(a), a).Из 5 и 6 имеем.Теперь можно сделать заключение: ¬A не выводима, следовательно исходная Аформула значима.Пример.
Показать значимость формулы:A: ∃x∃y∀z{[P(x, y)→[P(y, z)^P(z, z)]]^[[P(x, y)^Q(x, y)] →[Q(x, z)^Q(z, z)]]}Докажем невыводимость ¬А. Как и в предыдущем примере, приведем формулу ¬А кдизъюнктивной форме.a) a) Исключим логическую связку →:¬∃x∃y∀z{[¬P(x, y)v[P(y, z)^P(z, z)]]^[¬[P(x, y)^Q(x, y)]v[Q(x, z)^Q(z, z)]]}b) Внесем внешнее отрицание в скобки:∀x∀y∃z{[P{x, y)^[¬P(y, z)v¬P(z, z)]]v[[P(x, y)^Q(x, y)]^[¬Q(x, z)v¬Q(z, z)]]}c) Удалим кванторы существования (сколемизация):{[P(х, у)^[¬Р(у, f(х, у))v¬P(f(х, у), f(х, y))]]v[(P(x, y)^Q(x, y))^[¬Q(x, f(x, y))v¬Q(f(x, y), f(x, y))]]}d) Применим дистрибутивный закон ко всему выражению.Преобразование выполняется в соответствии со схемой:[insert image here][P(x, y)vP(x, y)]^[P(x, y)vQ(x, y)]^[P(x, y) v ¬Q(x, f(x, y))^¬Q(f(x, y), f(x, y))]^[¬P(y, f(x, y))v¬P(f(x, y), f(x, y))vP(x, y)] ^[¬P(y, f(x, y))v¬P(f(x, y), f(x, y))vQ(x, y)] ^ [¬P(y, f(x, y))v¬P(f(x, y), f(x, y)) v¬Q(x, f(x, y)) v ¬Q(f(x, y), f(x, y))]e)Упрощение: из первого дизъюнкта удаляется одно вхождение Р(х, у), удаляются вседизъюнкты, содержащие Р(х, у), т.е.
2-й, 3-й и 4-й. Выпишем полученные дизъюнкты,заменив имена переменных в каждом дизъюнкте:1. Р(х1, y1).2. ¬P(y2 , f(x2 , y2)) v ¬P(f(x2, y2), f(x2, y2))vQ(x2, y2)3. ¬P(y3 , f(x3 , y3)) v ¬P(f(x3 , y3), f(x3 , y3)) v ¬Q(x3 , f(x3 , y3)) v ¬Q(f(x3 , y3), f(x3 , y3)).Для 1 и 2 находим унификатор {y2 | x1, f(x2 , y3) | y1} и (после подстановки)резольвенту:4. ¬P(f(x2 , y2), f(x2 , y2)) v Q(x2 , y2)Резольвируют дизъюнкты 1 и 4: унификатор {f(x2 , y2) | х1, f(x2 , y2) | у1} ирезольвента5. Q(x2 , y2)Дизъюнкты 3 и 5 с унификатором {f(x3 , y3) | х2 , f(x3 , y3) | х2) дадут резольвенту:6. ¬P(y3 ,f(x3 , y3)) v ¬P(f(x3 , y3), f(x3 , y3)) v ¬Q(x3 , f(x3 , y3))Теперь резольвируют дизъюнкты 5 и 6 с унификатором {x3 | x2 , f(x3 , y3) | у2}:7. ¬P(y3 , f(x3 , y3)) v ¬P(f(x3 , y3), f(x3 , y3))8.9.Для дизъюнктов 1 и 7 с унификатором {f(x3 , y3) | x1, f(x3 , y3) | y3}получим резольвенту:¬P(y3 , f(x3 , y3))Наконец, для дизъюнктов 1 и 8 с унификатором {y3 | x1, f(x3 , y3) | y1} получаем.Таким образом формула ¬А не выводима, следовательно, праведливо исходноеутверждение.Рассмотрим несколько примеров применения метода резолюции к поиску ответов навопросы.
Разделим вопросы на четыре класса в зависимости от формы ответа:Класс А. Вопросы, требующие ответа "да " или " нет".Класс В. Вопросы, требующие в качестве ответа "где?", "кто?" или "при какихусловиях?".Класс С. Вопросы, требующие ответа в виде последовательности действий.Класс D. Вопросы, включающие проверку условий, например, имеющие конструкцию"ЕСЛИ <условие>,' ТО <действие>".1.2.3.4.5.Вопросы класса А.Пример.Аксиомы:Для всех x, y, z, если х и у - братья, а также у и z - братья, то х и z - братья.Борис и Кирилл - братья.Кирилл и Мефодий - братья.Мефодий и Глеб — братья.Доказать теоремуБорис и Глеб — братья.Запишем аксиомы на языке предикатов.
Пусть Р(х, у) означает "x и у - братья". Тогдапостановку задачи можно представить в форме предикатов:A1: P(x, y)^P(y, z)→P(x, z)≡¬[P(x, y)^P(y, z)]vP(x, z)≡¬P(x, y)v¬P(y, z)vP(x, z).A2: P(Б, К).A3: Р(К, М).A4: Р(М, Г).B5: Р(Б, Г).Представим аксиому в виде дизъюнктов, кроме того, теорему В5 , которую требуетсядоказать, необходимо взять с отрицанием.Д1: ¬Р(х, у) v ¬P(y, z) v P(x, z).Д2: Р(Б, К).Д3: Р(К, М).Д4: Р(М, Г).Д5: ¬Р(Б, Г).Вывод изобразим в виде дерева выводаРис.
2.5. Дерево выводаПоскольку получен пустой дизъюнкт , гипотеза Д5 неверна, и ответ следует "да", т.е.Борис и Глеб — братья.1.2.3.Вопросы класса В.Пример.Аксиомы:Миша повсюду ходит за Димой.Дима в школе.Доказать теорему:Где Миша?На языке предикатов:A1: ∀х(В(Дима,х)→В(Миша, х)).A2: В(Дима, школа).В3: ¬∃хВ(Миша, х) ≡ ∀х¬В(Миша, х).Аналогично рассмотренному в предыдущем примере имеем:Д1: ¬В(Дима, х)vB(Миша, x).Д2: В(Дима, школа).Д3: ¬В(Миша, х).Для получения ответа введем специальный дизъюнкт ОТВ, термы которого дублируюттермы предиката вопроса. С учётом сказанного дизъюнкт Д3 следовало бы заменить надизъюнкт Д3': ¬В(Миша, х)vОТВ(Миша, х).В этом и в последующих примерах будем пользоваться не графическим изображениемрезольвент, а записью их последовательности.(Д1 - Д2): Д4.
В(Миша, школа).(Д3'- Д4): Д5 . vOTB(Миша, школа), т.е. предикат ОТВ наследует смысл предикатавопроса и в данном случае читается как "Миша в школе".1.2.3.Пример.Аксиомы:Для всех х, у, и z, если х - отец у, z - отец х, то z - прародитель уКаждый человек имеет своего родителя.Вопрос:Для каждого х, кто является прародителем x?Формальная запись будет следующей:A1: ∀х, y, z(Р(х, у)^Р(z, х)→П(z, у).A2: ∀x∃v(P(v, x)).В3: ∀хП(u, х).Преобразуем аксиомы в дизъюнкты (взяв отрицание В3):Д1. ¬P(x, y)v¬P(z, x)vП(z, у).Д2. P(fC(x), x).Д3.
¬П(u, x)vOTB(u, x).Сколемовскую функцию fC, введенную при исключении квантора существования,можно интерпретировать как имя родителя каждого индивида, поэтому при выводе резольвентзаменой переменных подчеркнем изменение этого имени.Получение ответа :В дизъюнкте Д2 сделаем замену переменных v→x(Д2: P(fC(v), v). Тогда при сопоставлении дизъюнктов Д1 - Д2 для получениярезольвенты делаем подстановку z←fC(v), x←v.(Д1 - Д2 ): Д4. ¬Р(v, у)vП(fC(v), у)Теперь при сопоставлении дизъюнктов Д4 - Д2 для получения новой резольвентыделаем новую замену v в Д2 на q.(Д4 - Д2): Д5.
П(fC(fC(q)), q)(v←fC(q), y←q).C C(Д5 - Д3): Д6. v vOTB(f (f (q)), q)(x←q, u←fC(fC(q)))Полученный ответ можно интерпретировать следующим образом:«Для любого индивида (х) родитель родитель этого индивда х является егопрародителем».К сожалению, в каждом конкретном случае функция Сколема интерпретируется, исходяиз смысла вопроса и используемых в модели предикатов. Формализовать этот процесс сложно(если возможно вообще). В данном случае fC(х) - "быть родителем х".Вопросы класса С.Для вопросов этого типа задача состоит в нахождении последовательности действий,достигающей некоторой цели.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
