(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:
- first-order logic
- propositional resolution (First-order resolution is an extension of propositional resolution.)
- first-order unification (Unification is part of the resolution procedure.)
- 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.
Location: Lecture sequence "Resolution"
- 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.
→ Knowledge Representation and Reasoning
An introductory textbook on knowledge representation.
Location: Chapter 4, "Resolution," pages 49-74
→ Artificial Intelligence: a Modern Approach
A textbook giving a broad overview of all of AI.
Location: Section 9.5, pages 295-309
-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