propositional resolution

(1.4 hours to learn)

Summary

Resolution is an inference rule for logical systems -- in this case, for propositional logic. It is complete, in that if a set of propositional sentences is unsatisfiable, one can prove that using resolution. It is the basis for many powerful automated theorem provers.

Context

This concept has the prerequisites:

Goals

  • Be able to convert SAT instances to conjunctive normal form.
  • Know the resolution inference rule.
  • Show that resolution is sound.
  • Show that resolution is complete.

Core resources (read/watch one of the following)

-Free-

Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Author: Michael Genesereth
Other notes:
  • Click on "Preview" to see the videos.

-Paid-

See also

-No Additional Notes-