Bereinigte Normalform

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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.

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

Beispiel[Bearbeiten]

F:=\forall x\exists y\left(P\left(x,y\right) \wedge Q\left(x,z\right)\right)
G:=\exists u\left(\forall v P\left(u,v\right)\vee Q\left(v,v\right)\right)

In der Formel F sind die Variablen x und y gebunden und z 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 folgende Umbenennung (bei der Umbenennung müssen die gebundenen Variablen umbenannt werden):

G':=\exists u\left(\forall w P\left(u,w\right)\vee Q\left(v,v\right)\right)

Siehe auch[Bearbeiten]