／var／logmarcus chiu

Propositional Logic - (Negation - Conjunctive - Disjunctive) Normal Forms (NNF - CNF - DNF)

Created on

  • literal - is an atomic formula or its negation
  • maxterm - is a literal or a disjunction of literals
  • minterm - is a literal or a conjunction of literals

Types of Normal Forms

Types

Description

Negation Normal Form (NNF)

a formula where:

  • the only logical connectives allowed are and, or, and not
  • not is only applied to atomic formulae

Conjunctive Normal Form (CNF)

a formulae that is a conjunction of maxterms/disjunctions

Disjunctive Normal Form (DNF)

a formulae that is a disjunction of minterms/conjunctions

Translation to Normal Form

  • Translation to NNF
    • remove ↔  and →
      • A ↔ B ≃ (A → B) and (B → A)
      • A → B ≃ ¬A or B
    • push negations in until they apply only to atomic literals
      • ¬¬A ≃ A
      • ¬(A and B) ≃ ¬A or ¬B
      • ¬(A or B) ≃ ¬A and ¬B
    • at this point the formula is in Negation Normal Form
  • Translation to CNF from NNF
    • push disjunctions (or) in until they apply only to literals
      • A or (B and C) ≃ (A or B) and (A or C)
    • delete any maxterm that contains both P and ¬P since it is equivalent to true
    • delete any maxterm that includes another maxterm
      • A and (A or B) ≃ A
    • take 2 maxterms of the form below
      • (P or A) and (¬P or A) ≃ A
  • Translation to DNF from NNF
    • push conjunctions (and) in until they apply only to literals
      • A and (B or C) ≃ (A and B) or (A and C)
    • exactly the same simplifications can be performed for DNF as for CNF, exchanging the roles of ∧ and v