9. Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций (1131924)
Текст из файла
Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 9Полнота резолютивного выводаСтратегии резолютивного выводаВычислительные возможностиметода резолюцийПолнота резолютивного выводаТеорема полноты резолютивного выводаИз любой противоречивой системы дизъюнктоврезолютивно выводим пустой дизъюнктСхема доказательства:Iрассмотрим конечное противоречивое множество Gосновных примеров дизъюнктов исходной системы S(теорема Эрбрана)Iпокажем, что из G резолютивно выводим (лемма об основных дизъюнктах)Iпо выводу из G построим вывод из S(лемма о подъёме)Полнота резолютивного выводаЛемма об основных дизъюнктахИз любой конечной противоречивой системы основныхдизъюнктов резолютивно выводим пустой дизъюнктДоказательство леммы.Покажем выводимость из противоречивой системы Sиндукцией по числу kSk различных атомов, содержащихся вдизъюнктах SБаза индукции: kSk = 0Система S противоречива ⇒ S 6= ∅ ⇒ S = {}Индуктивный переход: kSk = N > 0Рассмотрим атом A, содержащийся в дизъюнктах SУдалим из S все дизъюнкты вида D ∨ A ∨ ¬A и склеимповторяющиеся литеры A, ¬A в каждом дизъюнктеПолученная система S red противоречива, и если выводим изS red , то выводим и из S(очевидно?)redЕсли kS k < N, то индуктивный переход доказанПолнота резолютивного выводаДоказательство леммы.Индуктивный переход: S red противоречива; kS red k = N > 0Разобьём S red на три подсистемы:1.
S+ = D | D ∈ S red , D = D 0 ∨ A2. S− = D | D ∈ S red , D = D 0 ∨ ¬A3. S× = S red \ (S+ ∪ S− )Построим все резольвенты по контрарной паре A, ¬A:Sr = {D1 ∨ D2 | D1 ∨ A ∈ S+ , D2 ∨ ¬A ∈ S− }S+S−S×kS red k = NS red : D ∨ A D ∨ ¬A12нет ASr ∪ S× :SrD1 ∨ D2S×нет AkSr ∪ S× k = N − 1Если выводим из Sr ∪ S× , то выводим и из S red , а значит,достаточно показать, что Sr ∪ S× — противоречивая системаПолнота резолютивного выводаДоказательство леммы.Индуктивный переход: S red противоречива; kS red k = N > 0S+S−S×D : I 6|= DD ∨ASrS×D : I 6|= DРассмотрим произвольную интерпретацию IПокажем, что I 6|= Sr ∪ S×Теорема об H-интерпретациях: без ограничения общностисчитаем, что I — H-интерпретацияПоложим I |= A(для I 6|= A всё аналогично)I 6|= S+ ∪ S− ∪ S× и I |= S+ ⇒ I 6|= S− ∪ S×Случай 1: I 6|= S×ОчевидноПолнота резолютивного выводаДоказательство леммы.Индуктивный переход: S red противоречива; kS red k = N > 0S+S−S×D1 ∨ AD2 ∨ ¬Aнет ASrS×D1 ∨ D2Случай 2: I |= A, I |= S× и I 6|= S−I 6|= D2 ∨ ¬A ⇒ I 6|= D2Рассмотрим H-интерпретацию J = I \ {A}J 6|= S+ ∪ S− ∪ S× , J |= S− и J |= S× ⇒ J 6|= S+J 6|= D1 ∨ A ⇒ J 6|= D1 ⇒ I 6|= D1I 6|= D1 , I 6|= D2 ⇒ I 6|= D1 ∨ D2HПолнота резолютивного выводаЛемма о подъёме для правила резолюцииПусть:I D1 , D2 — дизъюнкты, и VarD ∩ VarD = ∅12I D 0 , D 0 — основные примеры дизъюнктов D1 и D212соответственноI D 0 — резольвента дизъюнктов D 0 , D 012Тогда существует резольвента D дизъюнктов D1 , D2 ,примером которой является дизъюнкт D 0Где здесь “подъём”? Это подъём от частного случая к общемуD1θ1D10D2Dθ2θD0D20Полнота резолютивного выводаДоказательство леммы.D1D2θ1θ2D10D20D0Полнота резолютивного выводаДоказательство леммы.D1D2θ1D100 ∨ Lθ2D100∨D200D200 ∨ ¬LВыделим контрарную пару, по которой строилась резольвентаосновных дизъюнктовПолнота резолютивного выводаДоказательство леммы.D1000 ∨ L1D2000 ∨ ¬L2θ1D1000 θ1 ∨ L1 θ1θ2D1000 θ1∨D2000 θ2D2000 θ2 ∨ ¬L2 θ2Выделим контрарную пару, по которой строилась резольвентаосновных дизъюнктов, и литеры дизъюнктов D1 , D2 ,порождающие эту паруБез ограничения общности полагаем, что Domθ1 ∩ Domθ2 = ∅Полнота резолютивного выводаДоказательство леммы.D1000 ∨ L1D2000 ∨ ¬L2ηD1000 η ∨ L1 ηηD1000 η∨D2000 ηD2000 η ∨ ¬L2 ηВыделим контрарную пару, по которой строилась резольвентаосновных дизъюнктов, и литеры дизъюнктов D1 , D2 ,порождающие эту паруБез ограничения общности полагаем, что Domθ1 ∩ Domθ2 = ∅Тогда подстановка η = θ1 ∪ θ2 — унификатор атомов L1 , L2Полнота резолютивного выводаДоказательство леммы.D1000 ∨ L1D2000 ∨ ¬L2ηD1000 η ∨ L1 ηηD1000 η∨D2000 ηD2000 η ∨ ¬L2 ηТеорема об унификации:существует наиболее общий унификатор µ атомов L1 , L2Полнота резолютивного выводаДоказательство леммы.D1000 ∨ L1ηD1000 η ∨ L1 ηD1000 µ ∨ D2000 µD1000 η∨D2000 ηD2000 ∨ ¬L2ηD2000 η ∨ ¬L2 ηТеорема об унификации:существует наиболее общий унификатор µ атомов L1 , L2Тогда:ID1000 µ ∨ D2000 µ — резольвента дизъюнктов D1 , D2 поконтрарной паре L1 , ¬L2Полнота резолютивного выводаДоказательство леммы.D1000 ∨ L1µθD1000 µθ ∨ L1 µθD1000 µ ∨ D2000 µθ(D1000 µ∨D2000 µ)θD2000 ∨ ¬L2µθD2000 µθ ∨ ¬L2 µθТеорема об унификации:существует наиболее общий унификатор µ атомов L1 , L2Тогда:IID1000 µ ∨ D2000 µ — резольвента дизъюнктов D1 , D2 поконтрарной паре L1 , ¬L2существует подстановка θ, такая что η = µθHПолнота резолютивного выводаЛемма о подъёме для правила склейкиПусть:I D 0 — основной пример дизъюнкта D11I D 0 — склейка дизъюнкта D 01Тогда существует склейка дизъюнкта D1 , основнымпримером которой является дизъюнкт D 0Доказательство леммы.Доказывается аналогично лемме о подъёме для правиларезолюцииПолнота резолютивного выводаТеорема полноты резолютивного выводаИз любой противоречивой системы дизъюнктоврезолютивно выводим пустой дизъюнктДоказательство теоремы.Пусть S — противоречивая система дизъюнктовТеорема Эрбрана: существует конечное противоречивоемножество G основных примеров дизъюнктов из SЛемма об основных дизъюнктах: из G резолютивно выводимпустой дизъюнктДве леммы о подъёме: из S резолютивно выводим пустойдизъюнктHСтратегии резолютивного выводаА если система противоречива и дизъюнкты выводятся из неёпроизвольно, то обязательно ли будет выведен ?Нет, например: вариантам)(опускаем переход от дизъюнктов к ихR(a,b)(F)(R) Q(x, x)¬Q(x, y) ∨ ¬Q(y, z) ∨ Q(x, z) (T)(L) ¬R(x,y) ∨ Q(x, y)¬Q(a, b)Резолютивный вывод из этой системы может выглядеть так:¬Q(a, b)L¬R(a, b)FСтратегии резолютивного выводаА если система противоречива и дизъюнкты выводятся из неёпроизвольно, то обязательно ли будет выведен ?Нет, например: вариантам)(опускаем переход от дизъюнктов к ихR(a,b)(F)(R) Q(x, x)¬Q(x, y) ∨ ¬Q(y, z) ∨ Q(x, z) (T)(L) ¬R(x,y) ∨ Q(x, y)¬Q(a, b)Резолютивный вывод из этой системы может выглядеть так:¬Q(a, b)T¬Q(a, y) ∨ ¬Q(y, b)¬Q(a, b)∞RСтратегии резолютивного выводаА если система противоречива и дизъюнкты выводятся из неёпроизвольно, то обязательно ли будет выведен ?Нет, например: вариантам)(опускаем переход от дизъюнктов к ихR(a,b)(F)(R) Q(x, x)¬Q(x, y) ∨ ¬Q(y, z) ∨ Q(x, z) (T)(L) ¬R(x,y) ∨ Q(x, y)¬Q(a, b)Резолютивный вывод из этой системы может выглядеть так:¬Q(x, y) ∨ ¬Q(y, z) ∨ Q(x, z)RT¬Q(x, y) ∨ ¬Q(y, z)∨¬Q(x, y) ∨ ¬Q(y, x)¬Q(x, y0 ) ∨ ¬Q(y0 , z) ∨ Q(x, z)¬Q(x, y) ∨ ¬Q(y, z) ∨ ¬Q(x, y0 ) ∨ ¬Q(y0 , z) ∨ ¬Q(z, x)∞Стратегии резолютивного выводаОт способа применения правил резолютивного выводасущественно зависит возможность вывести Стратегия резолютивного вывода — это набор правил, согласнокоторым должны применяться правила резолюции и склейкипри построении резолютивного выводаСтратегия резолютивного вывода полна, если для любойпротиворечивой системы дизъюнктов существует успешныйрезолютивный вывод, построенный по этой стратегииА какие бывают стратегии вывода?Какие из них полные, а какие нет?И зачем использовать неполные стратегии вывода?Стратегии резолютивного выводаСемантическая резолюцияРассмотрим систему дизъюнктов S и интерпретацию IРазобьём S на две части, и будем их пополнять новымидизъюнктами при построении вывода:S+I = {D | I |= D},S−I = {D | I 6|= D}Правило I-резолюции — это правило резолюции, применённое кодному дизъюнкту из S+I и одному дизъюнкту из S−II-резолютивный вывод — это резолютивный вывод, в которомIIправило резолюции заменено на правило I-резолюцииправило вывода не применяется дважды к одномудизъюнкту (склейка) и к одной паре дизъюнктов(резолюция)Стратегии резолютивного выводаПример I-резолютивного выводаРассмотрим систему S = {¬A ∨ ¬B ∨ C , A ∨ C , B ∨ C , ¬C }и H-интерпретацию I = ∅Тогда в I-резолютивном выводе могут появиться такиедизъюнкты:(склейка опущена)S+I : D1 = ¬A ∨ ¬B ∨ CD2 = ¬CD5 = D1 + D3 = ¬B ∨ CD6 = D1 + D4 = ¬A ∨ CS−I : D3 = A ∨ CD4 = B ∨ CD7 = D2 + D3 = AD8 = D2 + D4 = BD9 = D5 + D8 = C = D9 + D2Стратегии резолютивного выводаТеорема полноты I-резолютивного выводаI-резолютивный вывод полон для любойинтерпретации IДоказательство.Похоже на доказательство полноты резолютивного выводаHСтратегии резолютивного выводаВходная резолюцияРассмотрим систему дизъюнктов SВыберем в системе S дизъюнкт D0Будем строить резолютивный вывод так:IIначнём с варианта дизъюнкта D0на каждом шаге построения будем добавлять в выводрезольвенту Di+1 последнего полученного дизъюнкта Di икакого-либо дизъюнкту из SВ результате будет построен входной резолютивный вывод,инициированный дизъюнктом D0Входной резолютивный вывод не является полным (очевидно?)Стратегии резолютивного выводаПример входного резолютивного выводаS = {¬A ∨ ¬B ∨ C , A ∨ C , B ∨ C , ¬C }Входной резолютивный вывод из S, инициированныйдизъюнктом ¬C , может выглядеть так:¬C¬A ∨ ¬B ∨ C¬A ∨ ¬BA∨C¬B ∨ C¬C¬BB ∨CC¬CВычислительные возможностиметода резолюцийДля решения каких задач пригоден метод резолюций?I.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
