Procédure de Saturation

Un mécanisme d'inférence général qui applique de manière répétée des règles d'inférence à un ensemble de formules ou de clauses jusqu'à ce qu'aucune nouvelle conséquence ne puisse être dérivée (point fixe) ou qu'une contradiction soit produite, couramment utilisé en démonstration automatique.