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 - The Resolution Rule

  • The resolution rule is a single inference that produces a new clause implied by two clauses (called the parent clauses) containing complementary literals

    • Two literals are said to be complements if one is the negation of the other (in the following, ai is taken to be the complement to bj).
    • The resulting clause contains all the literals that do not have complements. Formally:

    • Where a1, …, an, b1, …, bm are literals, and ai is the complement to bj
  • The clause produced by the resolution rule is called the resolvent of the two input clauses.
    • A literal and its negation produce a resolvent only if they unify under some substitution σ.
    • σ Is then applied to the resolvent

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.