Cássio Cristo
Dawyson Guerra
Matheu Santos
Geralmente aqueles que sabem pouco falam muito e aqueles que sabem muito
falam pouco.
Jean Jacques Rousseau
Interpretação de Herbrand de S
S − um conjunto de cláusulas
 H − o Universo de Herbrand de S
 I − uma interpretação de S sobre H
 I é uma Interpretação de Herbrand de S se
satisfaz às seguintes condições:
1. I mapeia todas as constantes de S nelas
próprias.
2. Seja f um símbolo funcional n-ário e sejam h1,
h2, .., hn elementos de H. Em I, à f é atribuída
uma função que mapeia (h1, h2, .., hn) − um
elemento de Hn − a f(h1,h2,..,hn) − um elemento
de H.

Interpretação de Herbrand de S
Não existe restrição com relação à
atribuição para cada símbolo predicado em
S, de maneira que diferentes Interpretações
de Herbrand podem existir dependendo de
tais diferentes atribuições. Desta forma, uma
Interpretação de Herbrand I de um conjunto
de cláusulas S é qualquer subconjunto de BS
(a Base de Herbrand).
Uma Interpretação de Herbrand é desta
forma uma livre atribuição de valores verdade
(verdadeiro ou falso) a todos os átomos da
BS.
Exemplo

Para testar se um conjunto S de
cláusulas é insatisfatível, precisa-se
considerar
somente
interpretações
sobre o universo Herbrand de S. Se S é
falso sob todas as interpretações do
universo Herbrand de S, então pode-se
concluir que S é insatisfatível
Implementação do Teorema de Herbrand

O teorema de Herbrand sugere um
procedimento de refutação. Isto é, dado
um conjunto insatisfatível S de cláusulas
para provar, se há um procedimento
mecânico que pode sucessivamente gerar
os conjuntos S1', ..., Sn', ... de instâncias
base de cláusulas em S e sucessivamente
testar se eles são insatisfatíveis, então
como garantido pelo Teorema de
Herbrand,
este
procedimento
pode
detectar um número finito N tal que SN' é
insatisfatível.

Gilmore em 1960 desenvolveu um
programa de computador que gerava,
sucessivamente, os conjuntos S0', S1', ...,
onde Si' é o conjunto de todos as
instâncias base obtidas pela troca das
variáveis em S por constantes no conjunto
de constantes i-nível Hi de S. Uma vez que
cada Si' é uma conjunção de cláusulas
base, pode-se usar qualquer método
disponível na lógica proposicional para
checar sua insatisfabilidade

Gilmore usou o método multiplicativo.
Isto é, quando cada Si' é produzido, Si'
é transformado em uma forma normal
disjuntiva. Qualquer conjunção na forma
normal disjuntiva que contém um par
complementar é removida. Se algum
conjunto Si' for vazio, então Si' é
insatisfatível e a prova é encontrada
Exemplo I
Considere S = {P(x), ~P(a)}.
 H0 = {a}
 S0' = P(a) ^ ~P(a) = €
 Dessa forma S é provado ser insatisfatível.

Exemplo II
Considere S = {P(a), ~P(x) ^ Q(f(x)), ~Q(f(a))}.
 H0 = {a}.
 S0' = P(a) ^ (~P(a) v Q(f(a))) ^ ~Q(f(a))

= (P(a) ^ ~P(a) ^ ~Q(f(a))) v (P(a) ^ Q(f(a)) ^
~Q(f(a)))

= €v €= €
 Dessa forma está provado que S é
insatisfatível.


O método multiplicativo usado por
Gilmore é ineficiente como é facilmente
visto. Por exemplo, para um pequeno
conjunto de 10 cláusulas base com dois
literais, há 210 conjunções
EXEMPLO
Seja S = { P( f(x), a, g(y), b) }. Então,
a e b, são as constantes e P e g são os símbolos dos
predicados...
Para resolver pega-se a constante e aplica na fórmula do
predicado e forma todas as combinações possíveis da
constante.
Exemplo:
H0 = { a, b}
H1 = { a, b, f(a), f(b), g(a), g(b) }
H2 = {a,b,f(a),f(b),g(a),
g(b),f(f(a)),f(f(b)),f(g(a)),f(g(b)),g(f(a)),g(f(b)), g(g(a)), g(g(b))}
Método de Davis e Putnam
Davis e Putnam introduziram um método
mais eficiente para testar se um conjunto
de cláusulas baixas é insatisfatível.
 Seja S um conjunto de cláusulas base.
Essencialmente, o método consiste das
quatro regras a seguir:
 I. Regra Tautológica:
Retirar todas as
cláusulas base de S que são tautológicas.
O restante do conjunto S' é insatisfatível se
e somente se S o for.


II. Regra do Literal-Único: Se há uma
cláusula unitária base L em S, obter S' de
S retirando todas aquelas cláusulas base
em S contendo L. Se S' é vazia, então S é
satisfatível. Caso contrário, obter um
conjunto S'' de S' pela retirada de ~L de S'.
S'' é insatisfatível se e somente se S o é.
Note que se ~L é uma cláusula unitária
base, então a cláusula torna-se € quando
~L é retirado da cláusula.

II. Regra do Literal-Único: Se há uma
cláusula unitária base L em S, obter S' de
S retirando todas aquelas cláusulas base
em S contendo L. Se S' é vazia, então S é
satisfatível. Caso contrário, obter um
conjunto S'' de S' pela retirada de ~L de S'.
S'' é insatisfatível se e somente se S o é.
Note que se ~L é uma cláusula unitária
base, então a cláusula torna-se € quando
~L é retirado da cláusula.

III. Regra do Literal-Puro: Um literal L
em uma cláusula base S é dito ser puro
em S se e somente se o literal ~L não
aparecer em nenhuma cláusula base
em S. Se um literal L é puro em S,
retirar todas as cláusulas base contendo
L. O restante do conjunto S' é
insatisfatível se e somente se S o é.
 IV.Regra
da Separação: Se um conjunto
S pode ser colocado na forma (A1  L) 
...  (Am  L)  (B1  ~L)  ...  (Bn 
~L)  R, onde Ai, Bi, e R são livres de L e
~L, então obter os conjuntos S1 = A1  ...
 Am  R e S2 = B1  ...  Bn  R. S é
insatisfatível se e somente se (S1  S2) é
insatisfatível, isto é, ambos S1 e S2 são
insatisfatíveis.
Resumo

A base do Teorema de Herbrand é um
conjunto formado a partir de símbolos
de
predicados,
que
é
gerado
consecutivamente, verificando-se a
insatisfatibilidade dos elementos. Um
programa
de
computador
pode
implementar a busca dos elementos,
pois na prática é muito lenta. Um
conjunto de fórmulas será testado de
forma recursiva.
OBRIGADO !