Ещё одни лекции В.А. Захарова (1158033), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

табл.атом. табл.?yT4закр. табл.ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод будем называть успешным (или табличнымопровержением ), если дерево вывода — конечное, и все листьядерева — закрытые таблицы.Существование успешного вывода означает, что корневаясемантическая таблица T0 невыполнима.Если T0 = ∅ | ϕ , то это означает, что |= ϕ.T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) (L∀)?T4 = ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) (L∀)?T4 = ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) (L∀)?T5 = ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) (L∀)?T4 = ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) (L∀)?T5 = ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) PPPP(L →))qPT6 = ∀x(P(x) → B(x)), |B(c) T7 = ∀x(P(x) → B(x)), |B(c), P(c)∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) (L∀)?T4 = ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) (L∀)?T5 = ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) PPPP(L →))qPT6 = ∀x(P(x) → B(x)), |B(c) T7 = ∀x(P(x) → B(x)), |B(c), P(c)∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) (R →)?T1 = ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) (R →)?T2 = ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) (R∀)?T3 = ∀x(P(x) → B(x)), ∀xP(x) | B(c) (L∀)?T4 = ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) (L∀)?T5 = ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) PPPP(L →))qPT6 = ∀x(P(x) → B(x)), |B(c) T7 = ∀x(P(x) → B(x)), |B(c), P(c)∀xP(x), B(c), P(c)∀xP(x), P(c)закрытая таблицазакрытая таблицаT0 = ∅ | ∃x(P(x) → ∀xP(x) T0 = ∅ | ∃x(P(x) → ∀xP(x) (R →)?T1 = ∃xP(x) | ∀xP(x) T0 = ∅ | ∃x(P(x) → ∀xP(x) (R →)?T1 = ∃xP(x) | ∀xP(x) (L∃)?T2 = P(c1 ) | ∀xP(x) T0 = ∅ | ∃x(P(x) → ∀xP(x) (R →)?T1 = ∃xP(x) | ∀xP(x) (L∃)?T2 = P(c1 ) | ∀xP(x) (R∀)?T3 = P(c1 ) | P(c2 ) T0 = ∅ | ∃x(P(x) → ∀xP(x) (R →)?T1 = ∃xP(x) | ∀xP(x) (L∃)?T2 = P(c1 ) | ∀xP(x) (R∀)?T3 = P(c1 ) | P(c2 ) атомарная таблицаT0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) (L∀)?T2 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) (L∀)?T2 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) (R∃)?T3 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) (L∀)?T2 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) (R∃)?T3 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) (L∃)?T4 = ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) (L∀)?T2 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) (R∃)?T3 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) (L∃)?T4 = ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) (R∀)?T5 = ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) T0 = ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) (R →)?T1 = ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) (L∀)?T2 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) (R∃)?T3 = ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) (L∃)?T4 = ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) (R∀)?T5 = ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) ?∞КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАЛемма о корректности правил выводаКаково бы ни было правило табличного выводаL&, R&, L∨, R∨, L →, R →, L¬, R¬, L∀, R∀, L∃, R∃T0 ,T1 , (T2 )таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1 (или выполнима таблица T2 ).КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыΓ, ϕ → ψ|Δ.Γ, ψ|Δ, Γ|ϕ, ΔТаблица Γ, ϕ → ψ|Δ выполнима ⇐⇒существует интерпретация I и набор d̄ = d1 , .

. . , dn значенийсвободных переменных, для которых⎧⎧⎨ I |= Γ[d̄],⎨ I |= Γ[d̄],⇐⇒⇐⇒I |= Δ[d̄],I |= Δ[d̄],⎩⎩I |= (ϕ → ψ)[d̄]I |= ψ[d̄] или I |= ϕ[d̄]Рассмотрим правило⇐⇒⎧⎨ I |= Γ[d̄],I |= Δ[d̄],⎩I |= ψ[d̄]L →:⎧⎨ I |= Γ[d̄],илиI |= Δ[d̄],⎩I |= ϕ[d̄]⇐⇒одна из таблиц T1 = Γ, ψ|Δ или T2 = Γ|ϕ, Δ выполнима.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыАналогично доказывается корректность остальных 7 правилдля логических связокКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыΓ, ∀x0 ϕ(x0 )|Δ.Γ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|ΔТаблица Γ, ∀x0 ϕ(x0 )|Δ выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . .

. , dn значений свободныхпеременных, для которых⎧⎨ I |= Γ[d1 , . . . , dn ],I |= Δ[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. Тогда⎩I |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , .

. . , dn ].Следовательно, таблица Γ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|Δвыполнима в интерпретации I .На каком этапе доказательства существенно используется тотфакт, что переменная x0 свободна для терма t в формуле ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыΓ, ∃xϕ(x)|Δ.Γ, ϕ(x){x/c}|ΔОчевидно, что выполнимость таблицы Γ, ϕ(x){x/c}|Δ влечетвыполнимость таблицы Γ, ∃xϕ(x)|ΔРассмотрим правилоL∃:Допустим, что выполнима таблица Γ, ∃xϕ(x)|Δ. Тогдасуществует интерпретация I и набор d1 , .

. . , dn значенийсвободных переменных, для которых⎧⎨ I |= Γ[d1 , . . . , dn ],I |= Δ[d1 , . . . , dn ],⎩I |= (∃xϕ)[d1 , . . . , dn ]Выполнимость ∃xϕ[d1 , . . . , dn ] означает, что существует такойэлемент d0 ∈ DI , что I |= ϕ[d0 , d1 , . . . , dn ].КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим интерпретацию J, которая отличается от I , толькотем, что в J константа c имеет другое значение, а именноc̄ = d0 .Тогда J |= (ϕ{x/c})[d1 , .

. . , dn ].Кроме того, J |= Γ[d1 , . . . , dn ] и J |= Δ[d1 , . . . , dn ].Следовательно, таблица Γ, ϕ(x){x/c}|Δ выполнима винтерпретации J.На каком этапе доказательства существенно используется тотфакт, что константа c не входит в состав формул из Γ, Δ иформулы ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАТеорема корректности табличного выводаЕсли для семантической таблицы T0 существуетуспешный табличный вывод, то таблица T0невыполнима.ДоказательствоСледует изопределения табличного вывода,леммы о корректности правил табличного вывода,и утверждения о невыполнимости закрытых таблиц.СледствиеЕсли для таблицы Tϕ = ∅ |ϕ можно построить успешныйтабличный вывод, то |= ϕ.КОНЕЦ ЛЕКЦИИ 4.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 5.Полнота табличного вывода.Теорема Левенгейма-Сколема.Теорема компактности Мальцева.Автоматическое доказательствотеорем.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема полноты табличного выводаЕсли семантическая таблица T0 невыполнима, то для T0существует успешный табличный вывод.Доказательство.Проведем для упрощенного частного случая таблицы T0 , вкоторойимеется лишь конечное число формул,все формулы замкнутые,в формулах нет функциональных символов.Пусть T0 = Γ0 | Δ0 — невыполнимая таблица. Будемстроить табличный вывод для T0 , руководствуясь следующейстратегией.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).

Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty1yT0@@@R yT@2ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0@@@R yT@2Ty3Ty1@@@R yT@4ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).

Характеристики

Список файлов лекций