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 (cont’)

  • Theorem : If the set of a clauses labeling the leaves of a resolution tree is satisfiable, then the clause at the root is satisfiable

  • Theorem ( Soundness ): If the empty clause is derived from a set of clauses, then the set of clauses is unsatisfiable

  • Theorem ( Completeness ) If a set of clauses is unsatisfiable, then the empty clause can be derived from it using resolution algorithm


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.