Un algoritmo o mecanismo determinista que, para cada fórmula de entrada en una teoría lógica o fragmento especificado, termina y declara correctamente si la fórmula es satisfacible (o pertenece a la teoría), conforme a garantías de exactitud y completitud para ese fragmento.

Principio

Restringir el lenguaje o la teoría a un fragmento decidible y diseñar reglas o algoritmos terminantes y correctos (a menudo mediante formas normales, construcciones de autómatas, cierre de congruencia, eliminación de cuantificadores o tableau) que exploren de manera exhaustiva el espacio de búsqueda en recursos finitos.

Demostración

Un procedimiento de decisión para igualdad con funciones no interpretadas (EUF) implementado mediante cierre de congruencia decide de forma determinista si un conjunto de igualdades y desigualdades es satisfacible manteniendo clases de equivalencia y propagando uniones hasta que se deriva una contradicción o se construye un modelo.

Aplicación incorrecta

Aplicar un procedimiento de decisión fuera de su fragmento declarado (por ejemplo, usar un procedimiento de Presburger en fórmulas con multiplicación de variables cuantificadas) puede llevar a no terminación o respuestas incorrectas; tratar un solucionador incompleto como procedimiento de decisión provoca aceptar indebidamente afirmaciones de satisfacibilidad.

Consecuencia

Cuando existe para una teoría, un procedimiento de decisión permite componentes modulares de razonamiento en sistemas mayores (p. ej. solucionadores SMT), proporciona garantías automatizadas de corrección para ese fragmento y permite la automatización completa de tareas de verificación expresables en el fragmento.

Inversión

La inversión es un método indecidible o semi-decidible que puede no terminar en todas las entradas o devolver solo respuestas parciales (p. ej. búsqueda enumerativa o solucionadores heurísticos); tales métodos sacrifican completitud y terminación por una aplicabilidad más amplia.

Límite

Se aplica a algoritmos con terminación y corrección probadas sobre un fragmento lógico o teoría claramente especificados. Excluye heurísticas, aproximaciones, procedimientos semi-decidibles que puedan divergir y métodos que solo producen respuestas probables o estadísticas.

Tensión semántica

Hay tensión entre la generalidad del fragmento lógico (fragmentos más amplios suelen ser indecidibles) y la tratabilidad algorítmica; también hay tensión entre construir un procedimiento completamente decisorio pero potencialmente costoso y usar heurísticas incompletas y rápidas en la práctica.

Síntesis

Un procedimiento de decisión es un algoritmo formalmente especificado, ajustado a un fragmento decidible, que garantiza terminación y respuestas correctas sí/no sobre satisfacibilidad, logrando esto mediante la restricción de expresividad y el uso de técnicas simbólicas o basadas en autómatas que agotan el espacio de búsqueda del fragmento.