Procedimiento de Decisión

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.