decidível

Decidível é um termo usado na teoria da computação e na lógica para descrever a existência de uma solução algorítmica para um problema de decisão. Um problema de decisão é decidível quando existe um algoritmo que, para qualquer entrada admissível, encerra em tempo finito com a resposta sim ou não. Em termos de máquinas, isso equivale a existir uma máquina de Turing total que sempre encerra e produz a resposta correta.

Existem também problemas semi-decidíveis (ou recursivamente enumeráveis): nesses casos, pode-se construir um algoritmo que aceita exatamente as entradas que pertencem ao conjunto, mas ele pode não terminar para entradas que não pertencem. Um problema é indecidível quando não existe algoritmo que resolva todos os casos.

Exemplos: decidíveis: a verificação de primalidade de números naturais; o problema SAT (satisfatibilidade de fórmulas proposicionais) — que é decidível, embora seja NP-completo; indecidíveis: o problema da parada (Halting problem) para máquinas de Turing; a validade em lógica de primeira ordem é indecidível em geral.

Conceitos relacionados incluem conjuntos decidíveis, cujas funções características são computáveis. A decidibilidade determina o que pode ser resolvido automaticamente; exemplos clássicos ilustram as fronteiras: a aritmética de Presburger é decidível, enquanto o problema da parada é indecidível e a validade da lógica de primeira ordem em geral também é indecidível.