(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:
- propositional logic
- propositional satisfiability (Resolution is a method for determining satisfiability of propositional sentences.)
- propositional proofs (Resolution is a complete proof procedure.)
- 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.
- Click on "Preview" to see the videos.
→ Artificial Intelligence: a Modern Approach
A textbook giving a broad overview of all of AI.
Location: Section 7.5, "Reasoning patterns in propositional logic," up through subsection "Completeness of resolution," pages 211-217
→ Knowledge Representation and Reasoning
An introductory textbook on knowledge representation.
Location: Chapter 4, "Resolution," up through Section 4.1, "The propositional case," pages 49-55
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation