In der Prädikatenlogik heißt eine Formel bereinigt, wenn

1. keine Variable sowohl frei als auch gebunden vorkommt,
2. hinter jedem Quantor eine andere Variable steht.

Hinweis: Zu jeder Formel gibt es eine bereinigte äquivalente Formel. Jede Formel F lässt sich durch geeignete, gebundene Umbenennung in eine bereinigte Form überführen.

Beispiel:

In der Formel F sind die Variablen x und y gebunden und a ist frei. F ist somit bereinigt. In der Formel G sind alle Vorkommen der Variable u gebunden, allerdings tritt v sowohl gebunden als auch frei auf. G ist daher nicht in bereinigter Form. Eine Überführung für G ist folgene Umbenennung:

Siehe auch: Normalform Abschnitt Prädikatenlogik