Lógica Computacional
Aula Teórica 12: estratégias de resolução
Resolução para verificar validade
Estratégias de resolução
Correcção da resolução
Teorema da resolução (Teorema 11.1)
Dada uma fórmula ϕ ∈ FP tal que FNC(ϕ), tem-se que ϕ é
contraditória se e só se ∅ ∈ Res∗ (ϕ).
Proposição 12.1
Dada uma fórmula ϕ ∈ FP tal que FNC(ϕ), tem-se que ϕ é válida
se e só se ∅ ∈ Res∗ (FNC(¬ϕ)).
Proposição 12.2
Dadas fórmulas ϕ, ψ, γ ∈ FP tal que FNC(γ) e γ ≡ ϕ ∧ ¬ψ, tem-se
que {ϕ} |= ψ se e só se ∅ ∈ Res∗ (γ).
2/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Objectivo
Procedimento automático
I
Pretende-se encontrar formas de implementar o método de
resolução, de forma que seja totalmente automático.
I
É necessário encontrar uma ordem para calcular os resolventes
das cláusulas de forma a “gerar” ∅.
I
Estratégias “cegas” ou ad-hoc não são (necessariamente)
eficientes.
3/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Estratégias de resolução
Definição 12.1: Resolução Negativa
Se no cálculo de Res∗ (ϕ) cada resolvente é encontrado a partir de
uma das cláusulas com apenas literais negados, diz-se que se está a
fazer Resolução-N.
Definição 12.2: Resolução Linear
Se no cálculo de Res∗ (ϕ) cada resolvente é encontrado a partir de
uma das cláusulas que é o resolvente do passo anterior, diz-se que
se está a fazer Resolução-L.
Proposição 12.3
Seja ϕ ∈ FP tal que FNC(ϕ) e considere-se que Res∗ (ϕ) foi obtido
por Resolução-N ou por Resolução-L. Tem-se que ϕ é contraditória
se e só se ∅ ∈ Res∗ (ϕ).
4/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Exemplo: C = {{p, q}, {¬p, r }, {¬q, s}, {¬r }, {¬s}}
Resolução-N, solução 1
Dedução
{¬p, r }
{¬r }
{¬p}
{p, q}
{q}
{¬q, s}
{¬s}
{¬q}
∅
Justificação
Cláusula C2
Cláusula C4
Resolvente de
Cláusula C1
Resolvente de
Cláusula C3
Cláusula C5
Resolvente de
Resolvente de
C2 e C4
{¬p} e C1
C3 e C5
{q} e {¬q}
Pela Proposição 12.3 conclui-se que a fórmula é contraditória.
5/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Exemplo: C = {{p, q}, {¬p, r }, {¬q, s}, {¬r }, {¬s}}
Resolução-N, solução 2
Dedução
{¬q, s}
{¬s}
{¬q}
{¬p, r }
{¬r }
{¬p}
{p, q}
{q}
∅
Justificação
Cláusula C3
Cláusula C5
Resolvente de
Cláusula C2
Cláusula C4
Resolvente de
Cláusula C1
Resolvente de
Resolvente de
C3 e C5
C2 e C4
{¬p} e C1
{q} e {¬q}
Pela Proposição 12.3 conclui-se que a fórmula é contraditória.
6/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Exemplo: C = {{p, q}, {¬p, r }, {¬q, s}, {¬r }, {¬s}}
Resolução-L, solução 1
Dedução
{¬p, r }
{¬r }
{¬p}
{p, q}
{q}
{¬q, s}
{s}
{¬s}
∅
Justificação
Cláusula C2
Cláusula C4
Resolvente de
Cláusula C1
Resolvente de
Cláusula C3
Resolvente de
Cláusula C5
Resolvente de
C2 e C4
{¬p} e C1
{q} e C3
{s} e C5
Pela Proposição 12.3 conclui-se que a fórmula é contraditória.
7/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Exemplo: C = {{p, q}, {¬p, r }, {¬q, s}, {¬r }, {¬s}}
Resolução-L, solução 2
Dedução
{¬q, s}
{¬s}
{¬q}
{p, q}
{p}
{¬p, r }
{r }
{¬r }
∅
Justificação
Cláusula C3
Cláusula C5
Resolvente de
Cláusula C1
Resolvente de
Cláusula C2
Resolvente de
Cláusula C4
Resolvente de
C3 e C5
{¬q} e C1
{p} e C2
{r } e C4
Pela Proposição 12.3 conclui-se que a fórmula é contraditória.
Há ainda uma terceira forma de fazer a prova por Resolução-L.
8/9
Resolução para verificar validade
Estratégias de resolução
Motivação
Resolução-N e Resolução-L
Exemplo: C = {{p, q}, {¬p, r }, {¬q, s}, {¬r }, {¬s}}
Pode-se sempre fazer Resolução-LN (seria a melhor estratégia!)?
Consegue-se verificar o exemplo por Resolução-LN?
Ou se começa de C4 ou de C5 .
I
Começando com C4 obtém-se {q}, mas não se tem {¬q}
Como tem que se pegar em C3 , falha a estratégia N
I
Começando com C5 obtém-se num passo {¬q}, mas não se
tem {q}; como se tem {p, q} obtém-se {p}, mas não se tem
{¬p} — falha de novo a estratégia N.
Por Resolução-LN não dá.
Conclui-se então que não se pode seguir só a estratégia LN (não é
universal).
9/9