Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Resolution - Converting to Clause Normal Form

  • Step 6: Drop all universal quantifiers
  • Step 7: Convert the expression to the conjunctions of disjuncts
      (a ∧ b) ∨ (c ∧ d)
      = (a ∨ (c ∧ d)) ∧ (b ∨ (c ∧ d))
      = (a ∨ c) ∧ (a ∨ d) ∧ (b ∨ c) ∧ (b ∨ d)
  • step 8: Split each conjunction into a separate clauses, which are just a disjunction of negated and nonnegated predicates, called literals
  • step 9: Rename so that no variable symbol appears in more than one clause.
        (∀X)(a(X) ∧ b(X)) = (∀X)a(X) ∧ (∀ Y)b(Y)

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.