A Machine-Oriented Logic Based on the Resolution Principle

Inside the paper

The problem

Automated theorem proving for first-order logic faces a large search through possible substitutions and consequences. Earlier procedures could spend substantial effort generating instances that do not contribute to a proof.

The idea

Robinson develops a resolution procedure that combines clauses after finding a suitable unifying substitution. The paper proves that refutation by this rule is complete and discusses ways to organize the search.

How it works

• Express the negated conjecture and premises as clauses, so proving the conjecture becomes a search for a contradiction.
• Find literals in clauses that can be made complementary by substituting terms for variables.
• Use a most general unifier to combine the remaining literals into a resolvent without prematurely choosing more specific substitutions.
• Repeat resolution until the empty clause is obtained, using search restrictions such as subsumption to avoid some redundant clauses.

What it showed

The paper establishes the unification theorem and the resolution theorem supporting the refutation procedure. It also analyzes search principles and redundancy, distinguishing the logical completeness result from the practical problem of finding a proof efficiently.

Read it for

Start with the ground case in Sections 2 and 4, then read the unification algorithm and resolvents in Section 5. Section 6 connects these to refutation; Section 7 is useful for search strategy, while the formal preliminaries can be consulted as needed.

Written in our own words from the paper itself. A draft the editors have not yet reviewed.