8. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций. Эрбрановские интерпретации. Теорема Эрбрана (Лекции)

Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 8Резолютивный выводКорректность резолютивного выводаПрименение метода резолюцийЭрбрановские интерпретацииТеорема ЭрбранаОбщая схема метода резолюцийисходная формулаϕотрицаниеψ = ¬ϕССФψssfПНФψpnfсистема дизъюнктовSϕрезолютивный выводпустого дизъюнкта из SϕОбщая схема метода резолюцийисходная формулаϕотрицаниеψ = ¬ϕССФψssfПНФψpnfсистема дизъюнктовSϕрезолютивный выводпустого дизъюнкта из SϕРезолютивный выводЕщё немного определенийПоложительная литера — это атомОтрицательная литера — это отрицание атомаПусть E — логическое выражение и θ — подстановкаТогдаIE θ — пример выражения EIесли VarE θ = ∅, то E θ — основной примерIесли θ : Var → Var — биекция, тоIθ — переименованиеIE θ — вариант выражения EРезолютивный выводПримерРассмотрим выражение E = P(x, f(y)) ∨ ¬R(y, c)и подстановкиθ = {x/u, y/z, u/x, z/y}η = {x/g(d), y/z}µ = {z/c}ε = {}Тогда:IIIIE η = P(g(d), f(z)) ∨ ¬R(z, c) — пример выражения EE ηµ = P(g(d), f(c)) ∨ ¬R(c, c) — основной примервыражения Eподстановки θ и ε — переименованияE θ = P(u, f(z)) ∨ ¬R(z, c) — вариант выражения EРезолютивный выводПравило резолюции:D1 ∨ L1 , D2 ∨ ¬L2(D1 ∨ D2 )θЗдесьIIID1 , D2 — дизъюнктыL1 , L2 — положительные литерыθ ∈ НОУ(L1 , L2 )Дизъюнкт (D1 ∨ D2 )θ — резольвентадизъюнктов D1 ∨ L1 , D2 ∨ ¬L2Литеры L1 , ¬L2 образуют контрарную паруРезолютивный выводПримерконтрарная параP(x, f(y)) ∨ ¬R(g(x, z), f(z))Q(x) ∨ R(y, x) ∨ ¬P(g(z, y), z)¬R(g(g(f(y), y), f(y)), f(f(y))) ∨ Q(g(f(y), y)) ∨ R(y, g(f(y), y))резольвентаθ = {x/g(f(y), y), z/f(y)} ∈ НОУ(P(x, f(y)), P(g(z, y), z))резольвента: (¬R(g(x, z), f(z)) ∨ Q(x) ∨ R(y, x))θРезолютивный выводПримерконтрарная параP(x, f(y)) ∨ ¬R(g(x, z), f(z))Q(x) ∨ R(y, x) ∨ ¬P(g(z, y), z)P(f(z), f(g(f(z), z))) ∨ Q(f(z)) ∨ ¬P(g(z, g(f(z), z)), z)резольвентаθ = {x/f(z), y/g(f(z), z)} ∈ НОУ(R(g(x, z), f(z)), R(y, x))резольвента: (P(x, f(y)) ∨ Q(x) ∨ ¬P(g(z, y), z))θРезолютивный выводПримерконтрарная параP(f(x), y)¬P(u, g(v))θ = {y/g(v), u/f(x)} ∈ НОУ(P(f(x), y), P(u, g(v)))резольвента: (???)θРезолютивный выводПримерконтрарная пара¬P(u, g(v)) ∨ falsefalse ∨ P(f(x), y)резольвентаθ = {y/g(v), u/f(x)} ∈ НОУ(P(f(x), y), P(u, g(v)))резольвента: (false ∨ false)θРезолютивный выводДостаточно ли правила резолюции для выявления всехпротиворечий?Оказывается, что нет.

Например:P(x) ∨ P(c)¬P(c) ∨ ¬P(y)Система из таких двух дизъюнктов противоречива, но поправилу резолюции из них всегда будут получаться дизъюнктыровно с двумя литерамиНеобходимо иметь правило, которое позволяет работать и стакими системами дизъюнктовРезолютивный выводПравило склейкиD ∨ L1 ∨ L2(D ∨ L1 )θЗдесьIIID — дизъюнктL1 , L2 — литерыθ ∈ НОУ(L1 , L2 )Дизъюнкт (D ∨ L1 )θ — склейка дизъюнкта D ∨ L1 ∨ L2Литеры L1 , L2 образуют склеиваемую паруРезолютивный выводПримерсклеиваемая параP(x)∨¬R(y, z, f(x))∨¬R(x, f(c), z)P(c) ∨ ¬R(c, f(c), f(c))склейкаθ = {x/c, y/c, z/f(c)} ∈ НОУ(¬R(y, z, f(x)), ¬R(x, f(c), z))склейка: (P(x) ∨ ¬R(y, z, f(x)))θРезолютивный выводПусть S — система дизъюнктовРезолютивный вывод из S — это конечная последовательностьдизъюнктовD1 , .

. . , Di , . . . , Dk ,такая что каждый дизъюнкт Di являетсяIIIвариантом дизъюнкта из S,склейкой дизъюнкта Dj , где j < i, илирезольвентой дизъюнктов Dj , Dm , где j < i и m < iДизъюнкт резолютивно выводим из S, если существуетрезолютивный вывод из S, оканчивающийся этим дизъюнктомРезолютивный выводПримерS = {D1 , D2 , D3 }, гдеD1 = P(x, f(y)) ∨ R(y)D2 = ¬R(y)D3 = ¬P(f(x), z) ∨ ¬P(y, y)Резолютивный вывод:вариант P(x1 , f(y1 )) ∨ R(y1 )вариантрезольвентавариантсклейкарезольвента¬R(y2 )P(x3 , f(y3 ))¬P(f(x4 ), z4 ) ∨ ¬P(y4 , y4 )¬P(f(x5 ), f(x5 ))Пустой дизъюнкт резолютивно выводим из системы SРезолютивный выводНасколько важно иметь возможность использоватьварианты дизъюнктов, а не только с сами дизъюнкты?Рассмотрим такую систему:S = {¬P(x), P(f(x))}НОУ(P(x), P(f(x))) = ∅Значит, у этих дизъюнктов нет ни одной резольвентыПри этом система S противоречива:у формул ∀x ¬P(x) и ∀x P(f(x)) нет общих моделейК вариантам дизъюнктов из S применимо правило резолюции:НОУ(P(x1 ), P(f(x2 ))) 6= ∅А на каком основании переменные можно переименовывать?∀x ϕ ≈ ∀y (ϕ {x/y}), если <...>Резолютивный выводРезолютивный вывод успешен (является резолютивнымопровержением), если он оканчивается пустым дизъюнктом А в чём успешность такого вывода?И что в нём опровергается?Каждый шаг построения вывода можно трактовать так:IIпредположим, что система, полученная из исходнойдобавлением всех выведенных дизъюнктов, выполниматогда система останется выполнимой, если к ней добавитьтакой дизъюнкт: <...>Выводимость опровергает предположение о выполнимостиисходной системы и этим успешно доказывает еёневыполнимостьНо это ещё нужно обосноватьКорректность резолютивного выводаТеорема корректности резолютивного выводаЕсли из системы дизъюнктов S резолютивно выводимпустой дизъюнкт, то S — противоречивая системаДоказательство теоремы.Если S |= , то система S противоречива,так как дизъюнкт не имеет моделиПокажем, что любой дизъюнкт, резолютивно выводимый из S,является логическим следствием SДостаточно доказать следующее:IIIвариант дизъюнкта D логически следует из D(это очевидно)резольвента дизъюнктов D1 и D2логически следует из D1 , D2склейка дизъюнкта D логически следует из DКорректность резолютивного выводаЛемма корректности правила резолюцииЕсли D — резольвента дизъюнктов D1 , D2 , то D1 , D2 |= DДоказательство леммы.(кванторные приставки опущены)Пусть D1 = D10 ∨ L1 , D2 = D20 ∨ ¬L2 , θ ∈ НОУ(L1 , L2 ),D = (D10 ∨ D20 )θ и L1 θ = L2 θ = LТогда будет верно:D1|= D1 θD1|= D10 θ ∨ L1 θD1|= D10 θ ∨ LD1 , D2 |= D10 θ ∨ LD1 , D2 |= D10 θ ∨ D20 θ ∨ LD2D2D2D1 , D2D1 , D2|= D2 θ|= D20 θ ∨ ¬L2 θ|= D20 θ ∨ ¬L|= D20 θ ∨ ¬L|= D10 θ ∨ D20 θ ∨ ¬LЗаметим, что(очевидно?)если Γ |= A ∨ B и Γ |= A ∨ ¬B, то Γ |= AТогда D1 , D2 |= D10 θ ∨ D20 θТо есть D1 , D2 |= DHКорректность резолютивного выводаЛемма корректности правила склейкиЕсли D — склейка дизъюнкта D1 , то D1 |= DДоказательство леммы.Похоже на доказательство корректности правила резолюции(то есть очевидно)HHПрименение метода резолюцийВспомним, для чего вводился резолютивный выводРассмотрим такую формулу:ϕ : ∃x (P(x) &(∀x P(x) → ∃y R(x, y)) → ∃y R(x, y))Задача: проверить общезначимость ϕ|= ϕ ?Покажем, как эта задача решается с помощьюметода резолюцийПрименение метода резолюцийРешениеЭтап 1.

Перейти к проверке противоречивости отрицания ψ = ¬ϕ¬∃x (P(x) &(∀x P(x) → ∃y R(x, y)) → ∃y R(x, y))Этап 2. Построить равносильнуюпредварённую нормальную форму ψpnf∀x ∃z ∃y ∀u (P(x) &(¬P(z) ∨ R(x, y)) & ¬R(x, u))Этап 3. Построить равновыполнимуюсколемовскую стандартную форму ψssf∀x ∀u (P(x) &(¬P(f(x)) ∨ R(x, g(x))) & ¬R(x, u))Этап 4. Перейти к проверке противоречивости системы SϕP(x)¬P(f(x)) ∨ R(x, g(x))¬R(x, u)Применение метода резолюцийРешениеЭтап 5.

Резолютивно вывести пустой дизъюнкт из SϕP(x)¬P(f(x)) ∨ R(x, g(x))¬R(x, u)вариант¬P(f(x1 )) ∨ R(x1 , g(x1 ))вариантP(x2 )резольвентавариантрезольвентаR(x3 , g(x3 ))¬R(x4 , u4 )Применение метода резолюцийРешениеКакой ответ и на каком основании мы получили?Нами построендизъюнкта из SϕуспешныйрезолютивныйвыводпустогоТеорема корректности резолютивного вывода:система Sϕ противоречиваБезымянная теорема в лекции 6: ССФ ψssf противоречиваТеорема о сколемизации: ПНФ ψpnf противоречиваТеорема о предварённой нормальной форме:формула ψ противоречиваψ = ¬ϕ: формула ϕ общезначимаПрименение метода резолюцийВсё ли это, что следует знать про метод резолюций?Для метода семантических таблиц были исследованыIIкорректность: верно ли, что наличие успешного выводаозначает общезначимость формулыполнота: верно ли, что для любой общезначимой формулыможно построить успешный выводА полон ли метод резолюций?Построить систему дизъюнктов Sϕ можно (очевидно) длялюбой формулы ϕА верно ли, что из любой противоречивой системы дизъюнктоврезолютивно выводим пустой дизъюнкт?Эрбрановские интерпретацииЧто означает противоречивость системы дизъюнктов S?Для любой интерпретации I существуют дизъюнкт∀exn (L1 ∨ · · · ∨ Lm ) из S и набор предметов den , такие чтоI 6|= L1 [den ],...,I 6|= Lm [den ]А так ли необходимо перебирать все интерпретации и предметыдля проверки противоречивости S?Например, для доказательства невыполнимости системы{P(x), ¬P(f(c))} достаточно заметить, что независимо отвыбора интерпретации Iлибо I 6|= P(x)[f(c)],либо I 6|= ¬P(f(c))Пытаясь рассуждать о предметах, не отталкиваясь от ихприроды и используя только термальное представление, мынеизбежно приходим к эрбрановским интерпретациямЭрбрановские интерпретацииВ основе эрбрановских интерпретаций лежатсвободные алгебры термов1Эрбрановская интерпретация IH = Hσ , ConstH , FuncH , Predсигнатуры σ = hConst, Func, Predi состоит изIстандартной предметной области Hσ :эрбрановского универсума (или H-универсума)IHσ — это множество всех основных термов2 сигнатурыII12σ, если Const 6= ∅h{c}, Func, Predi, если Const = ∅(c — эрбрановская константа)Думали увидеть это название в лекции 7 и навсегда забыть —но не тут-то было!Лекция 3: это термы, не содержащие переменныхЭрбрановские интерпретацииВ основе эрбрановских интерпретаций лежатсвободные алгебры термовЭрбрановская интерпретация IH = Hσ , ConstH , FuncH , Predсигнатуры σ = hConst, Func, Predi состоит изIстандартной оценки констант ConstH :II(c ∈ Const)стандартной оценки функциональных символов FuncH :IIc=cf(t1 , .

. . , tn ) = f(t1 , . . . , tn )(f ∈ Func; t1 , . . . , tn ∈ Hσ )произвольной оценки предикатных символов PredЭрбрановские интерпретацииЧем хороши H-интерпретации?IОни отличаются только оценкой предикатных символов,то есть можно не задумываться о заданииIпредметной области:Iоценки констант и функциональных символов:IIIэто H-универсумзначение основного терма — это сам термЧто более важно: для выяснения того, противоречива лисистема дизъюнктов, достаточно проверить еёвыполнимость только в эрбрановских интерпретацияхЭрбрановские интерпретацииТеорема об H-интерпретацияхСистема дизъюнктов выполнима тогда и только тогда,когда она имеет эрбрановскую модельДоказательство.(⇐): очевидно(⇒): Пусть S — выполнимая система дизъюнктови I = DI , Const, Func, Pred — её модель (сигнатуры σ)Дополним интерпретацию I оценкой эрбрановской константы,если в выбранной сигнатуре алфавита нет константРассмотрим такое отображение α : Hσ → DI :α(t) — значение основного терма t в интерпретации IПокажем, что модельюD для S будет такая эрбрановскаяEинтерпретация IH = Hσ , ConstH , FuncH , Pred :P(t1 , .