Project SherlockEst. Knowledge

Paper

1965

A Machine-Oriented Logic Based on the Resolution Principle

J. A. Robinson

Introduces resolution and unification as a single inference rule complete for first-order logic, replacing the many special-case rules earlier automated theorem provers needed.

Before you start

FreeAdvancedlink checked 17 Sept 2026

Groundwork for

Works in the library that name this one as a prerequisite.

STRIPS: A New Approach to the Application of Theorem Proving to Problem SolvingRichard E. Fikes & Nils J. Nilsson, 1971Represents planning states and operators so that theorem proving can generate plans directly, introducing the add/delete-list action representation that automated planners still use as a baseline.

Filed under Classical & Symbolic AI in Artificial Intelligence.