Resolução (lógica) - Resolution (logic)

Na lógica matemática e na prova automatizada de teoremas , a resolução é uma regra de inferência que leva a uma refutação completa da técnica de prova de teoremas para sentenças em lógica proposicional e lógica de primeira ordem . Para a lógica proposicional, a aplicação sistemática da regra de resolução atua como um procedimento de decisão para a insatisfabilidade da fórmula, resolvendo o (complemento do) problema de satisfatibilidade booleana . Para a lógica de primeira ordem , a resolução pode ser usada como base para um semi-algoritmo para o problema de insatisfação da lógica de primeira ordem , fornecendo um método mais prático do que um que segue o teorema da completude de Gödel .

A regra de resolução pode ser rastreada até Davis e Putnam (1960); no entanto, seu algoritmo exigia tentar todas as instâncias básicas da fórmula fornecida. Esta fonte de explosão combinatória foi eliminada em 1965 pelo algoritmo de unificação sintática de John Alan Robinson , que permitia instanciar a fórmula durante a prova "sob demanda" tanto quanto necessário para manter a integridade da refutação .

A cláusula produzida por uma regra de resolução é às vezes chamada de resolvente .

Resolução em lógica proposicional

Regra de resolução

A regra de resolução na lógica proposicional é uma única regra de inferência válida que produz uma nova cláusula implícita em duas cláusulas contendo literais complementares. Um literal é uma variável proposicional ou a negação de uma variável proposicional. Dois literais são considerados complementos se um for a negação do outro (a seguir, é considerado o complemento de ). A cláusula resultante contém todos os literais que não possuem complementos. Formalmente: ${\ displaystyle \ lnot c}$${\ displaystyle c}$

${\ displaystyle {\ frac {a_ {1} \ lor a_ {2} \ lor \ cdots \ lor c, \ quad b_ {1} \ lor b_ {2} \ lor \ cdots \ lor \ neg c} {a_ { 1} \ lor a_ {2} \ lor \ cdots \ lor b_ {1} \ lor b_ {2} \ lor \ cdots}}}$

Onde

todos , e são literais,${\ displaystyle a_ {i}}$${\ displaystyle b_ {i}}$${\ displaystyle c}$

a linha divisória significa " implica ".

O texto acima também pode ser escrito como:

${\ displaystyle {\ frac {(\ neg a_ {1} \ land \ neg a_ {2} \ land \ cdots) \ rightarrow c, \ quad c \ rightarrow (b_ {1} \ lor b_ {2} \ lor \ cdots)} {(\ neg a_ {1} \ land \ neg a_ {2} \ land \ cdots) \ rightarrow (b_ {1} \ lor b_ {2} \ lor \ cdots)}}}$

A cláusula produzida pela regra de resolução é chamada de resolvente das duas cláusulas de entrada. É o princípio do consenso aplicado a cláusulas ao invés de termos.

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 um desses pares; entretanto, o resultado é sempre uma tautologia .

O Modus ponens pode ser visto como um caso especial de resolução (de uma cláusula de um literal e uma cláusula de dois literais).

${\ displaystyle {\ frac {p \ rightarrow q, \ quad p} {q}}}$

é equivalente a

${\ displaystyle {\ frac {\ lnot p \ lor q, \ quad p} {q}}}$

Uma técnica de resolução

Quando combinada com um algoritmo de busca completo , a regra de resolução produz um algoritmo sólido e completo para decidir a satisfatibilidade de uma fórmula proposicional e, por extensão, a validade de uma 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 na lógica proposicional pode ser transformada em uma sentença equivalente na forma normal conjuntiva . As etapas são as seguintes.

• Todas as sentenças na base de conhecimento e a negação da sentença a ser provada (a conjectura ) estão conjuntivamente conectadas.
• A frase resultante é transformada em uma forma normal conjuntiva com os conjuntos vistos como elementos em um conjunto, S , de orações.
  • Por exemplo, dá origem ao conjunto .${\ displaystyle (A_ {1} \ lor A_ {2}) \ land (B_ {1} \ lor B_ {2} \ lor B_ {3}) \ land (C_ {1})}$${\ displaystyle S = \ {A_ {1} \ lor A_ {2}, B_ {1} \ lor B_ {2} \ lor B_ {3}, C_ {1} \}}$
• A regra de resolução é aplicada a todos os pares de cláusulas possíveis que contêm literais complementares. Após cada aplicação da regra de resolução, a sentença resultante é simplificada removendo literais repetidos. Se a cláusula contiver literais complementares, ela será descartada (como uma tautologia). Caso contrário, e se ainda não estiver presente no conjunto de cláusulas S , é adicionado a S e é considerado para futuras inferências de resolução.
• Se depois de aplicar uma regra de resolução a cláusula vazia for derivada, a fórmula original será insatisfatória (ou contraditória ) e, portanto, pode-se concluir que a conjectura inicial segue dos axiomas.
• 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 nenhuma cláusula nova, a conjectura não é um teorema da base de conhecimento original.

Uma instância desse algoritmo é o algoritmo Davis-Putnam original que foi posteriormente refinado no algoritmo DPLL que removeu a necessidade de representação explícita dos resolventes.

Esta descrição da técnica de resolução usa um conjunto S como a estrutura de dados subjacente para representar as derivações de resolução. Listas , árvores e gráficos acíclicos direcionados são outras alternativas possíveis e comuns. As representações em árvore são mais fiéis ao fato de que a regra de resolução é binária. Junto com uma notação sequente para cláusulas, uma representação em árvore também deixa claro como a regra de resolução está relacionada a um caso especial da regra de corte , restrita a fórmulas de corte atômicas. No entanto, as representações de árvore não são tão compactas quanto as representações de conjunto ou lista, porque mostram explicitamente subderivações redundantes de cláusulas que são usadas mais de uma vez na derivação da cláusula vazia. As representações de gráfico podem ser tão compactas no número de cláusulas quanto as representações de lista e também armazenam informações estruturais sobre quais cláusulas foram resolvidas para derivar cada resolvente.

Um exemplo simples

${\ displaystyle {\ frac {a \ vee b, \ quad \ neg a \ vee c} {b \ vee c}}}$

Em linguagem simples: suponha que seja falso. Para que a premissa seja verdadeira, deve ser verdadeira. Alternativamente, suponha que seja verdade. Para que a premissa seja verdadeira, deve ser verdadeira. Portanto, independentemente da falsidade ou veracidade de , se ambas as premissas forem válidas, a conclusão é verdadeira. ${\ displaystyle a}$${\ displaystyle a \ vee b}$${\ displaystyle b}$${\ displaystyle a}$${\ displaystyle \ neg a \ vee c}$${\ displaystyle c}$${\ displaystyle a}$${\ displaystyle b \ vee c}$

Resolução na lógica de primeira ordem

A regra de resolução pode ser generalizada para a lógica de primeira ordem para:

${\ displaystyle {\ frac {\ Gamma _ {1} \ cup \ left \ {L_ {1} \ right \} \, \, \, \, \ Gamma _ {2} \ cup \ left \ {L_ {2 } \ right \}} {(\ Gamma _ {1} \ cup \ Gamma _ {2}) \ phi}} \ phi}$

onde é um unificador mais geral de e , e e não têm variáveis ​​comuns. ${\ displaystyle \ phi}$${\ displaystyle L_ {1}}$${\ displaystyle {\ overline {L_ {2}}}}$${\ displaystyle \ Gamma _ {1}}$${\ displaystyle \ Gamma _ {2}}$

Exemplo

As cláusulas e podem aplicar esta regra como unificador. ${\ displaystyle P (x), Q (x)}$${\ displaystyle \ neg P (b)}$${\ displaystyle [b / x]}$

Aqui x é uma variável eb é uma constante.

${\ displaystyle {\ frac {P (x), Q (x) \, \, \, \, \ neg P (b)} {Q (b)}} [b / x]}$

Aqui vemos que

• As cláusulas e são as premissas da inferência${\ displaystyle P (x), Q (x)}$${\ displaystyle \ neg P (b)}$
• ${\ displaystyle Q (b)}$ (o resolvente das premissas) é sua conclusão.
• O literal é o literal resolvido à esquerda,${\ displaystyle P (x)}$
• O literal é o literal resolvido certo,${\ displaystyle \ neg P (b)}$
• ${\ displaystyle P}$ é o átomo ou pivô resolvido.
• ${\ displaystyle [b / x]}$ é o unificador mais geral dos literais resolvidos.

Explicação informal

Na lógica de primeira ordem, a resolução condensa os silogismos tradicionais de inferência lógica em uma única regra.

Para entender como a resolução funciona, considere o seguinte silogismo de exemplo de lógica de termos :

Todos os gregos são europeus.

Homer é grego.

Portanto, Homer é um europeu.

Ou, de forma mais geral:

${\ displaystyle \ forall xP (x) \ Rightarrow Q (x)}$

${\ displaystyle P (a)}$

Portanto, ${\ displaystyle Q (a)}$

Para reformular o raciocínio usando a técnica de resolução, primeiro as cláusulas devem ser convertidas para a forma normal conjuntiva (CNF). Desta forma, toda quantificação torna-se implícita: quantificadores universais em variáveis ​​( X , Y , ...) são simplesmente omitidos como entendidos, enquanto variáveis quantificadas existencialmente são substituídas por funções de Skolem .

${\ displaystyle \ neg P (x) \ vee Q (x)}$

${\ displaystyle P (a)}$

Portanto, ${\ displaystyle Q (a)}$

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

• Encontre duas cláusulas contendo o mesmo predicado, onde ele é negado em uma cláusula, mas não na outra.
• Realize uma unificação nos dois predicados. (Se a unificação falhar, você fez uma escolha incorreta de predicados. Volte para a etapa anterior e tente novamente.)
• Se quaisquer variáveis ​​não ligadas que foram ligadas nos predicados unificados também ocorrerem em outros predicados nas duas cláusulas, substitua-as por seus valores ligados (termos) lá também.
• Descarte os predicados unificados e combine os restantes das duas cláusulas em uma nova cláusula, também unida pelo operador "∨".

Para aplicar esta regra ao exemplo acima, encontramos que o predicado P ocorre na forma negada

¬ P ( X )

na primeira cláusula, e na forma não negada

P ( a )

na segunda cláusula. X é uma variável não vinculada, enquanto a é um valor vinculado (termo). Unificar os dois produz a substituição

X ↦ a

Descartar os predicados unificados e aplicar essa substituição aos predicados restantes (apenas Q ( X ), neste caso), produz a conclusão:

Q ( a )

Para outro exemplo, considere a forma silogística

Todos os cretenses são ilhéus.

Todos os ilhéus são mentirosos.

Portanto, todos os cretenses são mentirosos.

Ou mais geralmente,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

Portanto, ∀ X P ( X ) → R ( X )

No CNF, os antecedentes tornam-se:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

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

Agora, unificar Q ( X ) na primeira cláusula com ¬ Q ( Y ) na segunda cláusula significa que X e Y se tornam a mesma variável de qualquer maneira. Substituir isso nas cláusulas restantes e combiná-las dá a conclusão:

¬ P ( X ) ∨ R ( X )

Factoring

A regra de resolução, conforme definida por Robinson, também incorporou a factoring, que unifica dois literais na mesma cláusula, antes ou durante a aplicação da resolução conforme definido acima. A regra de inferência resultante é refutação completa, em que um conjunto de cláusulas é insatisfatório se e somente se houver uma derivação da cláusula vazia usando apenas resolução, aprimorada por fatoração.

Um exemplo de uma cláusula insatisfatória definida para a qual a fatoração é necessária para derivar a cláusula vazia é:

${\ displaystyle {\ begin {array} {rlcl} (1): & P (u) & \ lor & P (f (u)) \\ (2): & \ lnot P (v) & \ lor & P (f ( w)) \\ (3): & \ lnão P (x) & \ lor & \ lnão P (f (x)) \\\ end {array}}}$

Uma vez que cada cláusula consiste em dois literais, o mesmo ocorre com cada resolvente possível. Portanto, por resolução sem fatoração, a cláusula vazia nunca pode ser obtida. Usando fatoração, pode ser obtido, por exemplo, da seguinte forma:

${\ displaystyle {\ begin {array} {rll} (4): & P (u) \ lor P (f (w)) & {\ text {resolvendo (1) e (2), com}} v = f (u) \\ (5): & P (f (w)) & {\ text {fatorando (4), com}} u = f (w) \\ (6): & \ lnão P (f (f (w '))) & {\ text {resolvendo (5) e (3), com}} w = w', x = f (w ') \\ (7): & {\ text {false}} & {\ text {resolvendo (5) e (6), com}} w = f (w ') \\\ end {array}}}$

Resolução não cláusula

Foram elaboradas generalizações da regra de resolução acima, que não exigem que as fórmulas originárias estejam na forma oracional normal .

Essas técnicas são úteis principalmente na prova de teoremas interativos onde é importante preservar a legibilidade humana das fórmulas de resultados intermediários. Além disso, eles evitam a explosão combinatória durante a transformação para a forma de cláusula e, às vezes, economizam etapas de resolução.

Resolução não oracional na lógica proposicional

Para lógica proposicional, Murray, Manna e Waldinger usam a regra

${\ displaystyle {\ begin {array} {c} F [p] \; \; \; \; \; \; \; \; \; \; G [p] \\\ hline F [{\ textit { true}}] \ lor G [{\ textit {false}}] \\\ end {array}}}$,

onde denota uma fórmula arbitrária, denota uma fórmula contendo como uma subfórmula e é construída substituindo em cada ocorrência de por ; da mesma forma para . O resolvente se destina a ser simplificado usando regras como , etc. Para evitar a geração de resolventes triviais inúteis, a regra deve ser aplicada apenas quando tem pelo menos uma ocorrência "negativa" e "positiva" em e , respectivamente. Murray mostrou que essa regra é completa se aumentada por regras de transformação lógica apropriadas. ${\ displaystyle p}$${\ displaystyle F [p]}$${\ displaystyle p}$${\ displaystyle F [{\ textit {true}}]}$${\ displaystyle F [p]}$${\ displaystyle p}$${\ displaystyle {\ textit {true}}}$${\ displaystyle G}$${\ displaystyle F [{\ textit {true}}] \ lor G [{\ textit {false}}]}$${\ displaystyle q \ land {\ textit {true}} \ implica q}$${\ displaystyle p}$${\ displaystyle F}$${\ displaystyle G}$

Traugott usa a regra

${\ displaystyle {\ begin {array} {c} F [p ^ {+}, p ^ {-}] \; \; \; \; \; \; \; \; G [p] \\\ hline F [G [{\ textit {true}}], \ lnot G [{\ textit {false}}]] \\\ end {array}}}$,

onde os expoentes de indicam a polaridade de suas ocorrências. Enquanto e são construídos como antes, a fórmula é obtida substituindo cada ocorrência positiva e cada ocorrência negativa de in por e , respectivamente. Semelhante à abordagem de Murray, as transformações de simplificação apropriadas devem ser aplicadas ao resolvente. Traugott provou que sua regra é completa, desde que sejam os únicos conectivos usados ​​nas fórmulas. ${\ displaystyle p}$${\ displaystyle G [{\ textit {true}}]}$${\ displaystyle G [{\ textit {false}}]}$${\ displaystyle F [G [{\ textit {true}}], \ lnot G [{\ textit {false}}]]}$${\ displaystyle p}$${\ displaystyle F}$${\ displaystyle G [{\ textit {true}}]}$${\ displaystyle G [{\ textit {false}}]}$${\ displaystyle \ land, \ lor, \ rightarrow, \ lnot}$

O resolvente de Traugott é mais forte do que o de Murray. Além disso, não introduz novos juntadores binários, evitando assim uma tendência à forma oracional em resolução repetida. No entanto, as fórmulas podem crescer mais quando um pequeno é substituído várias vezes por um maior e / ou . ${\ displaystyle p}$${\ displaystyle G [{\ textit {true}}]}$${\ displaystyle G [{\ textit {false}}]}$

Exemplo de resolução proposicional de não cláusula

Por exemplo, partindo das premissas fornecidas pelo usuário

${\ displaystyle {\ begin {array} {rccc} (1): & a & \ rightarrow & b \ land c \\ (2): & c & \ rightarrow & d \\ (3): & b \ land d & \ rightarrow & e \\ (4 ): & \ lnot (a & \ rightarrow & e) \\\ end {array}}}$

a regra de Murray pode ser usada da seguinte maneira para inferir uma contradição:

${\ displaystyle {\ begin {array} {rrclccl} (5): & ({\ textit {true}} \ rightarrow d) & \ lor & (a \ rightarrow b \ land {\ textit {false}}) & \ implica & d \ lor \ lnot a & {\ mbox {de (2) e (1), com}} p = c \\ (6): & (b \ land {\ textit {true}} \ rightarrow e) & \ lor & ({\ textit {false}} \ lor \ lnot a) & \ implica & (b \ rightarrow e) \ lor \ lnot a & {\ mbox {de (3) e (5), com}} p = d \\ (7): & (({\ textit {true}} \ rightarrow e) \ lor \ lnot a) & \ lor & (a \ rightarrow {\ textit {false}} \ land c) & \ implica & e \ lor \ lnot a \ lor \ lnot a & {\ mbox {de (6) e (1), com}} p = b \\ (8): & (e \ lor \ lnot {\ textit {true}} \ lor \ lnot {\ textit {true}}) & \ lor & \ lnot ({\ textit {false}} \ rightarrow e) & \ implica & e & {\ mbox {de (7) e (4), com}} p = a \\ (9): & \ lnot (a \ rightarrow {\ textit {true}}) & \ lor & {\ textit {false}} & \ implica & {\ textit {false}} & {\ mbox {from (4) e (8), com}} p = e \\\ end {array}}}$

Para o mesmo propósito, a regra Traugott pode ser usada da seguinte forma:

${\ displaystyle {\ begin {array} {rcccl} (10): & a \ rightarrow b \ land ({\ textit {true}} \ rightarrow d) & \ implica & a \ rightarrow b \ land d & {\ mbox {from ( 1) e (2), com}} p = c \\ (11): & a \ rightarrow ({\ textit {true}} \ rightarrow e) & \ implica & a \ rightarrow e & {\ mbox {de (10) e (3), com}} p = (b \ land d) \\ (12): & \ lnot {\ textit {true}} & \ implica & {\ textit {false}} & {\ mbox {de (11 ) e (4), com}} p = (a \ rightarrow e) \\\ end {array}}}$

A partir de uma comparação de ambas as deduções, os seguintes problemas podem ser vistos:

• A regra de Traugott pode produzir um resolvente mais nítido: compare (5) e (10), que ambos resolvem (1) e (2) .${\ displaystyle p = c}$
• A regra de Murray introduziu 3 novos símbolos de disjunção: em (5), (6) e (7), enquanto a regra de Traugott não introduziu nenhum novo símbolo; nesse sentido, as fórmulas intermediárias de Traugott se assemelham mais ao estilo do usuário do que as de Murray.
• Devido a este último aspecto, a regra de Traugott pode tirar vantagem da implicação na suposição (4), utilizando-se como a fórmula não-atómico no passo (12). Usando as regras de Murray, a fórmula semanticamente equivalente foi obtida como (7), entretanto, ela não poderia ser usada devido à sua forma sintática.${\ displaystyle p}$ ${\ displaystyle a \ rightarrow e}$${\ displaystyle e \ lor \ lnot a \ lor \ lnot a}$${\ displaystyle p}$

Resolução não oracional na lógica de primeira ordem

Para a lógica de predicados de primeira ordem, a regra de Murray é generalizada para permitir subfórmulas distintas, mas unificáveis, e de e , respectivamente. Se for o unificador mais geral de e , então o resolvente generalizado é . Embora a regra permaneça válida se uma substituição mais especial for usada, nenhum desses aplicativos de regra é necessário para atingir a integridade. ${\ displaystyle p_ {1}}$${\ displaystyle p_ {2}}$${\ displaystyle F}$${\ displaystyle G}$${\ displaystyle \ phi}$${\ displaystyle p_ {1}}$${\ displaystyle p_ {2}}$${\ displaystyle F \ phi [{\ textit {true}}] \ lor G \ phi [{\ textit {false}}]}$${\ displaystyle \ phi}$

A regra de Traugott é generalizada para permitir várias subfórmulas distintas entre pares de e de , contanto que tenham um unificador mais comum, digamos . O resolvente generalizado é obtido após a aplicação das fórmulas parentais, tornando a versão proposicional aplicável. A prova de integridade de Traugott se baseia na suposição de que essa regra totalmente geral é usada; não está claro se sua regra permaneceria completa se restrita a e . ${\ displaystyle p_ {1}, \ ldots, p_ {m}}$${\ displaystyle F}$${\ displaystyle p_ {m + 1}, \ ldots, p_ {n}}$${\ displaystyle G}$${\ displaystyle p_ {1}, \ ldots, p_ {n}}$${\ displaystyle \ phi}$${\ displaystyle \ phi}$${\ displaystyle p_ {1} = \ cdots = p_ {m}}$${\ displaystyle p_ {m + 1} = \ cdots = p_ {n}}$

Paramodulação

Paramodulação é uma técnica relacionada para raciocinar em conjuntos de cláusulas onde o símbolo do predicado é a igualdade. Ele gera todas as versões "iguais" de cláusulas, exceto identidades reflexivas. A operação de paramodulação leva um positivo da cláusula, que deve conter um literal de igualdade. Em seguida, procura uma cláusula into com um subtermo que se une a um lado da igualdade. O subtermo é então substituído pelo outro lado da igualdade. O objetivo geral da paramodulação é reduzir o sistema a átomos, reduzindo o tamanho dos termos durante a substituição.

Implementações

• CARINE
• GKC
• Lontra
• Provérbio 9
• SNARK
• SPASS
• Vampiro
• Provador online Logictools

Veja também

• Desapego condensado  - uma versão anterior de resolução
• Programação lógica indutiva
• Resolução inversa
• Programação lógica
• Método de tableaux analíticos
• Resolução SLD
• Inferência de resolução

Notas

Referências

• Robinson , J. Alan (1965). "Uma lógica orientada à máquina baseada no princípio de resolução". Jornal do ACM . 12 (1): 23–41. doi : 10.1145 / 321250.321253 .
• Leitsch, Alexander (1997). O cálculo de resolução . Springer .
• Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving . Editores Harper & Row .
• Lee, Chin-Liang Chang, Richard Char-Tung (1987). Lógica simbólica e prova de teorema mecânico ([reimpressão] ed.). San Diego: Academic Press. ISBN 0-12-170350-9.

links externos

• Alex Sakharov. “Princípio da Resolução” . MathWorld .
• Alex Sakharov. "Resolução" . MathWorld .