Negationsnormalform (Prädikatenlogik)

Analog zur Aussagenlogik ist eine FO-Formel in Negationsnormalform (NNF), wenn:

1. Sie die Verknüpfungen $\to ,\leftrightarrow$ nicht enthält.
2. Das Negationszeichen $\mathrm{\neg }$ nur direkt vor atomaren Formeln steht.
   Dies wird durch Anwendung der De-Morgan-Regeln und der Quantoren-Dualität ($\mathrm{\neg }\mathrm{\forall }x\phi \equiv \mathrm{\exists }x\mathrm{\neg }\phi$) erreicht.