Princípio da resolução

O princípio da resolução é uma regra de inferência que dá origem a uma técnica de demonstração por refutação para sentenças e inferências da lógica proposicional e da lógica de primeira ordem.

A resolução na lógica proposicional

Regra de resolução

O sistema dedutivo de resolução na lógica proposicional não possui axiomas, mas apenas uma regra de inferência que produz, a partir de duas cláusulas, uma nova cláusula implicada por elas. A regra de resolução toma duas cláusulas contendo literais complementares e produz uma nova cláusula com todos os literais de ambos, excluídos estes complementares. Formalmente, onde $a_i$ e $b_j$ são literais complementares:

$$\frac{a_1\vee \dots \vee a_{i-1}\vee a_i\vee a_{i+1}\vee \dots \vee a_n,b_1\vee \dots \vee b_{j-1}\vee b_j\vee b_{j+1}\vee \dots \vee b_m}{a_1\vee \dots \vee a_{i-1}\vee a_{i+1}\vee \dots \vee a_n\vee b_1\vee \dots \vee b_{j-1}\vee b_{j+1}\vee \dots \vee b_m}$$ A cláusula produzida pela regra de resolução é chamada de resolvente das duas cláusulas iniciais.

Quando as duas cláusulas contêm mais de um par de literais complementares, a regra de resolução pode ser aplicada (independentemente) para cada par. Entretanto, apenas o par de literais resolvidos pode ser removido: todos os outros pares de literais permanecem na cláusula resolvente.

Uma técnica de resolução

Quando usada em conjunto com um algoritmo de busca, a regra de resolução ganha poder e utiliza o algoritmo de busca para decidir a satisfatibilidade de uma fórmula proposicional e a validade da sentença sob um conjunto de axiomas.

Esta técnica de resolução usa prova por contradição e é baseada no fato de que qualquer sentença da lógica proposicional pode ser convertida para uma sentença equivalente na forma normal conjuntiva. Os passos são os seguintes:

• Todas as premissas e a negação da sentença a ser provada (conjectura) tem que estar conectadas por conjunções.
• A sentença resultante é convertida para a forma normal conjuntiva (tratada como um conjunto de cláusulas, S).
• A regra de resolução é aplicada a todos os possíveis pares de cláusulas que contém literais complementares. Após cada aplicação da regra de resolução, a cláusula resultante é simplificada removendo-se os literais repetidos. Se a cláusula contém literais complementares, ela é descartada (como uma tautologia). Caso contrário, e se ela ainda não está presente no conjunto de cláusulas S, então ela é adicionada a S, e é considerada para posteriores inferências da resolução.
• Se depois de aplicar a regra de resolução uma cláusula vazia é derivada, a formula inteira não é satisfeita (ou contraditória), então é possível concluir que a conjectura inicial provém das premissas originais.
• Se, por outro lado, a cláusula vazia não pode ser derivada, e a regra de resolução não pode ser aplicada para derivar mais cláusulas, a conjectura não é um teorema da base de conhecimentos original.

Outra instância deste algoritmo é o algoritmo de Davis-Putnam original, que foi mais tarde refinado para o algoritmo DPLL, que removeu a necessidade de uma representação explícita dos resolventes.

Como exemplo do algoritmo acima, considere a seguinte fórmula:

$\mathrm{\neg }p\wedge (q\vee r\vee q)\wedge (\mathrm{\neg }r\vee \mathrm{\neg }s)\wedge (p\vee s)\wedge (\mathrm{\neg }q\vee \mathrm{\neg }s)$

Que pode ser vista como um conjunto de cláusulas:

$\{\{\mathrm{\neg }p\},\{q,r\},\{\mathrm{\neg }r,\mathrm{\neg }s\},\{p,s\},\{\mathrm{\neg }q,\mathrm{\neg }s\}\}$

Seja $C$ um conjunto de cláusulas e representamos por $\mathrm{\perp }$ a cláusula vazia, $\{\}$. Aplica-se então a regra de inferência:

• $\frac{\{C,p\}\{C^{\prime },\mathrm{\neg }p\}}{\{C,C^{\prime }\}}$

Aplicando a regra no conjunto de cláusulas do exemplo acima:

Foi possível então a dedução da cláusula vazia a partir do conjunto inicial de cláusulas.

A resolução na lógica de primeira ordem

A resolução na Lógica de primeira ordem condensa os silogismos tradicionais de inferência lógica em uma única regra. Para entender como a resolução funciona, considere o seguinte exemplo de silogismo da lógica aristotélica:

Todos os gregos são europeus.
Homero é grego.
Então, Homero é europeu.

Ou de maneira mais geral:

$\mathrm{\forall }$X.(P(X) implica Q(X)).
P(a).
Então, Q(a).

Para traçar o raciocínio usado na técnica de resolução, primeiro as cláusulas devem ser convertidas para a forma normal conjuntiva. Nessa forma, todas as quantificações se tornam implícitas: quantificadores universais em variáveis (X, Y...) são simplesmente omitidos quando subentendidos, enquanto variáveis em quantificadores existenciais são substituídas por funções de Skolem.

$\mathrm{\neg }$P(X) $\vee$ Q(X)
P(a) 
Então, Q(a)

Então a questão é, como a técnica de resolução deriva a última cláusula a partir das duas primeiras? A regra é simples:

• Encontre duas cláusulas contendo o mesmo predicado, onde uma cláusula é negada e a outra não.
• Faça a unificação em ambos os predicados. (Se a unificação falhar, então você fez uma má escolha de predicados. Volte para o passo anterior e tente novamente.)
• Se, após a unificação, alguma variável não-ligada que foi ligada nos predicados unificados também ocorre em outros predicados nas duas cláusulas, então substitua pelos seus respectivos termos ligados.
• Descarte os predicados unificados, e combine o restante das duas cláusulas em uma nova cláusula.

Para aplicar essa regra no exemplo acima, nós encontramos o predicado ‘P’ na forma negada na primeira cláusula:

$\mathrm{\neg }$P(X)

E em forma não negada na segunda cláusula:

P(a)

X é uma variável livre, enquanto a é um átomo. Unificando os dois obtemos a substituição:

$\sigma$ = [(a,X)]

Descartando os predicados unificados, e aplicando a substituição dos predicados restantes (apenas Q(X), nesse caso), obtemos a conclusão:

Q(a)

Para um outro exemplo, considere a forma silogística:

Todos os políticos são corruptos.
Todos os corruptos são mentirosos.
Então todos os políticos são mentirosos.

Ou de maneira mais geral:

$\mathrm{\forall }$X P(X) implica Q(X)
$\mathrm{\forall }$X Q(X) implica R(X)
Então, $\mathrm{\forall }$X P(X) implica R(X)

Na FNC (Forma Normal Conjuntiva):

$\mathrm{\neg }$P(X) $\vee$ Q(X)
$\mathrm{\neg }$Q(Y) $\vee$ R(Y)

(Note que a variável na segunda cláusula foi renomeada para deixar claro que variáveis em cláusulas diferentes são distintas)

Agora, unificando Q(X) na primeira cláusula com Q(Y) na segunda cláusula temos que X e Y se tornam a mesma variável. Efetuando esta substituição nas cláusulas restantes e combinando-as, temos a conclusão:

$\mathrm{\neg }$P(X) $\vee$ R(X)

Mais exemplos

Lógica Proposicional

Exemplo 1

Socrátes e Platão

• Sócrates está em tal situação que ele estaria disposto a visitar Platão (S), só se Platão estivesse disposto a visitá-lo (P);

$(P\to S)$

• Platão está em tal situação que ele não estaria disposto a visitar Sócrates, se Sócrates estivesse disposto a visitá-lo;

$(S\to \mathrm{\neg }P)$

• Platão está em tal situação que ele estaria disposto a visitar Sócrates, se Sócrates não estivesse disposto a visitá-lo.

$(\mathrm{\neg }S\to P)$

• Pergunta-se:

Sócrates está disposto a visitar Platão ou não?

$(P\to S),(S\to \mathrm{\neg }P),(\mathrm{\neg }S\to P)\models S$

Transformação de $(P\to S)\wedge (S\to \mathrm{\neg }P)\wedge (\mathrm{\neg }S\to P)$ para a forma conjuntiva:

$P\to S\equiv \mathrm{\neg }P\vee S$

$S\to \mathrm{\neg }P\equiv \mathrm{\neg }S\vee \mathrm{\neg }P$

$\mathrm{\neg }S\to P\equiv S\vee P$

Temos então o seguinte conjunto de cláusulas:

$\{\{\mathrm{\neg }P,S\},\{\mathrm{\neg }S,\mathrm{\neg }P\},\{S,P\},\{\mathrm{\neg }S\}\}$

Resolução:

$\frac{\{\mathrm{\neg }S\}\{S,P\}}{\{P\}}$

$\frac{\{\mathrm{\neg }S\}\{\mathrm{\neg }P,S\}}{\{\mathrm{\neg }P\}}$

$\frac{\{P\}\{\mathrm{\neg }P\}}{\mathrm{\perp }}$

Portanto concluímos que Sócrates está disposto a visitar Platão.

Exemplo 2

Ana

• Se Anelise não for cantora (P) ou Anamélia for pianista(Q), então Anaís será professora (R).

$((\mathrm{\neg }P\vee Q)\to R)$

• Se Ana for atleta (S), então Anamélia será pianista (Q).

$(S\to Q)$

• Se Anelise for cantora (P), então Ana será atleta (S).

$(P\to S)$

• Anamélia não será pianista (Q).

$(\mathrm{\neg }Q)$

É possível concluir que Anaís é professora (R)?

$(\mathrm{\neg }P\vee Q)\to R,S\to Q,P\to S,\mathrm{\neg }Q\models R$

Transformação do conjunto de premissas para a forma conjuntiva:

$\mathrm{\neg }P\vee Q\to R$
$\equiv \mathrm{\neg }(\mathrm{\neg }P\vee Q)\vee R$
$\equiv (\mathrm{\neg }\mathrm{\neg }P\wedge \mathrm{\neg }Q)\vee R$
$\equiv (P\wedge \mathrm{\neg }Q)\vee R$
$\equiv (P\vee R)\wedge (\mathrm{\neg }Q\vee R)$

$S\to Q\equiv \mathrm{\neg }S\vee Q$

$P\to S\equiv \mathrm{\neg }P\vee S$

Temos então o seguinte conjunto de cláusulas:

$\{\{P,R\},\{\mathrm{\neg }Q,R\},\{\mathrm{\neg }S,Q\},\{\mathrm{\neg }P,S\},\{\mathrm{\neg }Q\},\{\mathrm{\neg }R\}\}$

Resolução:

$\frac{\{\mathrm{\neg }R\}\{P,R\}}{\{P\}}$

$\frac{\{P\}\{\mathrm{\neg }P,S\}}{\{S\}}$

$\frac{\{S\}\{\mathrm{\neg }S,Q\}}{\{Q\}}$

$\frac{\{Q\}\{\mathrm{\neg }Q\}}{\mathrm{\perp }}$

Concluimos, portanto, que Anaís é Professora.

Lógica de Primeira Ordem

Exemplo 1

Toda pessoa é sábia ou tucana. Zé não é tucano. Zé é sábio?

U = pessoas
I[q(x)] = T sse x é sábio
I[p(x)] = T sse x é tucana
I[a] = Zé

O que quero provar?? Toda pessoa é sábia ou tucana. Zé não é tucano. Zé é sábio?

$(\mathrm{\forall }x(p(x)\vee q(x))\wedge \mathrm{\neg }p(a))\to q(a)$

Por refutação:

$$\mathrm{\neg }(((\mathrm{\forall }x(p(x)\vee q(x))\wedge \mathrm{\neg }p(a))\to q(a))$$$$\equiv \mathrm{\neg }(\mathrm{\neg }((\mathrm{\forall }x(p(x)\vee q(x))\wedge \mathrm{\neg }p(a))\vee q(a))$$$$\equiv (\mathrm{\forall }x(p(x)\vee q(x))\wedge \mathrm{\neg }p(a))\wedge \mathrm{\neg }q(a)$$
$$\equiv \mathrm{\forall }x(p(x)\vee q(x))\wedge \mathrm{\neg }p(a)\wedge \mathrm{\neg }q(a)$$

Eliminamos o quantificador universal:

$(p(x)\vee q(x))\wedge \mathrm{\neg }p(a)\wedge \mathrm{\neg }q(a)$

Como é possível notar, a sentença já se encontra na forma normal clausal.

• Nota: A forma normal clausal é simplesmente o nome que recebe a forma normal

conjuntiva após passar pelo processo de conversão, skolemização e reorganização típicos da lógica de primeira ordem.

Temos então o conjunto de cláusulas:

$\{\{p(x),q(x)\},\{\mathrm{\neg }p(a)\},\{\mathrm{\neg }q(a)\}\}$

Agora aplicamos a resolução:

$\frac{\{p(x),q(x)\}\{\mathrm{\neg }p(a)\}}{\{q(a)\}}$ 
com $\sigma$1=[(x,a)]

$\frac{\{\mathrm{\neg }q(a)\}\{q(a)\}}{\mathrm{\perp }}$
com $\sigma$2=[(x,a)]

Chegamos então a uma cláusula vazia. Portanto, concluímos que se Zé não é Tucano então Zé é sábio.

Exemplo 2

Agora um exemplo mais direto e detalhado:

Seja a fórmula:

$P(x)\to \mathrm{\exists }.P(x)$

Vamos mostrar que existe uma refutação da negação desta fórmula:

Passo 1: Negar a fórmula

$\mathrm{\neg }(P(x)\to \mathrm{\exists }.P(x))$

Passo 2: Forma normal prenex

$\mathrm{\forall }y.\mathrm{\neg }(P(x)\to P(y))$

Passo 3: Fechar existencialmente da Fórmula

$\mathrm{\exists }x.\mathrm{\forall }y.\mathrm{\neg }(P(x)\to P(y))$

Passo 4: Skolemizar

$\mathrm{\forall }y.(P(a)\to P(y))$

Passo 5: Eliminação de quantificadores universais

$P(a)\to P(y)$

Passo 6: Forma normal conjuntiva

$\mathrm{\neg }(P(a)\to P(y))$
$\equiv \mathrm{\neg }(\mathrm{\neg }P(a)\vee P(y))$
$\equiv \mathrm{\neg }\mathrm{\neg }P(a)\wedge \mathrm{\neg }P(y)$
$\equiv P(a)\wedge \mathrm{\neg }P(y)$

Passo 7: Notação Clausal

$\{\{P(a)\},\{\mathrm{\neg }P(y)\}\}$

Passo 8: Resolução

$\frac{\{P(a)\}\{\mathrm{\neg }P(a)\}}{\mathrm{\perp }}$ com $\sigma$0 = [(a, y)]

Referências

• J. Alan Robinson (1965), A machine-oriented logic based on the resolution principle. Journal of the ACM, Volume 12, Issue 1, pp. 23–41.

Ver também

• Unificação
• Universo de Herbrand
• Skolemização
• Lógica de primeira ordem
• Lógica proposicional
• Forma normal clausal

Ligações externas

• Resolution Principle at MathWorld