Negationsnormalform: alle Negationen nur bei atomen (keine Implikationen: statt !p(x) schreibe p(!x), keine Negationen vor Klammern: statt !(x UND y) schreibe (!x ODER !y), !x ist ok)

Bereinigte Negationsnormalform: Negationsnormalform + kein Schnitt zwischen Freien und gebundenen Variablen (Umbenenung)

Praenexe Normalform: alle Quntoren stehen ganz links in der Formel, keine weiter

Skolemnormalform:

1. All-Abschluss ueber allen freien Variablen

2. Skolemisirung: fuer alle Existenz-Quantoren und quantifizieren Variablen fuege ein k-Stelliges Funktionsymbol mit allen All-Quantifizierten Variablen, die Links vom Existenz-Quantor stehen. Dann ersetze alle Stellen mit dieser Variante mit Funktion, abhaengig von allen All-Quantifizierten Veriablen

3. Formel (jetzt ohne Existenz-Quantoren) muss in KNF stehen