Лемма (о подъеме).

Если D₁^/ – пример дизъюнкта D₁,

D₂^/ – пример дизъюнкта D₂ и

D^/ – резольвента D₁^/ и D₂^/,

то существует обобщенная резольвента D дизъюнктов D₁ и D₂,

такая что D^/ – пример D.

Примечание. Обобщенная резольвента – это резольвента склеек посылок.

Доказательство. Если D₁ и D₂ имеют общие переменные, то заменой переменных в одном из дизъюнктов можно добиться того, что переменные дизъюнкта D₁ отличны от переменных дизъюнкта D₂. Будем поэтому считать, что D₁ и D₂ не имеют общих переменных.

Так как D₁ ^/ – пример D₁ и D₂^/ – пример D₂, то существуют подстановки α₁ и α₂ такие, что D₁^/=(D₁)α₁ и D₂^/=(D₂)α₂. Последовательность α =(α₁,α₂) также будет подстановкой и поскольку D₁ и D₂ не имеют общих переменных, то D₁^/= (D₁)α и D₂^/= (D₂)α.

Дизъюнкт D^/ является резольвентой дизъюнктов D₁^/ и D₂^/. Это означает, что существуют литералы L₁^/єD₁^/ и L₂^/єD₂^/ и подстановка τ такие, что τ - наиболее общий унификатор L₁^/ и L₂^/ и

D^/=((D₁^/)τ -(L₁^/)τ) U ((D₂^/)τ -(L₂^/)τ) (1)

Пусть L₁¹,…,L₁^r – литералы дизъюнкта D₁, которые подстановкой α переводятся L₁^/, а L₂¹,…,L₂^s – литералы дизъюнкта D₂, которые подстановкой α переводятся в L₂^/. Следовательно, литералы L₁¹,…,L₁^r, унифицируемы, а поэтому существует наиболее общий унификатор β₁ для этого множества. Дизъюнкт (L₁¹)β₁ (равный (L₁²)β₁,…, (L₁^r)β₁) обозначим через L₁. По определению наиболее общего унификатора найдется подстановка γ₁, для которой выполняется равенство α₁= β₁ ◦ γ₁.

По аналогичным соображениям, существуют подстановки β₂ и γ₂ такие, что β₂ – наиболее общий унификатор множества литералов L₂¹,…,L₂^s и α₂= β ₂◦ γ₂. Литерал (L₂¹) β₂ обозначим через L₂.

Легко видеть, что L₁ и L₂ не имеют общих переменных. Поскольку дизъюнкты D₁ и D₂ также не имеют общих переменных, то можно считать, что (β₁, β₂)= β, (γ₁, γ₂)= γ и α= β ◦ γ. Сказанное в этом абзаце иллюстрируется рисунками 4.1 и 4.2.

Рис. 4.1

Рис. 4.2

Литералы L₁′ и L₂′, как отмечено выше, унифицируемы подстановкой τ. Следовательно, литералы L₁ и L₂ также унифицируемы (подстановкой γ◦τ). Отсюда следует, что существует наиболее общий унификатор σ множества {L₁, L₂} (см.рис.4.3). Возьмем в качестве D дизъюнкт

D=[ ((D₁) β) σ – (L₁)σ] U [((D₂) β) σ – (L₂)σ] (2)

Ясно, что D – резольвента дизъюнктов D₁ и D₂.

Осталось показать. Что D′ –пример D.

Рис. 4.3

Так как σ – наиболее общий унификатор L₁ и L₂, то существует подстановка δ такая, что γ◦τ =σ◦δ. В таком случае из последнего равенства, равенств (1), (2) и α= β ◦ γ следует, что

D′=((D₁′)τ – (L₁′)τ) U ((D₂′)τ –(L₂′)τ)=

[((D₁) α) τ –((L₁¹) α) τ] U [((D₂) α) τ –((L₂¹) α) τ] =

[(D₁) α◦τ –(L₁¹) α◦τ] U [(D₂) α◦τ –(L₂¹) α◦τ]=

[(D₁) β ◦ γ ◦ τ –(L₁¹) β ◦ γ ◦τ] U [(D₂) β ◦ γ ◦τ –(L₂¹) β ◦ γ ◦τ]=

[(D₁) β ◦ σ ◦ δ – (L₁¹) β ◦ σ ◦ δ] U [(D₂) β ◦ σ ◦ δ – (L₂¹) β ◦ σ ◦ δ ]=

[(D₁) β ◦ σ – (L₁) σ] δ U [(D₂) β ◦ σ – (L₂) σ] δ =

(D) δ.

Мы доказали, что D′ – пример D.

Дата добавления: 2015-11-30