First-order resolution

In mathematical logic and automated theorem proving, first-order resolution is a theorem-proving technique. It condenses the traditional syllogisms of logical inference down to a single rule.

To understand how resolution works, consider the following example syllogism of term logic:

```All Greeks are Europeans.
Homer is a Greek.
Therefore, Homer is a European.
```

Or, more generally:

```∀X, P(X) implies Q(X).
P(a).
Therefore, Q(a).
```

To recast the reasoning using the resolution technique, first the clauses must be converted to Conjunctive normal form. In this form, all quantification becomes implicit: universal quantifiers on variables (X, Y...) are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions.

```¬P(X) ∨ Q(X)
P(a)
Therefore, Q(a)
```

So the question is, how does the resolution technique derive the last clause from the first two? The rule is simple:

• Find two clauses containing the same predicate, where it is negated in one clause but not in the other.
• Perform a unification on the two predicates. (If the unification fails, you made a bad choice of predicates. Go back to the previous step and try again.)
• If any unbound variables which were bound in the unified predicates also occur in other predicates in the two clauses, replace them with their bound values (terms) there as well.
• Discard the unified predicates, and combine the remaining ones from the two clauses into a new clause, also joined by the "∨" operator.

To apply this rule to the above example, we find the predicate P occurs in negated form

```¬P(X)
```

in the first clause, and in non-negated form

```P(a)
```

in the second clause. X is an unbound variable, while a is a bound value (atom). Unifying the two produces the substitution

```X => a
```

Discarding the unified predicates, and applying this substitution to the remaining predicates (just Q(X), in this case), produces the conclusion:

```Q(a)
```

For another example, consider the syllogistic form

```All Cretans are islanders.
All islanders are liars.
Therefore all Cretans are liars.
```

Or more generally,

```∀X P(X) implies Q(X)
∀X Q(X) implies R(X)
Therefore, ∀X P(X) implies R(X)
```

In CNF, the antecedents become:

```¬P(X) ∨ Q(X)
¬Q(Y) ∨ R(Y)
```

(Note I renamed the variable in the second clause to make it clear that variables in different clauses are distinct.)

Now, unifying Q(X) in the first clause with ¬Q(Y) in the second clause means that X and Y become the same variable anyway. Substituting this into the remaining clauses and combining them gives the conclusion:

``` ¬P(X) ∨ R(X)
```

The resolution rule (with additional factoring) similarly subsumes all the other syllogistic forms of traditional logic.

• Art and Cultures
• Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
• Space and Astronomy