semiopedia.org
Resolution Principle

Resolution Principle

A complete and sound method of automated theorem proving in first-order logic that uses contradiction and clause resolution to derive proofs.

The Resolution Principle, introduced by Alan Robinson in 1965, is a fundamental method in automated reasoning that revolutionized the field of theorem proving. At its core, the principle provides a single inference rule that can replace all other rules of logical deduction in first-order logic.

The principle operates on clauses (disjunctions of literals) and works through a process of contradiction. To prove a theorem, its negation is added to the set of known axioms, and the resolution principle is applied repeatedly until either a contradiction is found (proving the original theorem) or no new clauses can be derived.

Key aspects of the Resolution Principle include:

  1. Clause Form
  • All formulas must be converted to Conjunctive Normal Form
  • Statements are represented as sets of clauses
  • Each clause is a disjunction of literals (atomic formulas or their negations)

  1. The Resolution Rule The core operation combines two clauses containing complementary literals (P and ¬P) to produce a new clause containing all remaining literals from both parent clauses. This process is called resolving the clauses.

  2. Unification The principle employs unification, a pattern-matching procedure that determines how variables in different clauses can be instantiated to make literals complementary. This is crucial for handling variables in first-order logic.

Historical Significance: The Resolution Principle marked a significant breakthrough in automated deduction and laid the groundwork for:

Connections to Systems Theory: The Resolution Principle exemplifies several important systemic concepts:

Limitations and Extensions: While complete for first-order logic, the basic resolution principle has limitations:

  • Can be computationally expensive
  • May generate many irrelevant clauses
  • Requires careful strategy selection

Various refinements and strategies have been developed to improve efficiency:

The Resolution Principle continues to influence modern developments in:

Its elegance lies in reducing complex logical reasoning to a single, mechanically applicable rule, making it a cornerstone of computational logic and automated reasoning systems.