Procedimiento de Saturación

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.