propositional resolution

(1.4 hours to learn)


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.


This concept has the prerequisites:


  • 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)


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.


See also

-No Additional Notes-