Лекции В.А. Захарова, страница 11
Описание файла
PDF-файл из архива "Лекции В.А. Захарова", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 11 страницы из PDF
. , DN } противоречива⇐⇒существует конечное противоречивое множество G 0основных примеров дизъюнктов системы S.В чем состоит главная особенность теоремы Эрбрана?Основной пример дизъюнкта не содержит предметныхпеременных, и поэтому является простой булевой формулойТаким образом проблема общезначимости формул логикипредикатов (сложная проблема!!!) сводится к проблемевыполнимости булевой формулы (простой проблеме??!!).ТЕОРЕМА ЭРБРАНАМаленькое лукавство.Увы, теорема Эрбрана не сообщает нам ничего о том, КАКИЕосновные примеры дизъюнктов образуют это противоречивоемножество G 0 .Нам нужно придумать механизм поиска этого противоречивогомножества G 0 .Дэвис и Патнем предложили использовать компьютер дляперебора всех эрбрановских интерпретаций в поискепротиворечивой системы основных примеров дизъюнктов.
НоДж. Робинсон поступил хитрее...Из дизъюнктов системы S нужно устранять потенциальныепротиворечия, пока не будут устранены все источникипротиворечия или не будет получено неустранимое (явное)противоречие.ТЕОРЕМА ЭРБРАНАЕсли в системе S содержатся дизъюнкты D1 = L и D2 = ¬L,то, очевидно, S противоречива (явное противоречие).А если в S есть дизъюнкты D1 = D10 ∨ L и D2 = D20 ∨ ¬L, тоI |= D1 и I |= D2 влечет I |= D10 ∨ D20 . Значит, добавлениедизъюнкта D0 = D10 ∨ D20 к S не нарушает ее выполнимости.Зато устраняется потенциальное противоречие L и ¬L.Правило вывода, разрешающее противоречия,D10 ∨ L, D20 ∨ ¬LD10 ∨ D20называется правилом резолюции . Это правило можноприменять до тех пор, пока не возникнет неустранимоепротиворечие D1 = L и D2 = ¬L. Это и будет служитьпризнаком противоречивости системы S.ТЕОРЕМА ЭРБРАНАНу, а если D1 = P(x) и D2 = ¬P(f (y )), то как быть тогда?Ведь здесь нет явного противоречия.Противоречие здесь скрытое.
Дизъюнкты D1 и D2 имеютосновные примерыP(f (c)) = D1 {x/f (c)} и ¬P(f (c)) = D2 {y /c},которые образуют противоречие. Значит, D1 и D2 тожепротиворечивы. Но как отыскать это скрытое противоречие?Нужно постараться привести литеры P(x) и P(f (y )) к общемувиду. Приведение выражений к общему виду называетсяунификацией .Нам нужен алгоритм унификации!ЗАДАЧА УНИФИКАЦИИПриведение двух атомов A0 и A00 к общему виду достигаетсяприменением такой подстановки θ, для которой A0 θ = A00 θ.Значит, для решения задачи унификации придется изучитьалгебраические свойства подстановок.ВоспоминанияПодстановка — это отображение θ : Var → Term.Конечная подстановка θ = {x1 /t1 , x2 /t2 , .
. . , xn /tn }.E θ — применение подстановки θ к выражению E .ЗАДАЧА УНИФИКАЦИИКомпозиция подстановокПусть θ, η ∈ Subst. Композиция подстановок θη — этоподстановка µ, которая определяется следующимсоотношением:µ(x) = (xθ)η для любой x ∈ Var .УтверждениеПусть θ = {x1 /t1 , . . . , xn /tn }, η = {y1 /s1 , .
. . , ym /sm }. Тогдаподстановкаµ = {x1 /t1 η, . . . , xn /tn η} ∪{yi /si : yi ∈/ {x1 , x2 , . . . , xn }} −{xj /tj η : xj = tj η}.является композицией θη.ЗАДАЧА УНИФИКАЦИИДоказательствоµ = {x1 /t1 η, . . . , xn /tn η} ∪{yi /si : yi ∈/ {x1 , x2 , . . . , xn }} −{xj /tj η : xj = tj η}.Рассмотрим произвольную z ∈ Var . Возможны 3 варианта.1. z = xj ∈ Domθ . Тогда z(θη) = (xj θ)η = tj η.Если tj η 6= xj , то xj ∈ Domµ , и xj µ = tj η.Если tj η = xj , то xj ∈/ Domµ , и xj µ = xj .В любом случае xi (θη) = xi µ.2. z = yi ∈ Domη \ Domθ .
Тогда z(θη) = (yi θ)η = yi η = si ,и zµ = si .3. z = yi ∈/ Domη ∪ Domθ . Тогда z(θη) = z и zµ = z.ЗАДАЧА УНИФИКАЦИИПримерθ = {x/f (x, c), y /g (u), z/y },η = {x/g (y ), y /z, u/c}.θη =ЗАДАЧА УНИФИКАЦИИПримерθ = {x/f (x, c), y /g (u), z/y },η = {x/g (y ), y /z, u/c}.θη =ЗАДАЧА УНИФИКАЦИИПримерθ = {x/f (x, c), y /g (u), z/y },η = {x/g (y ), y /z, u/c}.θη = {x/f (x, c)η, y /g (u)η, z/y η} ∪ {u/c}ЗАДАЧА УНИФИКАЦИИПримерθ = {x/f (x, c), y /g (u), z/y },η = {x/g (y ), y /z, u/c}.θη = {x/f (x, c)η, y /g (u)η, z/y η} ∪ {u/c}{x/f (g (y ), c), y /g (c), z/z, u/c}ЗАДАЧА УНИФИКАЦИИПримерθ = {x/f (x, c), y /g (u), z/y },η = {x/g (y ), y /z, u/c}.θη = {x/f (x, c)η, y /g (u)η, z/y η} ∪ {u/c}{x/f (g (y ), c), y /g (c), z/z, u/c}{x/f (g (y ), c), y /g (c), u/c}ЗАДАЧА УНИФИКАЦИИОпределениеПусть E1 и E2 — два логических выражения (термы, атомы,формулы и др.)Подстановка θ называется унификатором выражений E1 и E2 ,если E1 θ = E2 θ.Подстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2 , если1.
θ — унификатор выражений E1 и E2 ;2. для любого унификатора η выражений E1 и E2 существуеттакая подстановка ρ, для которой верно равенствоη = θρНОУ(E1 , E2 ) — множество наиболее общих унификатороввыражений E1 и E2 .ЗАДАЧА УНИФИКАЦИИПримерE1 = P(f (x1 ), x2 )E2 = P(y1 , c)η = {x1 /f (c), x2 /c, y1 /f (f (c))} — унификатор E1 и E2 , т.к.E1 η = P(f (f (c)), c) = E2 η.θ = {x2 /c, y1 /f (x1 )} — наиболее общий унификатор E1 и E2 ,т.к.E1 θ = P(f (x1 ), c) = E2 θ,η = θ{x1 /f (c)}.Выражения E1 и E2 унифицируемы , и θ ∈ НОУ(E1 , E2 ).ЗАДАЧА УНИФИКАЦИИПримерE1 = R(f (x1 ), x1 )E2 = R(y1 , f (y1 ))Выражения E1 и E2 не имеют унификаторов, иНОУ(E1 , E2 ) = ∅.ЗАДАЧА УНИФИКАЦИИЗадача унификациисостоит в том, чтобы для двух выражений E1 и E2 выяснить,являются ли эти выражения унифицируемыми,и, в случае их унифицируемости, вычислитьнаиболее общий унификатор.КОНЕЦ ЛЕКЦИИ 7.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 8.Алгоритм унификации.АЛГОРИТМ УНИФИКАЦИИПодстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2 , если1. θ — унификатор выражений E1 и E2 , т. е. E1 θ = E2 θ;2. для любого унификатора η выражений E1 и E2 существуеттакая подстановка ρ, для которой верно равенствоη = θρЗадача унификациисостоит в том, чтобы для двух выражений E1 и E2 выяснить,являются ли эти выражения унифицируемыми,и, в случае их унифицируемости, вычислитьнаиболее общий унификатор E1 и E2 .АЛГОРИТМ УНИФИКАЦИИНачнем с самой простого варианта задачи унификации.Как найти НОУ выражений E1 и E2 , если одно из этихвыражений — переменная, т.
е. E1 = x ∈ Var ?Лемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅.АЛГОРИТМ УНИФИКАЦИИЛемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅.Доказательство.1. Случай x ∈/ Vart .Iθ = {x/t} — унификатор выражений x и t.Действительно, xθ = t и tθ = t (т. к.
x ∈/ Vart ).IКаков бы ни был унификатор η выражений x и t, верноη = {x/t}η.Возьмем произвольную переменную y , y ∈ Var .Если y = x, то x{x/t}η = tη = xη. (почему? ) А еслиy 6= x, то y {x/t}η = y η.Таким образом, для любой переменной y верноy {x/t}η = y η, т. е. {x/t}η = η.АЛГОРИТМ УНИФИКАЦИИЛемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅.Доказательство.2. Случай x ∈ Vart .Для любой подстановки θ длина терма xθ превосходит длинутерма t(x)θ.Поэтому xθ 6= tθ для любой подстановки θ, т. е. НОУ(x, t) = ∅.АЛГОРИТМ УНИФИКАЦИИОбщий случай.Пусть E1 = P(t1 , t2 , . .
. , tn ), E2 = P(s1 , s2 , . . . , sn ).Для решения задачи унификации сопоставим паре атомовE1 , E2 систему уравненийt1 = s 1t2 = s 2E(E1 , E2 ) :···tn = s nи будем решать задачу унификации для систем уравнений.АЛГОРИТМ УНИФИКАЦИИОпределениеПодстановкаθ называется унификатором системы уравнений Et=s11t2 = s 2E:···tn = s nесли для любого i, 1 ≤ i ≤ n, термы ti θ и si θ одинаковы.Фактически, унификатор θ = {x1 /r1 , .
. . , xk /rk } — это решениесистемы уравнений E в свободной алгебре термов(эрбрановской интерпретации).Соответствующим образом определяется и наиболее общийунификатор системы уравнений(определение дать самостоятельно ).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))E1 :g (y ) = zявляется подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 :E1 θ :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 :E1 θ :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 :E1 θ :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zПочему?не имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПростой случай.ОпределениеСистема уравнений E называется приведенной , если x1 = s 1x2 = s 2E:···xn = s nи при этомI{x1 , .
. . , xn } ⊆ Var ,Iвсе переменные x1 , . . . , xn попарно различные,nS{x1 , . . . , xn } ∩Varsi = ∅.Ii=1АЛГОРИТМ УНИФИКАЦИИПримерСистема уравнений E1 является приведенной, а E2 — нет. x = f (y , g (y )) x = f (y , g (y ))z =wz =wE1 :E2 :u = g (x)u = g (c)АЛГОРИТМ УНИФИКАЦИИПростой случай.Лемма (о приведенной системе)Если система уравнений E x1 = s 1x2 = s 2E:···xn = s nявляется приведенной, то подстановка {x1 /s1 , x2 /s2 , .
. . , xn /sn }является наиболее общим унификатором системы E.ДоказательствоСамостоятельно. С использованием леммы о связке.АЛГОРИТМ УНИФИКАЦИИОбщий случай.Найти унификатор — это значит решить систему уравнений.Решать систему будем методом исключения переменных (как в«обычной» алгебре). Исключив все переменные, получимрешение (приведенную систему). Важно, чтобы все системыуравнений, которые мы будем строить в процессе «исключенияпеременных» были равносильны исходной системе.ОпределениеСистемы уравнений E1 и E1 называются равносильными , еслиНОУ(E1 ) = НОУ(E2 ).АЛГОРИТМ УНИФИКАЦИИОписание алгоритма унификации(Алгоритм Мартелли–Монтанари).Это — недетерминированный алгоритм, состоящий из 6 правил,которые можно применять в любом порядке до тех пор, покаIлибо ни одно из правил применить невозможно(построена приведенная система уравнений),Iлибо применяется правило, устанавливающееневозможность унификации.Исходная система E0 ; i = 0;while применимо одно из 6 правил doвыбрать правило R, применимое к Ei ;Ei++ = R(Ei )odАЛГОРИТМ УНИФИКАЦИИПравила преобразования решения уравнений.(1) уравнение f (t10 , t20 , .