Satisfatibilidade

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Ambox rewrite.svg
Esta página precisa ser reciclada de acordo com o livro de estilo (desde agosto de 2011).
Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.

Na lógica matemática, satisfatibilidade e validade são conceitos elementares da semântica. Uma fórmula é satisfatível se é possível achar uma interpretação ( modelo) que torne a fórmula verdadeira.[1] Uma fórmula é válida se todas as interpretações tornam a fórmula verdadeira. Os opostos deste conceito são insatisfatibilidade e invalidade, isto é, uma fórmula é insatisfatível se nenhuma das interpretações tornam a fórmula verdadeira, e inválida se alguma dessas interpretações tornam a fórmula falsa. Estes quatro conceitos etsão relacionados uns aos outros de maneira exatamente análoga ao quadrado das oposições de Aristóteles.

Os quatro conceitos podem ser usados para aplicar todas as teorias: uma teoria é satisfatível (válida) se uma (todas) as interpretações torna(m) cada um dos axiomas da teoria verdade, e a teoria é insatisfatível (inválida) se todas (uma) as interpretações tornam(a) cada um dos axiomas da teoria falso.

Também é possível considerar apenas as interpretações que tornam todos os axiomas de uma segunda teoria verdadeiros. Esta generalização é comumente chamada satisfatibilidade módulo teorias.

A questão de saber se uma sentença em uma proposição lógica é satisfatíval é um problema de decisão. Em geral, a questão de saber se sentenças em lógica de primeira ordemm são satisfeitas não é decidível. Na álgebra universal e teoria das equações, os métodos de reescrita de termos, fecho de congruência e unificação são usados para tentar decidir satisfatibilidade. Uma teoria particular é decidida ou não depende se a teoria é livre de variável ou está em outras condições.[2]

Redução de validade para satisfatibilidade[editar | editar código-fonte]

Para a lógica clássica, geralmente é possível reexpressar a questão da validade da fórmula para uma envolvendo satisfatibilidade, por causa da relação entre os conceitos expressados acima, no quadrado das oposições. Em particular φ é válido se e somente se ¬φ é insatisfatível, o que significa dizer que não é verdade que ¬φ é satisfatível. Por outro lado, φ é satisfatível se e somente se ¬φ é inválida.

Para lógica sem negação, tal como o cálculo proposicional positivo, as questões de validade e satisfatibilidade não devem estar relacionadas. No caso do cálculo proposicional positivo, o problema da satisfatibilidade é trivial, pois toda fórmula é satisfatível, enquanto o problema da validade é co-NP completo.

Satisfatibilidade proposicional[editar | editar código-fonte]

Principal Propositional_satisfiability

No caso da lógica proposicional clássica, satisfatibilidade é decidível para fómulas proposicionais. Em particular, satisfatibilidade é um problema NP-completo, e é um dos problemas mais intensamente estudados na teoria da complexidade computacional.

Satisfatibilidade em lógica de primeira ordem[editar | editar código-fonte]

Satisfatibilidade é indecidível e de fato nem sequer é uma propriedade das fómulas na lógica de primeira ordem (LPO), Este fato tem a ver com a indecidibilidade do problema da validade para LPO. A validade universal da fórmula é um problema semi-decidível. Se satisfatibilidade também fosse um problema semi-decidível, então o problema da exsitência de contramodelos deveria ser também (uma fórmula tem contramodelos se sua negação é satisfeita). Então o problema da validade lógica seria decidível, o que contradiz a tese de Church-Turing.

Satisfatibilidade na teoria dos modelos[editar | editar código-fonte]

Na teoria dos modelos, uma formula atômica é satisfatível se existe uma coleção de elementos da estrutura que tornam a fórmula verdadeira.[3] Se A é uma estrutura, φ é uma fórmula, e a é uma coleção de elementos, tirados da estrutura, que satisfazem φ. Comumente é escrito assim

A ⊧ φ [a]

Se φ não possui variáveis, isto é, φ é uma sentença atômica, e é satisfeita por A, então escreve-se

A ⊧ φ

Neste caso, pode se dizer também que A é um modelo para φ, ou que φ é verdadeiro em A. Se T é uma coleção de sentenças atômicas (uma teoria) satisfeita por A, se escreve

A ⊧ T

Notas[editar | editar código-fonte]

  1. See, for example, Boolos and Jeffrey, 1974, chapter 11.
  2. Term Rewriting and All That. [S.l.]: Cambridge University Press, 1998. 58-92 pp. ISBN 0521779200
  3. A Shorter Model Theory. [S.l.]: Cambridge University Press, 1997. 12 pp. ISBN 0521587131

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

  • Boolos and Jeffrey, 1974. Computability and Logic. Cambridge University Press.