Princípio da resolução

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[editar | editar código-fonte]

Regra de resolução[editar | editar código-fonte]

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 and 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[editar | editar código-fonte]

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:

\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:

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

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[editar | editar código-fonte]

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:

\forallX.(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.

\negP(X) \vee Q(X)
P(a) 
Então, Q(a)

Então a questão é, como a técnica de resolução deriva a ultima 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:

\negP(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:

\forallX P(X) implica Q(X)
\forallX Q(X) implica R(X)
Então, \forallX P(X) implica R(X)

Na FNC (Forma Normal Conjuntiva):

\negP(X) \vee Q(X)
\negQ(Y) \vee R(Y)

(Note que a variável na segunda cláusula foi renomeada pra 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:

\negP(X) \vee R(X)

Mais exemplos[editar | editar código-fonte]

Lógica Proposicional[editar | editar código-fonte]

Exemplo 1[editar | editar código-fonte]

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:

P \rightarrow S \quad \equiv \quad \neg P \vee S
S \rightarrow \neg P \quad \equiv \quad \neg S \vee \neg P
\neg S \rightarrow P \quad \equiv \quad S \vee P

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

\{\{\neg P, S\},\{\neg S, \neg P\},\{S, P\},\{\neg S\}\}

Resolução:

\frac{\{\neg S\} \qquad \{S, P\}}{\{P\}}
\frac{\{\neg S\} \qquad \{\neg P, S\}}{\{\neg P\}} 
\frac{\{P\} \qquad \{\neg P\}}{\bot}

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

Exemplo 2[editar | editar código-fonte]

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:

\neg P \vee Q \rightarrow R
\equiv \neg (\neg P \vee Q) \vee R
\equiv (\neg \neg P \wedge \neg Q) \vee R
\equiv (P \wedge \neg Q) \vee R
\equiv (P \vee R) \wedge (\neg Q \vee R)
S \rightarrow Q \quad \equiv \quad \neg S \vee Q
P \rightarrow S \quad \equiv \quad \neg P \vee S 

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

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


Resolução:

\frac{\{\neg R\} \quad \{P, R\}}{\{P\}}
\frac{\{P\} \quad \{\neg P, S\}}{\{S\}}
\frac{\{S\} \quad \{\neg S, Q\}}{\{Q\}}
\frac{\{Q\} \quad \{\neg Q\}}{\bot}

Concluimos, portanto, que Anaís é Professora.

Lógica de Primeira Ordem[editar | editar código-fonte]

Exemplo 1[editar | editar código-fonte]

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?

\forall x (p(x) \vee q(x)) \wedge \neg p(a)\rightarrow q(a)

Por refutação:

\neg (\forall x (p(x) \vee q(x)) \wedge \neg p(a)\rightarrow q(a))
\equiv \neg (\neg (\forall x (p(x) \vee q(x)) \wedge \neg p(a)) \vee q(a))
\equiv \forall x (p(x) \vee q(x)) \wedge \neg p(a) \vee q(a)
\equiv \forall x (p(x) \vee q(x)) \wedge \neg p(a) \wedge \neg q(a)

Eliminamos o quantificador universal:

(p(x) \vee q(x)) \wedge \neg p(a) \wedge \neg q(a)

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

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)\}, \{\neg p(a)\}, \{\neg q(a)\}\}

Agora aplicamos a resolução:

\frac{\{p(x),q(x)\}\quad \{\neg p(a)\}}{\{q(a)\}} 
com \sigma1=[(x,a)]
\frac{\{\neg q(a)\}\quad \{q(a)\}}{\bot}
com \sigma2=[(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[editar | editar código-fonte]

Agora um exemplo mais direto e detalhado:

Seja a fómula:

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

\neg (P(x) \rightarrow \exists .P(x))

Passo 2: Forma normal prenex

\forall y. \neg (P(x) \rightarrow P(y))

Passo 3: Fechar existencialmente da Fórmula

\exist x. \forall y. \neg (P(x) \rightarrow P(y))

Passo 4: Skolemizar

\forall y.(P(a) \rightarrow P(y))

Passo 5: Eliminação de quantificadores universais

P(a) \rightarrow P(y)

Passo 6: Forma normal conjuntiva

\neg (P(a) \rightarrow P(y))
\equiv \neg (\neg P(a) \vee P(y))
\equiv \neg \neg P(a) \wedge \neg P(y)
\equiv P(a) \wedge \neg P(y)

Passo 7: Notação Cláusal

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

Passo 8: Resolução

\frac{\{P(a)\} \quad \{\neg P(a)\}}{\bot}\qquad com \sigma0 = [(a, y)]

Referências[editar | editar código-fonte]

  • 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[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]