5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем (В.А. Захаров - Лекции), страница 3

Применим стратегию издоказательства теоремы полноты. Т. к. 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 , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаиболее критичный этап потроения табличного вывода —выбор нужного правила.

Это касается правил (L∀) и (R∃).L∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆iR∃hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}iпоскольку выбор терма t правилами не оговаривается. Простойперебор всех термов практически невозможен. (почему ? )АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМПотому что термов очень-очень много. Если есть одиндвухместный функциональный символ f (2) и две константыc1 , c2 , то с их помощью можно построить более 101000 основныхтермов высоты 10.

Это количество значительно превосходитчисло наносекунд, прошедших с момента Большого Взрыва.Значит, нужно придумать способ, позволяющий быстро и точновычислять тот терм, который нужно подставлять вместопеременных, связанных кванторами.Эту задачу в 1964 г. сумели решить Дж. Робинсон (методрезолюций) и С.

Маслов (обратный метод ε-термов).КОНЕЦ ЛЕКЦИИ 5..