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 - Principle

  • Resolution commonly requires sentences to be in clause normal form (also called conjunctive normal form or CNF)
    • A clause is a disjunction of literals (implicitly universally quantified)
      • E.g. : l1 ∨ … ∨ ln
    • A formula in clause normal form conjunction of a set of clauses
      • E.g.: C1 ∧ … ∧ Cn = (ln ∨ … ∨ lm) ∧ … ∧ (li ∨ … ∨ lj)
  • High level steps in a resolution proof:
    • Put the premises or axioms into clause normal form (CNF)
    • Add the negation of the to be proven statement, in clause form, to the set of axioms
    • Resolve these clauses together, using the resolution rule , producing new clauses that logically follow from them
    • Derive a contradiction by generating the empty clause.
    • The substitutions used to produce the empty clause are those under which the opposite of the negated goal is true

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.