Skolem Normalform

Einfache Sprache

Def. Skolem Normalform

Die Menge der prädikatenlogische Formeln in Skolem Normalform ($\mathbf{SNF}$) sind alle Formeln in PNF die auch Universelle Formeln sind, als deren Quantorenblock nur Allquantoren enthält.

Durch die Skolemisierung können wir aus einer Formel in PNF eine Formel in $\mathbf{SNF}$ machen, die nach dem Satz Skolemisierung ist Korrekt erfüllbarkeitsäquivalent ist.