Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации (Лекции 2014), страница 2

. . , 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..