Att en formel i ett språk L är på normalform betyder att den uppfyller vissa syntaktiska regler. Det finns ett flertal intressanta normalformer, varav följande kan nämnas.

Disjunktiv normalform redigera

En (satslogisk) formel är på disjunktiv normalform om den är en disjunktion av fall, där ett fall är en konjunktion av atomära satser. Följande formler är på disjunktiv normalform:

 
 
 

Varje logisk formel är ekvivalent med en formel på disjunktiv normalform.

Konjunktiv normalform redigera

En (satslogisk) formel är på konjunktiv normalform om den är en konjunktion av fall, där ett fall är en disjunktion av atomära satser. Följande formler är på konjunktiv normalform:

 
 
 

Varje logisk formel är ekvivalent med en formel på konjunktiv normalform.

Prenex normalform redigera

En formel i första ordningens logik är på prenex normalform om den består av en följd av kvantifikatorer följd av en kvantifikatorfri formel. Följande formler är på prenex normalform:

 
 

Varje första ordningens formel är ekvivalent med en formel på prenex normalform.

Skolems normalform redigera

En formel i första ordningens logik är på Skolems normalform om den är på konjunktiv prenex normalform med enbart allkvantifikatorer. Varje första ordningens formel kan Skolemiseras till en formel på Skolems normalform. Den resulterande formeln är inte nödvändigtvis ekvivalent med originalet, men den är satisfierbar om och endast om originalformeln är satisfierbar.

Skolems normalform är uppkallad efter Thoralf Skolem.