first-order resolution

(4.4 hours to learn)


Resolution is an inference rule for first-order logic which is a key part of many automated theorem provers.


This concept has the prerequisites:


  • Be able to eliminate existential quantifiers using Skolemization.
  • Be able to reduce a set of first-order sentences to conjunctive normal form.
  • State the resolution rule and be able to apply it to simple examples.
  • Know how resolution can be used to give constructive proofs, where one desires a set of substitutions to variables which make the consequent true.

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:
  • This actually covers relational logic, but at the level of this concept node, most of the ideas are the same. See the bonus lecture "First order logic (a very brief introduction)" for an explanation of the differences.
  • Click on "Preview" to see the videos.


See also

-No Additional Notes-