Princípio da 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 ${\displaystyle a_{i}}$ e ${\displaystyle b_{j}}$ são literais complementares:

$${\displaystyle {\frac {a_{1}\lor \ldots \vee a_{i-1}\vee a_{i}\vee a_{i+1}\vee \ldots \lor a_{n},\quad b_{1}\lor \ldots \vee b_{j-1}\vee b_{j}\vee b_{j+1}\vee \ldots \lor b_{m}}{a_{1}\lor \ldots \lor a_{i-1}\lor a_{i+1}\lor \ldots \lor a_{n}\lor b_{1}\lor \ldots \lor b_{j-1}\lor b_{j+1}\lor \ldots \lor 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.

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:

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

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

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

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

• ${\displaystyle {\frac {\{C,p\}\quad \{C',\neg p\}}{\{C,C'\}}}}$

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.

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);

${\displaystyle (P\rightarrow 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;

${\displaystyle (S\rightarrow \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.

${\displaystyle (\neg S\rightarrow P)}$

• Pergunta-se:

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

${\displaystyle (P\rightarrow S),(S\rightarrow \neg P),(\neg S\rightarrow P)\models S}$

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

${\displaystyle P\rightarrow S\quad \equiv \quad \neg P\vee S}$

${\displaystyle S\rightarrow \neg P\quad \equiv \quad \neg S\vee \neg P}$

${\displaystyle \neg S\rightarrow P\quad \equiv \quad S\vee P}$

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

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

Resolução:

${\displaystyle {\frac {\{\neg S\}\qquad \{S,P\}}{\{P\}}}}$

${\displaystyle {\frac {\{\neg S\}\qquad \{\neg P,S\}}{\{\neg P\}}}}$

${\displaystyle {\frac {\{P\}\qquad \{\neg P\}}{\bot }}}$

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

Ana

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

${\displaystyle ((\neg P\vee Q)\rightarrow R)}$

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

${\displaystyle (S\rightarrow Q)}$

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

${\displaystyle (P\rightarrow S)}$

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

${\displaystyle (\neg Q)}$

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

${\displaystyle (\neg P\vee Q)\rightarrow R,S\rightarrow Q,P\rightarrow S,\neg Q\models R}$

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

${\displaystyle \neg P\vee Q\rightarrow R}$
${\displaystyle \equiv \neg (\neg P\vee Q)\vee R}$
${\displaystyle \equiv (\neg \neg P\wedge \neg Q)\vee R}$
${\displaystyle \equiv (P\wedge \neg Q)\vee R}$
${\displaystyle \equiv (P\vee R)\wedge (\neg Q\vee R)}$

${\displaystyle S\rightarrow Q\quad \equiv \quad \neg S\vee Q}$

${\displaystyle P\rightarrow S\quad \equiv \quad \neg P\vee S}$

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

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

Resolução:

${\displaystyle {\frac {\{\neg R\}\quad \{P,R\}}{\{P\}}}}$

${\displaystyle {\frac {\{P\}\quad \{\neg P,S\}}{\{S\}}}}$

${\displaystyle {\frac {\{S\}\quad \{\neg S,Q\}}{\{Q\}}}}$

${\displaystyle {\frac {\{Q\}\quad \{\neg Q\}}{\bot }}}$

Concluimos, portanto, que Anaís é Professora.

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?

${\displaystyle (\forall x(p(x)\vee q(x))\wedge \neg p(a))\rightarrow q(a)}$

Por refutação:

$${\displaystyle \neg (((\forall x(p(x)\vee q(x))\wedge \neg p(a))\rightarrow q(a))}$$

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

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

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

Eliminamos o quantificador universal:

${\displaystyle (p(x)\vee q(x))\wedge \neg p(a)\wedge \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:

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

Agora aplicamos a resolução:

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

${\displaystyle {\frac {\{\neg q(a)\}\quad \{q(a)\}}{\bot }}}$
com ${\displaystyle \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.

Agora um exemplo mais direto e detalhado:

Seja a fórmula:

${\displaystyle P(x)\rightarrow \exists .P(x)}$

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

Passo 1: Negar a fórmula

${\displaystyle \neg (P(x)\rightarrow \exists .P(x))}$

Passo 2: Forma normal prenex

${\displaystyle \forall y.\neg (P(x)\rightarrow P(y))}$

Passo 3: Fechar existencialmente da Fórmula

${\displaystyle \exists x.\forall y.\neg (P(x)\rightarrow P(y))}$

Passo 4: Skolemizar

${\displaystyle \forall y.(P(a)\rightarrow P(y))}$

Passo 5: Eliminação de quantificadores universais

${\displaystyle P(a)\rightarrow P(y)}$

Passo 6: Forma normal conjuntiva

${\displaystyle \neg (P(a)\rightarrow P(y))}$
${\displaystyle \equiv \neg (\neg P(a)\vee P(y))}$
${\displaystyle \equiv \neg \neg P(a)\wedge \neg P(y)}$
${\displaystyle \equiv P(a)\wedge \neg P(y)}$

Passo 7: Notação Clausal

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

Passo 8: Resolução

${\displaystyle {\frac {\{P(a)\}\quad \{\neg P(a)\}}{\bot }}\qquad }$ com ${\displaystyle \sigma }$0 = [(a, y)]