# CNF

A propositional formula is a CNF formula^{}, meaning Conjunctive Normal Form^{}, if it is a conjunction^{} of disjunction^{} of literals^{} (a literal is a propositional variable or its negation^{}). Hence, a CNF is a formula of the form: ${K}_{1}\wedge {K}_{2}\wedge \mathrm{\dots}\wedge {K}_{n}$, where each ${K}_{i}$ is of the form ${l}_{i1}\vee {l}_{i2}\vee \mathrm{\dots}\vee {l}_{im}$ for literals ${l}_{ij}$ and some $m$ (which can vary for each ${K}_{i}$).

Example: $(x\vee y\vee \mathrm{\neg}z)\wedge (y\vee \mathrm{\neg}w\vee \mathrm{\neg}u)\wedge (x\vee v)$.

Title | CNF |
---|---|

Canonical name | CNF |

Date of creation | 2013-03-22 14:02:35 |

Last modified on | 2013-03-22 14:02:35 |

Owner | rspuzio (6075) |

Last modified by | rspuzio (6075) |

Numerical id | 7 |

Author | rspuzio (6075) |

Entry type | Definition |

Classification | msc 03B05 |

Synonym | conjunctive normal form |

Related topic | DNF |

Related topic | AtomicFormula |