# first-order resolution

(4.4 hours to learn)

## Summary

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

## Context

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.)

## Goals

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

## -Free-

→ Coursera: Introduction to Logic (2014)

An introductory logic course geared towards computer scientists.

Location:
Lecture sequence "Resolution"

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.

## -Paid-

→ 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

## See also

-No Additional Notes-