Nesta sec¸˜ao provaremos a correc¸˜ao deJXORh, isto ´e, para cada substituic¸˜aoσ ∈ S tem-se que σ ´e um
ACUNh-unificador idempotente deΓ. No Lema a seguir usaremos a noc¸˜ao de soluc¸˜ao de um estado Γk∆kΛ dada na Definic¸˜ao 3.2
Lema 3.17. Sejam Γk∆kΛ, Γ′k∆′kΛ′ estados v´alidos de JXORh tais que
Γk∆kΛ =⇒JXORh Γ′k∆′kΛ′. Seφ |= Γ′kΛ′ent˜aoφ |= ΓkΛ.
Demonstrac¸˜ao. SejamΓk∆kΛ, Γ′k∆′kΛ′eφ como na hip´otese, vamos provar que o resultado vale para
a) Γk∆kΛ =⇒T rivΓ′k∆′kΛ′ :
Ent˜ao temosΛ′ = Λ e Γ = Γ′∪ {0}, pela hip´otese, φ |= Γ′kΛ′ent˜ao para cadaT ∈ Γ′ e para cada
x = S ∈ Λ′temos quexφ =⊕h Sφ e T φ =⊕h0.
Note que0φ =⊕h 0 ent˜ao para cada x = S ∈ Λ e cada T ∈ Γ temos xφ =⊕h Sφ e T φ =⊕h 0,
equivalentemente,φ |= ΓkΛ. b) Γk∆kΛ =⇒Simp Γ′k∆′kΛ′ :
Ent˜ao temos Γ = ˜Γ ∪ {x ⊕ S}, onde x ´e uma vari´avel solta, e Γ′ = P urif (˜Γγ ↓), ∆′ = ∆γ ↓ e Λ′ = Λγ ↓ ∪{x = S} onde γ = {x 7→ S}. Como x ´e uma vari´avel solta de Γ e x ⊕ S est´a em sua
forma normal ent˜aox /∈ Var(S) e portanto γ ´e idempotente. Vamos provar queφ |= ΓkΛ
1. Para cadaT ∈ Γ tem-se que T φ =⊕h 0 :
TomeT ∈ Γ qualquer. • x ∈ Var(T ) :
CasoT = x ⊕ S ent˜ao obtemos T γ = xγ ⊕ S = S ⊕ S =⊕h 0; caso contr´ario, T =ACx ⊕ T
′
poisx ´e uma vari´avel solta de Γ. Logo x /∈ Var(T′) pois x ⊕ T′est´a em sua forma normal.
Seja o conjunto P := P urif ({(x ⊕ T′)γ ↓}) ent˜ao P ´e uma extens˜ao conservativa de {(x ⊕ T′)γ ↓}. Note que P ⊆ Γ′. Como por hip´otese φ |= Γ′kΛ′, temos que φ ´e um
ACUNh-unificador paraP , ent˜ao por P ser uma extens˜ao conservativa de {(x ⊕ T′)γ ↓}, φ ´e um ACUNh-unificador de((S ⊕ T′) ↓)φ ↓=
⊕h 0, equivalentemente, (S ⊕ T
′)φ ↓= ⊕h 0 e
pelo Teorema 2.1 podemos concluir que(S ⊕ T′)φ =⊕h0.
Note quex = S ∈ Λ′e portantoxφ =
⊕h Sφ, ent˜ao temos as seguintes igualdades:
T φ = (x ⊕ T′)φ = xφ ⊕ T′φ =⊕hSφ ⊕ T
′φ = (S ⊕ T′)φ = ⊕h 0
• x /∈ Var(T ) : Neste caso T γ ↓= T ↓. Como por hip´otese Γ est´a em sua forma pura temos queP urif (T ↓) = T ↓ e ent˜ao T ↓∈ Γ′. Comoφ |= Γ′kΛ′ temos queT ↓ φ =⊕h 0, e
portanto,T ↓ φ ↓=⊕h 0, isto ´e, T φ ↓=⊕h 0 e pelo Teorema 2.1 obtemos T φ =⊕h0.
2. Para caday = T ∈ Λ tem-se que yφ =⊕h T φ:
• x ∈ Var(T ) :
Defina o conjuntoX := {p ∈ Pos(T ) | T |p = x}, em outros termos, o conjunto das posic¸˜oes
de ocorrˆencia da vari´avelx em T .
Observe que para cada p, q ∈ X, p 6= q ent˜ao pkq, pois s˜ao posic¸˜oes vari´aveis. Ent˜ao enumerando o conjunto X obtemosX = {p1, . . . , pn}, e considere o seguinte contexto:
T [S]X := T [S]p1[S]p2· · · [S]pn
P definic¸˜ao de substituic¸˜ao, temos que T [S]p1[S]p2· · · [S]pn = T γ, como y = T γ ↓∈ Λ′,
temos queyφ =⊕h(T γ ↓)φ, e portanto,
yφ =⊕h yφ ↓=AC(T γ ↓)φ ↓= T γφ ↓=⊕h T γφ
Por´em T γφ = (T [S]p1[S]p2· · · [S]pn)φ = (T [S]X)φ = (T φ)[Sφ]X. Como x = S ∈ Λ′
temos quexφ =⊕hSφ, portanto T γφ = (T φ)[Sφ]X =⊕h(T φ)[Sφ]X.
Note queT [x]p = T para cada p ∈ X, pela definic¸˜ao do conjunto X e portanto:
(T φ)[xφ]X = (T [x]X)φ = (T [x]p1[x]p2· · · [x]pn)φ = T φ
Assim concluindo queyφ =⊕h T γφ =⊕h (T φ)[xφ]X = T φ.
• x 6∈ Var(T ) :
Ent˜aoT γ ↓= T ↓ logo y = T ↓∈ Λ′, e pela hip´otese deφ |= Γ′kΛ′, temos queyφ =
⊕h (T ↓
)φ. Portanto obtemos: yφ =⊕hyφ ↓=AC (T ↓)φ ↓= T φ ↓=⊕hT φ.
Logo por (1) e (2) segue queφ |= Γ|Λ c) Γk∆kΛ =⇒N −decΓ′k∆′kΛ′ :
TemosΓ = ˜Γ ∪ {s ⊕ t ⊕ S} e γ um mgu sint´atico de s =? t.
Como N-decomposic¸˜ao bifurca para dois ramos ent˜ao existem dois poss´ıveis casos para o estado Γ′k∆′kΛ′.
• Γ′ = Γ, ∆′ = ∆ ∪ {s 6= t} e Λ′ = Λ: Esse caso ´e trivial pois Γ′ = Γ e Λ′ = Λ e portanto, φ |= Γ′kΛ′implica queφ |= ΓkΛ.
• Γ′ = ˜Γγ ↓ ∪{Sγ ↓}, ∆′ = ∆γ e Λ′ = Λγ ∪ [γ]: Como φ |= Γ′kΛ′e para cadax ∈ Dom(γ),
tem-se quex = xγ ∈ Λ′ segue quexφ =
⊕ xγφ. Tomando y ∈ V \ Dom(γ) temos yγ = y
ent˜aoyγφ = yφ =⊕h yφ, donde conclu´ımos que γφ =⊕hφ.
Vamos provar queφ |= ΓkΛ. 1. TomeT ∈ Γ qualquer.
– T ∈ ˜Γ:
Observe que T γ ↓∈ Γ′, e por hip´otese temos φ |= Γ′kΛ′, ent˜ao (T γ ↓)φ = ⊕h 0 e
pelo Teorema 2.1 obtemos(T γ ↓)φ ↓=AC 0. Como (T γ ↓)φ ↓= T γφ ↓ e γφ =⊕h φ
obtemos as seguintes igualdades:
0 =AC (T γ ↓)φ ↓= T γφ ↓=⊕hT γφ =⊕h T φ.
– T = s ⊕ t ⊕ S ∈ Γ:
Comoγ ´e um mgu de s =? t temos que u = sγ = tγ. Como γφ =⊕h φ temos que
sφ ⊕ tφ ⊕ Sφ =⊕hsγφ ⊕ tγφ ⊕ Sγφ = uφ ⊕ uφ ⊕ Sγφ =⊕hSγφ.
Por outro lado, Sγφ =⊕h Sγφ ↓= (Sγ ↓)φ ↓=⊕h (Sγ ↓)φ. Como por hip´otese,
φ |= Γ′kΛ′eSγ ↓∈ Γ′temos que(Sγ ↓) =
⊕h0. Logo, para cada T ∈ Γ. T φ =⊕h0.
2. Tomey = T ∈ Λ qualquer ent˜ao y = T γ ↓∈ Λ′e ent˜ao,yφ =⊕h (T γ ↓)φ.
Comoγφ =⊕h φ e (T γ ↓)φ ↓= T γφ ↓ temos igualdades, (T γ ↓)φ =⊕h (T γ ↓)φ ↓=
T γφ ↓=⊕h T γφ =⊕hT φ, concluindo que yφ =⊕h T φ.
d) Γk∆kΛ =⇒N ul Γ′k∆′kΛ′ :
Pela definic¸˜ao da regra de inferˆencia nulificac¸˜ao temos queΓ = ˜Γ ∪ {S ⊕ h(t)}, Γ′ = ˜Γ ∪ {S, t}, ∆′ = ∆ e Λ′ = Λ.
Por hip´otese temos queφ |= Γ′kΛ′ e portanto para cadaT ∈ Γ′e para cadax = T′ ∈ Λ′tem-se que
T φ =⊕h 0 e xφ =⊕hT
′φ. Falta provar apenas que (S ⊕ h(t))φ = ⊕h0.
Note que t ∈ Γ′, logotφ =⊕h 0, e lembrando que h(0) =⊕h 0 ´e uma regra de XORh portanto
Lema 3.18. Sejam Γk∆kΛ, Γ′k∆′kΛ′ estados v´alidos de J
XORh tais que
Γk∆kΛ =⇒∗
JXORh Γ
′k∆′kΛ′. Seφ |= Γ|Λ′ ent˜aoφ |= ΓkΛ.
Demonstrac¸˜ao. Sejam Γk∆kΛ, Γ′k∆′kΛ′ e φ como na hip´otese. Ent˜ao existe um n ∈ N tal que
Γk∆kΛ =⇒nJ
XORh Γ
′k∆′kΛ′, vamos provar por induc¸˜ao sobren.
Hip´otese de induc¸˜ao: SejamE1 := Γ1k∆1kΛ1,E2 := Γ2k∆2kΛ2 estados v´alidos deJXORhtais que
E1=⇒mJXORh E2em < n Se ϕ |= Γ2kΛ2ent˜aoϕ |= Γ1kΛ1.
Base da induc¸˜ao: Suponhan = 0 e portanto Γk∆kΛ =⇒0JXORh Γ′k∆′kΛ′implicando queΓk∆kΛ =
Γ′k∆′kΛ′ e portanto Γ′ = Γ, ∆′ = ∆ e Λ′ = Λ e como por hip´otese φ |= Γ′kΛ′ assim temos que φ |= ΓkΛ.
Supoonhan > 1 ent˜ao existe Γ′′k∆′′kΛ′′um estado v´alido deJXORhtal que:
Γk∆kΛ =⇒n−1J
XORh Γ
′′k∆′′kΛ′′=⇒
JXORh Γ
′k∆′kΛ′
Comoφ |= Γ′kΛ′ temos que pelo Lema 3.17,φ |= Γ′′kΛ′′e comon − 1 < n e Γk∆kΛ =⇒n−1 JXORh
Γ′k∆′kΛ′temos pela hip´otese de induc¸˜ao queφ |= ΓkΛ, como queriamos demonstrar.
Assim provamos que para todon ∈ N, se Γk∆kΛ =⇒nJXORh Γ′k∆′kΛ′ e φ |= Γ′kΛ′ ent˜ao φ |=
ΓkΛ.
Iremos agora enunciar o Teorema da Correc¸˜ao deJXORh e demonstra-lo utilizando principalmente
o Lema 3.18 e o fato de que cada soluc¸˜ao gerada pelo algoritmo ´e uma substituic¸˜ao idempotente. Lema 3.19. SejamΓk∆kΛ, Γ′k∆′kΛ′ estados v´alidos deJ
XORh e substituic¸˜oesσΛ:= {x 7→ S | x =
S ∈ Λ}, σΛ′ := {x 7→ S | x = S ∈ Λ′} tais que Γk∆kΛ =⇒∗
JXORh Γ
′k∆′kΛ′. Seσ
Λ ´e idempotente,
ent˜aoσΛ′ ´e idempotente.
Demonstrac¸˜ao. SejamΓk∆kΛ, Γ′k∆′kΛ′,σ
ΛeσΛ′ como na hip´otese. Vamos provar para cada regra de
inferˆencia deJXORh.
a) Γk∆kΛ =⇒T rivΓ′k∆′kΛ′ :
Temos queΛ′ = Λ e portanto σΛ′ = σΛ, e o resultado segue.
b) Γk∆kΛ =⇒Simp Γ′k∆′kΛ′ :
Temos queΓ = ˜Γ ∪ {x ⊕ S}, Γ′ = P urif (˜Γγ ↓), ∆′ = ∆γ ↓ e Λ′ = Λγ ↓ ∪{x = S} onde γ = {x 7→ S} e x uma vari´avel solta.
Afirmac¸˜ao: Para caday = T ∈ Λ, y /∈ Var(S):
Observe que porΓk∆kΛ ser um estado v´alido de JXORh, ent˜ao existe um estado inicialΓk∅k∅ tal
queΓk∅k∅ =⇒∗JXORh Γk∆kΛ e portanto, para cada y = T ∈ Λ, existem Γyk∆ykΛy,Γ′yk∆′ykΛ′y
estados v´alidos deJXORh tais queΓy = ˜Γy ∪ {y ⊕ T′} onde y ´e uma vari´avel solta de Γy,Γ′y =
P urif ((˜Γy)γ′ ↓), ∆′y = ∆yγ′ ↓, Λ′y = Λyγ′↓ ∪{y = T′} e
Γk∅k∅ =⇒∗JXORh Γyk∆ykΛy =⇒Simp Γ′yk∆′ykΛ′y =⇒∗JXORh Γk∆kΛ
E portanto a vari´avely /∈ Var(Γ′y) e como as regras de inferˆencia s´o inserem vari´aveis novas, ent˜ao
y /∈ Var(Γ), em particular y /∈ Var(S).
Note queΛ′ = Λγ ↓ ∪{x = S} e portanto σΛ′ = {y 7→ T γ ↓ | y = T ∈ Λ} ∪ {x 7→ S}. Como
σΛ= {y 7→ T | y = T ∈ Λ} ent˜ao: σΛ′ = {y 7→ yσΛγ ↓ | y ∈ Dom(σΛ)} ∪ {x 7→ S}.
Por hip´oteseσΛ´e idempotente ent˜ao obtemos que para caday ∈ Dom(σΛ) tem-se que Dom(σΛ) ∩
Var(yσΛ) = ∅ e como Var(yσΛγ ↓) ⊆ (Var(yσΛ) \ {x}) ∪ Var(S). pois γ = {x 7→ S}, e pela
afirmac¸˜ao temos que Dom(σΛ) ∩ Var(S) = ∅. Al´em disso para cada y ∈ Dom(σΛ′) \ {x} =
Dom(σΛ) temos Var(yσΛ′) ∩ {x} = ∅. Assim,
(Dom(σΛ′) \ {x}) ∩ Var(yσΛ′) = Dom(σΛ) ∩ Var(yσΛγ ↓)
⊆ Dom(σΛ) ∩ ((Var(yσΛ)) ∪ Var(S)) = ∅
(3.7)
Portanto Dom(σΛ′) ∩ Var(yσΛ′) = ∅ para cada y ∈ Dom(σΛ′) \ {x} e como xσΛ′ = Var(S)
ent˜ao pela afimac¸˜ao acima e por x /∈ Var(S) temos que Dom(σΛ′) ∩ Var(xσΛ′) = Dom(σΛ′) ∩
Var(S) = ∅, concluindo que para todo y ∈ Dom(σΛ′), Dom(σΛ′) ∩ Var(yσΛ′) = ∅, e portanto σΛ′
´e idempotente.
c) Γk∆kΛ =⇒N −decΓ′k∆′kΛ′ :
TemosΓ = ˜Γ ∪ {s ⊕ t ⊕ T } e γ ´e um mgu idempotente de s =? t, via unificac¸˜ao sint´atica, tal que Dom(γ) ⊆ Var(s) ∪ Var(t) e Var(Im(γ)) ⊆ Var(s) ∪ Var(t) ⊆ Var(Γ).
Como provamos no item anterior que para cada x = S ∈ Λ, tem-se que x /∈ Var(Γ) e portanto para cadax = S ∈ Λ, x /∈ Var(Im(γ)), isto ´e, Dom(σΛ) ∩ Var(Im(γ)) = ∅. Por hip´otese σΛ ´e
idempotente, ent˜aoDom(σΛ) ∩ Var(Im(σΛ)) = ∅, e portanto obtemos:
Dom(σΛ) ∩
Var(Im(γ)) ∪ Var(σΛ)
Existem dois ramos na inferˆencia, ent˜ao analisaremos separadamente cada um: • Γ′ = Γ, ∆′ = ∆ ˙∪{s 6= t} e Λ′ = Λ: Logo σ
Λ′ = σΛ e portanto pela hip´otese deσΛ ser
idempotente ent˜aoσΛ′ ´e idempotente.
• Γ′= ˜Γγ ↓, ∆′ = ∆γ ↓ e Λ′ = Λγ ∪ [γ]:
An´alogo ao caso da regra simplificac¸˜ao, com a diferenc¸a de que[γ] pode incluir mais de uma vari´avel no dom´ınio, pelo mesmo racioc´ınio da regra simplificac¸˜ao obtemos que:
σΛ′ := {x 7→ xσΛγ ↓ | x ∈ Dom(σΛ)} ∪ γ
Portanto temosDom(σΛ′) = Dom(σΛ) ∪ Dom(γ) e,
Var(Im(σΛ′)) ⊆
Var(Im(σΛ)) \ Dom(γ)
∪ Var(Im(γ)) Ent˜ao podemos concluir queDom(σΛ′) ∩ Var(Im(σΛ′)) = ∅.
d) Γk∆kΛ =⇒N ulΓ′k∆′kΛ′ : Temos que Λ′= Λ e portanto por σ
Λ′ ´e idempotente.
Lema 3.20. SeΓk∆kΛ um estado v´alido de JXORhent˜aoσΛ´e uma substituic¸˜ao idempotente.
Demonstrac¸˜ao. ComoΓk∆kΛ ´e um estado v´alido de JXORhent˜ao existe um estado inicial bΓk∅k∅ e um
n ∈ N tais que bΓk∅k∅ =⇒nJXORh Γk∆kΛ. Vamos provar por induc¸˜ao sobren ∈ N:
Hip´otese de induc¸˜ao: SeΓ′k∆′kΛ′ ´e um estado v´alido deJ
XORh onde existe um estado inicial bΓ′k∅k∅
em < n tais que bΓ′k∅k∅ =⇒mJXORh Γ′k∆′kΛ′. Ent˜ao σΛ′ ´e uma substituic¸˜ao idempotente.
Caso base: Quandon = 0 temos que Γk∆kΛ ´e um estado inicial e portanto Λ = ∅, logo σΛ= ∅ que ´e
a substituic¸˜ao identidade, logo idempotente.
Suponha agora quen > 1, portanto existe Γ′k∆′kΛ′tal que
b
Γk∅k∅ =⇒n−1J
XORh Γ
′k∆′kΛ′ =⇒
JXORh Γk∆kΛ
Comon − 1 < n e pela hip´otese de induc¸˜ao temos que Γ′k∆′kΛ′ ´e um estado v´alido deJ
XORh onde
Teorema 3.4 (Correc¸˜ao de JXORh). Sejam ˜Γ um problema de ACUNh-unificac¸˜ao em sua forma pa-
dronizada, Γ := P urif (˜Γ) e L := JXORh(Γk∅k∅). Ent˜ao para cada σ ∈ L temos que σ ´e um
ACUNh-unificador idempotente de ˜Γ.
Demonstrac¸˜ao. Sejaσ ∈ L, ent˜ao pela definic¸˜ao do algoritmo JXORh existe∅k∆kΛ um estado v´alido
deJXORhtal queσ = σΛeΓk∅k∅ =⇒∗JXORh ∅k∆kΛ.
Pelo Lema 3.20,σ ´e idempotente, logo para cada x = S ∈ Λ temos xσ = xσσ = xσΛσ =⊕hSσ
Implicando queσ |= ∅kΛ e pelo Lema 3.18 temos que σ |= Γk∅, isto ´e, para cada T ∈ Γ, tem-se que T σ =⊕h 0 e portanto σ ´e um ACUNh-unificador de Γ. Pelo Teorema 3.2 temos que Γ ´e uma extens˜ao
conservativa de ˜Γ e como σ ´e um ACUNh-unificador idempotente de Γ ent˜ao σ ´e um ACUNh-unificador idempotente de ˜Γ.