A resolução na lógica proposicional é um método A resolução na lógica proposicional é um método de prova, regra de inferência.de prova, regra de inferência.

Toma duas cláusulas contendo literais Toma duas cláusulas contendo literais complementares e produz uma nova cláusula com complementares e produz uma nova cláusula com os literais que sobraram de ambas, até que se os literais que sobraram de ambas, até que se chegue ao objetivo da resolução.chegue ao objetivo da resolução.

Provar que as cláusulas são válidas, para que isto Provar que as cláusulas são válidas, para que isto aconteça é necessário obter a aconteça é necessário obter a cláusula vaziacláusula vazia (().Caso contrário, a resolução não prova que o ).Caso contrário, a resolução não prova que o algoritmo é válido. algoritmo é válido.

É uma regra de inferência envolvendo duas É uma regra de inferência envolvendo duas cláusulas que contêm literais sobre o mesmo cláusulas que contêm literais sobre o mesmo átomo, mas de polaridade oposta.átomo, mas de polaridade oposta.

Exemplo: Exemplo: A \/ p A \/ p p \/ B p \/ B (Resolução) (Resolução)

A \/ BA \/ B As fórmulas A \/ p e As fórmulas A \/ p e p \/ B são chamadas de p \/ B são chamadas de

resolventesresolventes, e a fórmula inferida A \/ B é chamada , e a fórmula inferida A \/ B é chamada de de resolutaresoluta, não ocorre à eliminação de suas , não ocorre à eliminação de suas premissas, assim, uma fórmula pode ser usada premissas, assim, uma fórmula pode ser usada mais de uma vez como resolvente.mais de uma vez como resolvente.

Exemplo 1: Exemplo 1:

p p p p

Exemplo 2:Exemplo 2:

Regra auxiliar da contração de cláusulas:Regra auxiliar da contração de cláusulas:

p \/ p \/ qp \/ p \/ q

p \/ qp \/ q (contração) (contração)

É aquela em que ao menos um dos É aquela em que ao menos um dos resolventes é uma cláusula unitária.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 \/ D A\/ B \/ C 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 G2-A em G3- A, B, C em G4-A, B em G5- A B resolvente 1, 36- A resolvente 5, 47- 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