Conjunctieve normaalvorm

In de logica is een formule in conjunctieve normaalvorm (Eng. conjunctive normal form, CNF, ook wel afgekort als CNV) als die bestaat uit een conjunctie van disjuncties met literalen (ook een conjunctie van clausules genoemd). In een conjunctieve normaalvorm komen alleen de booleaanse operatoren 'en', 'of' en negatie voor, waarbij de negatie alleen als onderdeel van een literaal kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties.

Elke formule kan omgezet worden naar een equivalente formule in conjunctieve normaalvorm met behulp van equivalentieregels (zoals de wetten van De Morgan en distributiviteit) die de formule omschrijven naar een logisch equivalente vorm in CNF.