Loading AI tools
Da Wikipédia, a enciclopédia livre
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.
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 e são literais complementares:
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:
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 um conjunto de cláusulas e representamos por a cláusula vazia, . Aplica-se então a regra de inferência:
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 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:
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.
P(X) 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:
Para aplicar essa regra no exemplo acima, nós encontramos o predicado ‘P’ na forma negada na primeira cláusula:
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:
= [(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:
X P(X) implica Q(X) X Q(X) implica R(X) Então, X P(X) implica R(X)
Na FNC (Forma Normal Conjuntiva):
P(X) Q(X) Q(Y) 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:
P(X) R(X)
Socrátes e Platão
Sócrates está disposto a visitar Platão ou não?
Transformação de 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.
Ana
É possível concluir que Anaís é professora (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.
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?
Por refutação:
Eliminamos o quantificador universal:
Como é possível 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:
Agora aplicamos a resolução:
com 1=[(x,a)]
com 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:
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
com 0 = [(a, y)]
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.