Introduction to Logic

Tools
for
Thought

Lesson 14.4

Resolution Principle

The Relational Resolution Principle is analogous to that of propositional resolution. The main difference is the use of unification to unify literals before applying the rule. Although the rule is simple, there are a couple complexities, so we start with a simple version and then refine it to deal with these complexities.

A simple version of the Resolution Principle for Relational Logic is shown below. Given a clause with a literal φ and a second clause with a literal ¬ψ such that φ and ψ have a most general unifier σ, we can derive a conclusion by applying σ to the clause consisting of the remaining literals from the two original clauses.

{φ₁, ... , φ, ... , φ_m}
{ψ₁, ... , ¬ψ, ... , ψ_n}

{φ₁, ... , φ_m, ψ₁, ..., ψ_n}σ
where σ=mgu(φ, ψ)

Consider the example shown below. The first clause contains the positive literal p(a,y) and the second clause contains a negative occurrence of p(x, f(x)). The substitution {x←a, y←f(a)} is a most general unifier of these two expressions. Consequently, we can collect the remaining literals r (y) and q(g(x)) into a clause and apply the substitution to produce a conclusion.

{p(a, y), r(y)}
{¬p(x, f(x)), q(g(x))}

{r(f(a)), q(g(a))}

Unfortunately, this simple version of the Resolution Principle is not quite good enough. Consider the two clauses shown below. Given the meaning of these two clauses, it should be possible to resolve them to produce the empty clause. However, the two atomic sentences do not unify. The variable x must be bound to a and b at the same time.

{p(a, x)}

{¬p(x, b)}

Fortunately, this problem can easily be fixed by extending the Resolution Principle slightly as shown below. Before trying to resolve two clauses, we select one of the clauses and rename any variables the clause has in common with the other clause.

{φ₁, ... , φ, ... , φ_m}
{ψ₁, ... , ¬ψ, ... , ψ_n}

{φ₁τ, ... , φ_mτ, ψ₁, ... , ψ_n}σ
where τ is a variable renaming on {φ₁, ... , φ, ... , φ_m}
where σ=mgu(φτ, ψ)

Renaming solves this problem. Unfortunately, we are still not quite done. There is one more technicality that must be addressed to finish the story. As stated, even with the extension mentioned above, the rule is not quite good enough. Given the clauses shown below, we should be able to infer the empty clause {}; however, this is not possible with the preceding definition. The clauses can be resolved in various ways, but the result is never the empty clause.

{p(x), p(y)}

{¬p(u), ¬p(v)}

The good news is that we can solve this additional problem with one last modification to our definition of the Resolution Principle. If a subset of the literals in a clause Φ has a most general unifier γ, then the clause Φ' obtained by applying γ to Φ is called a factor of Φ. For example, the literals p(x) and p(f(y)) have a most general unifier {x←f(y)}, so the clause {p(f(y)), r(f(y), y)} is a factor of {p(x), p(f(y)),r(x, y)}. Obviously, any clause is a trivial factor of itself.

Using the notion of factors, we can give a complete definition for the Resolution Principle. Suppose that Φ and Ψ are two clauses. If there is a literal φ in some factor of Φ and a literal ¬ψ in some factor of Ψ, then we say that the two clauses Φ and Ψ resolve and that the new clause ((Φ'-{φ})∪(Ψ'-{¬ψ}))σ is a resolvent of the two clauses.

Φ
Ψ

((Φ'-{φ})∪(Ψ'-{¬ψ}))σ
where τ is a variable renaming on Φ
where Φ' is a factor of Φτ and φ∈Φ'
where Ψ' is a factor of Ψ and ¬ψ∈Ψ'
where σ=mgu(φ, ψ)

Using this enhanced definition of resolution, we can solve the problem mentioned above. Once again, consider the premises {p(x), p(y)} and {¬p(u), ¬p(v)}. The first premise has the factor {p(x)}, and the second has the factor {¬p(u)}, and these two factors resolve to the empty clause in a single step.

Use the arrow keys to navigate.

Press the escape key to toggle all / one.