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:
- propositional logic
- propositional satisfiability (Resolution is a method for determining satisfiability of propositional sentences.)
- propositional proofs (Resolution is a complete proof procedure.)
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.
Other notes:
- Click on "Preview" to see the videos.
-Paid-
→ 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
See also
-No Additional Notes-