Лекция 5. Полнота табличного вывода. Теорема Левенгейма-Сколема... (Лекции 2014), страница 2

т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,L0 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,L0 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4).

В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4).

В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }и.

т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАПредположим, что указанная стратегия не приводит кпостроению успешного вывода для невыполнимой таблицыT0 = h Γ0 | ∆0 i. Тогда в дереве вывода либо существуетбесконечная ветвь, не содержащая закрытых таблицT0 −→ T1 −→ T2 −→ . . . −→ Tn −→ Tn+1 −→ . .

.либо существует ветвь, оканчивающаяся незакрытой атомарнойтаблицейT0 −→ T1 −→ T2 −→ . . . −→ Tatom −→ Tatom −→ Tatom −→ . . .Будем полагать, что в последнем случае последовательностьтаблиц также бесконечна.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАНа основе бесконечной последовательности незакрытых таблицT0 , T1 , . .

. , Tn , Tn+1 , . . . , каждая из которых имеет видTn = h Γn | ∆n i построим три множества:∞S1). Γω =Γiмножество всех формул из левых частейтаблиц,∆iмножество всех формул из правых частейтаблиц,LTiмножество всех констант из списков констант, ассоциированных с таблицами избесконечной ветви.i=02). ∆ω =∞Si=03). Lω =∞Si=0Используя множества Γω , ∆ω , Lω , построим интерпретацию Iω ,в которой будет выполняться каждая таблицапоследовательности.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАIω = hDI , Const, PrediDI = Lωпредметная область состоит из всех константных символов,входящих в состав формул из Γω и ∆ω ,Const : Const → Lωзначением c каждой константы c (как символа из алфавита)является ее собственное изображение c ( как элементмножества Lω ), т.

е. c = c,Pred : Pred → (Lω n → {true, false})для каждого предикатного символа P (n) и набора элементовci1 , . . . , cin из LωP(ci1 , . . . , cin ) = true ⇐⇒ P(ci1 , . . . , cin ) ∈ Γω .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАПокажем, чтолюбая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ ∆ω , невыполнима в интерпретации Iω .Доказательство проведем при помощи индукции по числулогических операций (связок и кванторов) в формуле.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАБазис индукцииϕ, ψ — атомарные формулы.Во всех таблицах Ti содержатся только замкнутые формулы(почему ? ).Поэтому формулы ϕ, ψ имеют вид P(ci1 , . . . , cin ).Если ϕ ∈ Γω , то P(ci1 , .

. . , cin ) = true, и поэтому Iω |= ϕ.Если ψ ∈ ∆ω , то ψ 6∈ Γω (почему ? ).Значит, P(ci1 , . . . , cin ) = false, и поэтому Iω 6|= ψ.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходПредположим, что утверждение верно для всех формул,имеющих не более n связок и кванторов. Рассмотрим формулыϕ, ψ, содержащие n + 1 связку и квантор.Если ϕ = ϕ1 → ϕ2 ∈ Γω , то есть такая таблица Ti = hΓi |∆i i,что ϕ1 → ϕ2 ∈ Γi .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ϕ1 → ϕ2 — первая формула в списке формул Γj .Поэтому либо ϕ1 ∈ ∆j+1 , либо ϕ2 ∈ Γj+1 .В первом случае, согласно индуктивному предполжению,Iω 6|= ϕ1 , и поэтому Iω |= ϕ.Во втором случае, согласно индуктивному предполжению,Iω |= ϕ2 , и поэтому Iω |= ϕ.Итак, в обоих случаях получаем Iω |= ϕ1 → ϕ2 .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходАналогичные рассуждения применимы и для других связок.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ Γω , то формула ∀xϕ1 (x) бесконечно частовстречается в левых частях таблиц Ti = hΓi |∆i i (почему ? ).Поэтому правило (L∀) применяется к формуле ∀xϕ1 (x)бесконечно часто.Тогда, согласно описанию применяемой стратегии построениятабличного вывода, для любой константы c, c ∈ Lω ,существует такая таблица Tj = hΓj |∆j i, что ϕ1 (c) ∈ Γj .Значит, согласно индуктивному предполжению, Iω |= ϕ1 (c) длялюбой константы c, c ∈ Lω .Так как DI = Lω , приходим к заключению о том, чтоIω |= ∀xϕ1 (x).ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ ∆ω , то есть такая таблица Ti = hΓi |∆i i,что ∀xϕ1 (x) ∈ ∆i .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ∀xϕ1 (x) — первая формула в списке формул ∆j .Поэтому существует такая константа c, c ∈ Lω , чтоϕ1 (c) ∈ ∆j+1 .Согласно индуктивному предполжению, это означает, чтоIω 6|= ϕ1 (c), и поэтому Iω 6|= ∀xϕ1 (x).Аналогичные рассуждения применимы и для формул сквантором ∃.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТаким образом,любая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ ∆ω , невыполнима в интерпретации Iω .Поскольку, Γ0 ⊆ Γω и ∆0 ⊆ ∆ω , приходим к заключению о том,чтоIω |= Γ0 , Iω 6|= ∆0 .Это означает, что таблица T0 выполнима в интерпретации Iωвопреки условию о невыполнимости T0 .Источник полученного противоречия — предположение оневозможности построить успешный вывод, руководствуясьописанной стратегией.

Значит, предложенная стратегияпозволяет построить успешный вывод для всякойневыполнимой таблицы.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАЭто было упрощенное доказательство теоремы полноты.А насколько существенны те упрощения, которые былиобъявлены в начале доказательства? А именно,IКакие изменения нужно внести в структуру данных,представляющих таблицы, чтобы доказательство можнобыло распространить и на таблицы, содержащиебесконечные множества формул?IКакие изменения нужно внести в стратегию построениятабличного вывода, чтобы построить успешный вывод дляневыполнимой таблицы, формулы которой содержатсложные термы?IКакие изменения нужно внести в определениеинтерпретации Iω , чтобы доказательство можно былоприменить к таблицам, содержащим незамкнутыеформулы?ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема Геделя (о полноте)Если формула ϕ общезначима, то существует успешныйтабличный вывод для таблицу Tϕ = h∅|ϕi.ДоказательствоСледует из теоремы полноты.Итак, формула ϕ общезначима⇐⇒для таблицы Tϕ существует успешный вывод.И в доказательстве теоремы полноты показано, как построитьэтот вывод.ТЕОРЕМА ЛЕВЕНГЕЙМА-СКОЛЕМАТеоремаФормула ϕ выполнима ⇐⇒ ϕ имеет модель сконечной или счетно-бесконечной предметной областью.ДоказательствоЕсли ϕ выполнима, то для таблицы Tϕ∗ = hϕ|∅i нельзяпостроить успешный вывод.

Применим стратегию издоказательства теоремы полноты. Т. к. Tϕ∗ выполнима,получим дерево с ветвью, в которой нет закрытых таблиц.Tϕ∗ = T0 −→ T1 −→ T2 −→ . . . −→ Tn −→ Tn+1 −→ . . .Для этой ветви построим интерпретацию Iω , в которойIDi = Lω = {c1 , c2 , . . . } — конечное или счетно-бесконечноемножество констант из таблиц последовательности;Iвыполнимы все таблицы Ti (в т.ч. и Tϕ∗ ).ТЕОРЕМА КОМПАКТНОСТИ МАЛЬЦЕВАТеоремаΓ |= ϕ ⇐⇒существует такое конечное подмножество Γ0 , Γ0 ⊆ Γ, что Γ0 |= ϕ.Доказательство1. Γ |= ϕ ⇐⇒ таблица T = hΓ|ϕi невыполнима (почему? )2. Таблица T = hΓ|ϕi невыполнима ⇐⇒ cуществуетуспешный вывод для T (почему? )3.

успешный вывод — это конечное дерево, и поэтомусуществует лишь конечое множество формул Γ0 , Γ0 ⊆ Γ,к которым применяются правила вывода.4. Но тогда для таблицы T = hΓ0 |ϕi cуществует точно такойже успешный вывод.5. Значит, Γ0 |= ϕ.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМСтратегия построения табличного вывода, использованная вдоказательстве теоремы полноты — это алгоритм построениядоказательства истинности утверждений, выраженныхформулами логики предикатов.Автоматические системы построения доказательств(логических выводов) называются пруверами . От пруверовтребуются следующие качества:Iкорректность (абсолютно необходимо)Iполнота (очень-очень желательно)Iэффективность (желательно)Первый прувер (крайне неэффективный) был разработан в1957 в США (Newell, Simon, Show)АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМОбщая схема прувера'$'Формулы,Правилатаблицывывода,ϕ1'ϕknпрувера Π16%ΠNϕm-ϕ&ЯдроΠ2...-?&$%$&%АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаш прувер (табличный вывод) корректен и полон.

Нонасколько он эффективен?В алгоритме построения дерева табличного выводаприменяется двойной переборный поиск:Iвыбор формулы , к которой нужно применить правиловвода,Iвыбор правила , которое нужно применять к формуле.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));Бузину посадил киевлянин.∀x(Посадил(x, бузина) →Живет(x, Киев));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаиболее критичный этап потроения табличного вывода —выбор нужного правила.