Sättigungsverfahren

Ein allgemeiner Inferenzmechanismus, der Inferenzregeln wiederholt auf eine Menge von Formeln oder Klauseln anwendet, bis keine neuen Konsequenzen mehr ableitbar sind (Fixpunkt) oder eine Widerspruchsklausel erzeugt wird; gebräuchlich in Theorembeweisern und automatischem Schließen.