9. Полнота резолютивного вывода. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций (Лекции)

Математическая логикаЛектор:Подымов Владислав Васильевич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.