Resolution (Predicate Logic)

Propositional resolution can be generalised to be applicable to predicate logic as well, though there are a few extra steps involved. Refutations and resolution proofs are the same as they were in propositional logic, however, our standard resolution rule has a few modifications.

Resolution Rule §

In predicate logic, the resolution rule depends on unification of two formula.

Let $P$ and $Q$ be unifiable atomic predicates having a unifier $\theta$. Then, for any two disjunctive clauses, $C_1$ and $C_2$ we have the resolution rule:

$$\begin{array}{rl}& C_1\vee P\\ & C_2\vee \neg Q\\ & (C_1\vee C_2)[\theta ]\end{array}$$

It helps to rename any same variables in $P$ and $Q$ to different ones.

For example, take:

$$\{R(x,y),Q(y)\}\{S(z),\neg Q(a)\}$$

We know that $Q(y)$ and $Q(a)$ are unifiable with $\theta =\{y\mapsto a\}$

So we use the resolution rule:

$$\begin{array}{rl}& R(x,y)\vee Q(y)\\ & S(z)\vee \neg Q(a)\\ & (R(x,y)\vee S(z))[\theta ]\end{array}$$

resulting in a final clause (remember to apply the renaming!)

$$\{R(x,a),S(z)\}$$

Resolution Requires Resolution Rule and Factoring §

Sometimes a resolution rule is not sufficient to obtain a refutation, and requires factoring as well.

For example, take the two clauses:

$$\{P(x),Q(y)\}\{\neg P(a),\neg Q(b)\}$$

we can easily apply a resolution rule to eliminate $P$ or $Q$, but not both! Because the rule specifies elimination of atomic predicates, we can only eliminate one predicate at a time.

So we could do, for example $\theta =\{x\mapsto a\}$ and use the resolution rule to obtain:

$$\{Q(y),\neg Q(b)\}$$

Now what? We only have a single clause. We need to factor the clause by using $\theta =\{y\mapsto b\}$:

$$\{Q(y),\neg Q(b)\}\approx \{\}=\perp$$

Formal Definition §

Explanation §

The extra steps for resolution come from substituting variables to terms, in order to ensure two different formulae are talking about the same objects.

For example, take the formulae:

$$[P(x)\to B(x)]\wedge [\neg B(p)]$$

• $P$ means is a parrot
• $B$ means is beautiful
• $p$ is a constant called Polly.
• Remember that $x$ is conventionally a universally quantifiable variable, (so we take $\forall x$)

Then if we ‘fix’ $x\mapsto p$, (and this is possible because implicitly, we have something that applies for all values of $x$) we have:

$$[P(p)\to B(p)]\wedge [\neg B(p)]$$

Now, our predicates are essentially propositions,(because they are being done over a constant). What we have actually done is unification.

We can then use our resolution rule to evaluate it

$$[P(p)\to B(p)],[\neg B(p)]⊢\neg P(p)$$

This action of remapping is the keystone of resolution in predicate logic.

The main steps of resolution in predicate logic are: