# 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-