Conjunctieve normaalvorm
Van Wikipedia
In de logica is een propositie in conjunctieve normaalvorm (Eng. Conjunctive Normal Form, CNF) als die bestaat uit een conjunctie van disjuncties (ook een conjunctie van clauses genoemd). In een conjunctieve normaalvorm komen alleen de Booleaanse operatoren en, of en negatie voor waarbij de negatie alleen als onderdeel van een atomaire formule kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties.
Elke propositie kan omgezet worden naar een equivalente propositie in conjunctieve normaalvorm met behulp van regels (zoals de wetten van De Morgan en distributiviteit) die de propositie omschrijven naar een logisch equivalente vorm in CNF.
CNF is onder andere belangrijk in het automatisch redeneren, het deelgebied van informatica waarin computers logische redeneerprocessen uitvoeren. Verschillende klassieke algoritmes in dat vakgebied schrijven formules om naar CNF voor ze ermee gaan rekenen.
[bewerk] Voorbeelden
Voorbeelden van proposities in conjunctieve normaalvorm:
[bewerk] Conversie naar conjunctieve normaalvorm
Elke formule van de klassieke propositielogica kan omgezet worden naar CNF door herhaling van de volgende stappen.
- Elimineer
(bi-implicatie) met behulp van:
- Elimineer
(implicatie) met behulp van:
- Verplaats
(negatie) naar binnen met behulp van:
(elimineren van dubbele negatie)
(wetten van De Morgan)
(wetten van De Morgan)
- Distribueer
over 
:
Voor de klassieke predikatenlogica bestaat een soortgelijke procedure. In de modale logica is conversie naar CNF niet in alle gevallen mogelijk.
