Un mecanismo general de inferencia que aplica repetidamente reglas de inferencia a un conjunto de fórmulas o cláusulas hasta que no pueden derivarse nuevas consecuencias (punto fijo) o se produce una contradicción, utilizado habitualmente en demostración automática y razonamiento automatizado.

Principio

Aplicar exhaustivamente las reglas de inferencia aplicables a la base de conocimiento actual, añadir las nuevas consecuencias y continuar hasta el cierre; la corrección y terminación dependen del conjunto de reglas, ordenación y estrategias (p. ej., eliminación de redundancias).

Demostración

En razonamiento basado en cláusulas, un procedimiento de saturación ejecuta pasos de resolución y simplificación sobre un conjunto inicial de cláusulas, añadiendo resolventes y simplificando, hasta que se deriva la cláusula vacía (contradicción) o no quedan resolventes novedosos según la estrategia elegida.

Aplicación incorrecta

Ejecutar la saturación sin control de redundancia, ordenación o estrategias de selección puede generar rápidamente un número intratable de consecuencias y hacer explotar memoria y tiempo, volviendo la saturación ingenua impracticable para teorías complejas.

Consecuencia

Cuando se controla eficazmente (mediante subsunción, ordenaciones de términos y heurísticas), la saturación proporciona búsqueda de prueba completa para muchas lógicas y soporta la adición incremental de axiomas manteniendo las consecuencias derivadas.

Inversión

El revés es la búsqueda dirigida por objetivos (top-down) que trabaja hacia atrás desde una fórmula objetivo en lugar de agotar consecuencias hacia adelante; puede ser más focalizada pero puede perder lemas útiles derivados hacia adelante si no se combina con saturación.

Límite

Se aplica a sistemas deductivos donde las reglas de inferencia y las propiedades de cierre están bien definidas; no garantiza terminación en lógica de primer orden en general a menos que se impongan restricciones o estrategias de equidad.

Tensión semántica

Existe tensión entre saturación hacia adelante y métodos dirigidos hacia atrás: la saturación es exhaustiva y puede producir lemas útiles en múltiples pruebas, mientras la búsqueda hacia atrás es dirigida y con frecuencia más eficiente para consultas específicas.

Síntesis

Un procedimiento de saturación es la aplicación disciplinada y exhaustiva de reglas de inferencia con estrategias de control de redundancias y ordenación para alcanzar un punto fijo de consecuencias derivables o detectar contradicción, formando la base de muchos sistemas de razonamiento automatizado.