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

Дизъюнкты 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..