# 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}\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.

### 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:
Que pode ser vista como um conjunto de cláusulas:
Seja $C$ um conjunto de cláusulas e representamos por $\bot$ a cláusula vazia, $\{\}$. Aplica-se então a regra de inferência:
* ${\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.

## 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:
Ou de maneira mais geral:
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.
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:
E em forma não negada na segunda cláusula:
X é uma variável livre, enquanto a é um átomo. Unificando os dois obtemos a substituição:
Descartando os predicados unificados, e aplicando a substituição dos predicados restantes (apenas Q(X), nesse caso), obtemos a conclusão:
Para um outro exemplo, considere a forma silogística:
Ou de maneira mais geral:
Na FNC (Forma Normal Conjuntiva):
(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:

## 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\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;
$(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.
$(\neg S\rightarrow P)$
* Pergunta-se:
Sócrates está disposto a visitar Platão ou não?
$(P\rightarrow S),(S\rightarrow \neg P),(\neg S\rightarrow P)\models S$
Transformação de $(P\rightarrow S)\wedge (S\rightarrow \neg P)\wedge (\neg S\rightarrow P)$ para a forma conjuntiva:
Temos então o seguinte conjunto de cláusulas:
Resolução:
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).
$((\neg P\vee Q)\rightarrow R)$
* Se Ana for atleta (S), então Anamélia será pianista (Q).
$(S\rightarrow Q)$
* Se Anelise for cantora (P), então Ana será atleta (S).
$(P\rightarrow S)$
* Anamélia não será pianista (Q).
$(\neg Q)$
É possível concluir que Anaís é professora (R)?
$(\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:
Temos então o seguinte conjunto de cláusulas:
Resolução:
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?
O que quero provar?? Toda pessoa é sábia ou tucana. Zé não é tucano. Zé é sábio?
Por refutação:
Eliminamos o quantificador universal:
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:
Agora aplicamos a resolução:
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:
Vamos mostrar que existe uma refutação da negação desta fórmula:
Passo 1: Negar a fórmula
Passo 2: Forma normal prenex
Passo 3: Fechar existencialmente da Fórmula
Passo 4: Skolemizar
Passo 5: Eliminação de quantificadores universais
Passo 6: Forma normal conjuntiva
Passo 7: Notação Clausal
Passo 8: Resolução