4.1. CLÁUSULAS
128
Todas as estruturas de Herbrand têm o mesmo domı́nio (ou universo) e coincidem no valor
dos sı́mbolos funcionais: apenas diferem no valor dos sı́mbolos de predicado.
Exemplo 4.6. Para a linguagem Lss (do slowsort) o domı́nio (ou universo) de qualquer
estrutura de Herbrand A é:
A = {0,nil,s(0),s(nil),cons(0,0),cons(0,nil),cons(nil,0),cons(nil,nil),. . . }
e 0A = 0, nilA = nil, sA (0) = s(0), etc
Exemplo 4.7. Seja a linguagem L tal que F1 = {f, g}, R1 = {p, r} e R2 = {q}. Como L
não tem constantes adicionamos uma constante c a T0 de L. O universo de Herbrand é:
A = {c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),. . . }
e cA = c, f A (c) = f(c), f A (g(c)) = f(g(c)), etc
Teorema 4.1. Seja Φ um conjunto de cláusulas. Então Φ é satisfazı́vel se e só se tiver um
modelo de Herbrand.
Demonstração. (⇐) É óbvio que se Φ tiver um modelo de Herbrand é satisfazı́vel
(⇒) Seja A um modelo de Φ. É necessário mostrar que Φ tem um modelo de Herbrand, AH :
associamos a cada sı́mbolo relacional R a relação:
A
A
RAH = {(t1 , . . . , tn ) ∈ T0n | (tA
1 , . . . , tn ) ∈ R }
Vejamos que AH é um modelo de Φ: seja ∀(λ1 ∨ . . . ∨ λm ) ∈ Φ.
AH |= ∀(λ1 ∨ . . . ∨ λm )
sse para toda a interpretação das variáveis sH em AH se tem
AH |=sH (λ1 ∨ . . . ∨ λm )
Se sH (x) = t ∈ T0 seja s(x) = tA em A. Como A |= ∀(λ1 ∨ . . . ∨ λm ), então A |=s
(λ1 ∨ . . . ∨ λm ), isto é, existe pelo menos um k tal que A |=s λk . Mas, por construção de
AH e como cada λi é um literal, A |=s λi sse AH |=sH λi , 1 ≤ i ≤ m (verifica!). Donde
AH |=sH (λ1 ∨ . . . ∨ λm ) sse A |=s (λ1 ∨ . . . ∨ λm )
.
Nota que se Φ não fosse um conjunto de cláusulas o teorema não se verificava.
Departamento de Ciência de Computadores F.C.U.P.
4.1. CLÁUSULAS
129
Exemplo 4.8. O conjunto de proposições {p(c), ∃x¬p(x)} da linguagem com F0 = {c} e
R1 = {p} é satisfazı́vel mas não tem modelo de Herbrand: A = ({0, 1}, ·A ) com cA = 0 e
pA = {0} satisfaz o conjunto. Mas T0 = {c} e as únicas estruturas de Herbrand são tais que
pH1 = ∅ e pH2 = {c}, e nenhuma satisfaz o conjunto.
Corolário 4.1. Um conjunto de cláusulas de Horn é satisfazı́vel sse tiver um modelo de
Herbrand.
Definição 4.6. Dado um conjunto de cláusulas de Horn Φ o modelo mı́nimo de Herbrand
de Φ é a estrutura de Herbrand AΦ tal que, para R ∈ Rn :
RAΦ = {(t1 , . . . , tn ) ∈ T0n | Φ ⊢ R(t1 , . . . , tn )}
O modelo da definição anterior é mı́nimo porque:
Teorema 4.2. Seja Φ um conjunto satisfazı́vel de cláusulas de Horn. Então:
• AΦ |= Φ
• se AH é um modelo de Herbrand de Φ, então para todo o sı́mbolo relacional n-ário R,
RAΦ ⊆ RAH
Demonstração. Para toda a fórmula atómica α, com variáveis x1 , . . . , xk e para toda a interpretação de variáveis s, se s(xi ) = ti , 1 ≤ i ≤ k, então, pela definição de AΦ , tem-se:
AΦ |=s α sse Φ ⊢ α[tk /xk ]
(4.5)
onde α[tk /xk ] é a fórmula que resulta de α substituindo simultaneamente todas as ocorrências
de x1 , . . . , xk por t1 , . . . , tk .
Seja ∀x1 . . . ∀xm θ ∈ Φ, e θ não tem quantificadores. Vamos mostrar que se tem AΦ |=s θ
qualquer que seja a interpretação s.
Temos dois casos:
θ ≡ (¬α1 ∨ . . . ∨ ¬αn ∨ α), com n ≥ 0 Temos que demonstrar que AΦ |=s (α1 ∧ . . . ∧
αn ) → α, para toda interpretação s. Se n = 0, então θ é uma fórmula atómica e o
resultado segue de (4.5). Se n > 0, se AΦ |=s α1 ∧ . . . ∧ αn , então AΦ |=s αi ,
1 ≤ i ≤ n. Mas, de (4.5), Φ ⊢ α1 [tm /xm ], . . . , Φ ⊢ αm [tm /xm ]. E então, Φ ⊢ α[tm /xm ],
porque Φ ⊢ ((α0 ∧ . . . ∧ αn ) → α)[tm /xm ]. Temos então que AΦ |=s θ.
θ ≡ (¬α0 ∨ . . . ∨ ¬αn ) De ∀x1 . . . ∀xm θ ∈ Φ, vem que Φ ⊢ θ[tm /xm ] (aplicando m vezes a
regra ∀E). Logo, Φ ⊢ ¬(α0 ∧ . . . ∧ αn )[tm /xm ]. Se AΦ 6|=s (¬α0 ∨ . . . ∨ ¬αn ), então
AΦ |=s α0 , . . . AΦ |=s αn . Mas, por (4.5), Φ ⊢ α0 [tm /xm ],. . . , Φ ⊢ αn [tm /xm ], donde
Φ ⊢ (α0 ∧ . . . ∧ αn )[tm /xm ]. Absurdo! Então, AΦ |=s θ.
Departamento de Ciência de Computadores F.C.U.P.
4.1. CLÁUSULAS
130
Seja AH um modelo de Herbrand de Φ e R um sı́mbolo relacional. Se (t1 , . . . , tn ) ∈ RAΦ ,
então Φ ⊢ R(t1 , . . . , tn ), e pela integridade, AH |= R(t1 , . . . , tn ), i.e, (t1 , . . . , tn ) ∈ RAH
O teorema seguinte garante que dado um programa definido P (conjunto de cláusulas de Horn
positivas) e um objectivo G (uma cláusula de Horn negativa) , P ∪ {G} é não satisfazı́vel se
e só se G não é satisfeito em AP .
Teorema 4.3. Seja Φ um conjunto de cláusulas de Horn. Para qualquer fórmula fechada
da forma ∃x1 . . . ∃xn (α0 ∧ . . . ∧ αl ), onde cada αi é uma fórmula atómica, as seguintes
afirmações são equivalentes:
1. Φ ⊢ ∃x1 . . . ∃xn (α0 ∧ . . . ∧ αl )
2. AΦ |= ∃x1 . . . ∃xn (α0 ∧ . . . ∧ αl )
3. existem t1 , . . . , tn ∈ T0 , tal que Φ ⊢ (α0 ∧ . . . ∧ αl )[tn /xn ]
Demonstração.
(1)⇒(2) pela integridade da LPO.
(2)⇒(3) Se AΦ |= ∃x1 . . . ∃xn (α0 ∧ . . . ∧ αl ) existe uma interpretação das variáveis s, com
s(xi ) = ti , 1 ≤ i ≤ n, tal que AΦ |=s (α0 ∧ . . . ∧ αl ). Logo AΦ |=s α0 , . . . ,AΦ |=s αl , e,
por (4.5), Φ ⊢ α0 [tn /xn ], . . . Φ ⊢ αl [tn /xn ]. E aplicando a regra ∧ I l vezes, Φ ⊢ (α0 ∧ . . . ∧
αl )[tn /xn ].
(3)⇒ (1) Basta aplicar n vezes a regra ∃I.
Exercı́cio 4.4. Seja L uma linguagem de 1¯a ordem sem igualdade e Φ um conjunto de
proposições.
1. Mostra que Φ ⊢ ∃xφ não implica necessariamente que existe um termo t ∈ T tal que
Φ ⊢ φ[t/x]
2. Supõe que Φ é um conjunto de cláusulas de Horn e φ da forma α0 ∧ . . . ∧ αl onde αi
são fórmulas atómicas. Mostra que se Φ ⊢ ∃xφ existe t ∈ T0 tal que Φ ⊢ φ[t/x].
⋄
Resolução 4.4
1. Basta considerar R1 = {R}, Φ = {∃xR(x)} e φ a fórmula R(x).
2. Segue do teorema anterior.
Seja P um programa definido. Então:
Departamento de Ciência de Computadores F.C.U.P.
4.1. CLÁUSULAS
131
LP linguagem de primeira ordem constituı́da por todos os sı́mbolos não lógicos de P (eventualmente com mais uma constante c). Ex: Seja P
p(x) ← q(f(x), g(x))
r(x) ←
LP é dada por F0 = {c}, F1 = {f, g}, R1 = {p, r} e R2 = {q}
UP O universo de Herbrand de P , isto é, o conjunto dos termos fechados da linguagem LP .
Ex:
UP = {c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),. . . }
BP A base de Herbrand de LP , é o conjunto de todas as fórmulas atómicas fechadas da
linguagem LP . Ex:
BP = {p(c), q(c, c), r(c), p(f(c)), p(g(c)), q(f(c), c), . . .}
IA Cada estrutura de Herbrand de LP fica identificada por um subconjunto de BP (dos
átomos que são verdadeiros nessa estrutura)...Isto é, dada uma estrutura de Herbrand
A, existe um e um só IA ⊆ BP tal que, para cada sı́mbolo relacional n-ário R de LP e
para t1 , . . . , tn ∈ UP :
R(t1 , . . . , tn ) ∈ IA sse (t1 , . . . , tn ) ∈ RA
Ex: Seja A tal que pA = rA = {c, f(c), g(c)} e qA = ∅. Então,
IA = {p(c), p(f(c)), p(g(c)), r(c), r(f(c)), r(g(c))}
. Nota que A 6|= P (porquê?).
MP
MP = IAP , onde AP é modelo mı́nimo de Herbrand. Ex: MP = {r(t) | t ∈ UP }
Corolário 4.2. Seja P um programa definido. Então
MP = {φ ∈ BP | P |= φ}
Exercı́cio 4.5. Mostra o corolário anterior. ⋄
Exercı́cio 4.6. Mostra que MP ⊆ IA para qualquer modelo de Herbrand A de P . ⋄
Exercı́cio 4.7. Para cada um dos programas definidos P e objectivos G descritos abaixo
determina:
• LP
Departamento de Ciência de Computadores F.C.U.P.
4.2. UNIFICAÇÃO
132
• cada fórmula do programa e do objectivo sem ser na notação clausal (i.e com os quantificadores e operações lógicas ∨ , ∧ e ¬)
• um modelo de Herbrand A de P
• UP
• BP
• IA para o modelo de Herbrand A que escolheste
• para G =← α1 , . . . , αk determina os termos fechados t1 ,. . . ,tn tais que P |= (α1 ∧ . . . ∧
αk )[t1 /x1 , . . . , tn /xn ], onde x1 ,. . . ,xn são as variáveis que ocorrem em G ou mostra que
P ∪ {G} é satisfazı́vel.
a)
P :
N esimo(s(0), cons(x, y), x) ←
N esimo(s(w), cons(y, z), x) ← N esimo(w, z, x)
G:
b)
P :
← N esimo(x, cons(y, cons(z, nil)), z)
Delete(x, cons(x, y), y) ←
Delete(x, cons(y, z), cons(y, w)) ← Delete(x, z, w)
G:
c)
P :
← Delete(y, cons(x, cons(y, nil), z)
M ax(x, y, x) ← Less eq(y, x)
M ax(x, y, y) ← Less eq(x, y)
Less eq(0, x) ←
Less eq(s(x), s(y)) ← Less eq(x, y)
G:
← M ax(s(0), x, s(s(0)))
⋄
4.2
Unificação
Definição 4.7. Uma substituição é uma função σ : Var −→ T tal que o conjunto dos
xi ∈ Var com σ(xi ) = ti 6= xi é finito. E escreve-se
σ = [t1 /x1 , . . . , tn /xn ]
A substituição identidade é a substituição ι tal que ι(x) = x, para todo o x ∈ Var.
Uma substituição [t1 /x1 , . . . , tn /xn ] é fechada se todos os ti são termos fechados.
Departamento de Ciência de Computadores F.C.U.P.