
A resolução na lógica proposicional é um método
de prova, regra de inferência.

Toma duas cláusulas contendo literais
complementares e produz uma nova cláusula com
os literais que sobraram de ambas, até que se
chegue ao objetivo da resolução.

Provar que as cláusulas são válidas, para que isto
aconteça é necessário obter a cláusula vazia
().Caso contrário, a resolução não prova que o
algoritmo é válido.

É uma regra de inferência envolvendo duas
cláusulas que contêm literais sobre o mesmo
átomo, mas de polaridade oposta.

Exemplo: A \/ p
 p \/ B (Resolução)
A \/ B

As fórmulas A \/ p e  p \/ B são chamadas de
resolventes, e a fórmula inferida A \/ B é chamada
de resoluta, não ocorre à eliminação de suas
premissas, assim, uma fórmula pode ser usada
mais de uma vez como resolvente.
Exemplo 1:
p
p

Exemplo 2:
Regra auxiliar da contração de cláusulas:
p \/ p \/ q
p \/ q
(contração)

É aquela em que ao menos um dos
resolventes é uma cláusula unitária.
Ex: (p \/ s \/ r),  s \/ r  res p \/ r, com
apenas resoluções unitárias
p \/ s \/ r
p
s \/ r
r
s
 s \/ r
r
r


Resolução Linear é aquela em que a
fórmula resoluta de um passo deve ser
usada como resolvente do passo seguinte,
de forma que a árvore de prova é
degenerada em uma linha, de forma que
os ramos á direita são sempre constituídos
de uma única fórmula, o exemplo também
se encaixa na resolução linear

 p \/ q,  q \/ s   p \/ s
 p \/ q
 q \/ s
p \/ s
 p \/ s

Referêcia:
Silva, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. De.Lógica para
Computação. São Paulo: Thomson Learning 2006
{(A \/ B \/ D), (A \/ B \/ C \/ D), (B \/ C),
( A),(C)}
A\/ B \/  D
A\/ B \/ C
A \/ B \/ C \/ D
 B \/ C
A \/ C  A
C
C

Referêcia:
Silva, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. De.Lógica para
Computação. São Paulo: Thomson Learning 2006

Uma refutação ou objeção, em lógica é
uma razão que vai contra uma
premissa, lema ou conclusão
Referêcia:
Hübner Jomi F. Jomi. Provas com Resolução. (http://www.inf.furb.br/~jomi/logica/slides/resolucao.pdf) acessado
27/04/2009.
Refutação de G = {[A, B, C], [A], [A, B, C], [A, B]}
1-A, B,C
em G
2-A
em G
3- A, B, C
em G
4-A, B
em G
5- A B
resolvente 1, 3
6- A
resolvente 5, 4
7- 
resolvente 2, 6
Silva, Flávio S. C. da; FINGER, Marcelo;
MELO, Ana C. V. De.Lógica para
Computação. São Paulo: Thomson Learning
2006
Souza, João N. de. Lógica para Ciência da
Computação. Campus 2002