Resolution inference

In propositional logic, a resolution inference is an instance of the following rule:

[math]\displaystyle{ \frac{\Gamma_1 \cup\left\{ \ell\right\} \,\,\,\, \Gamma_2 \cup\left\{ \overline{\ell}\right\} }{\Gamma_1 \cup\Gamma_2}|\ell| }[/math]

We call:

• The clauses [math]\displaystyle{ \Gamma_1 \cup\left\{ \ell\right\} }[/math] and [math]\displaystyle{ \Gamma_2 \cup\left\{ \overline{\ell}\right\} }[/math] are the inference’s premises
• [math]\displaystyle{ \Gamma_1 \cup \Gamma_2 }[/math] (the resolvent of the premises) is its conclusion.
• The literal [math]\displaystyle{ \ell }[/math] is the left resolved literal,
• The literal [math]\displaystyle{ \overline{\ell} }[/math] is the right resolved literal,
• [math]\displaystyle{ |\ell| }[/math] is the resolved atom or pivot.

This rule can be generalized to first-order logic to:

[math]\displaystyle{ \frac{\Gamma_1 \cup\left\{ L_1\right\} \,\,\,\, \Gamma_2 \cup\left\{ L_2\right\} }{ (\Gamma_1 \cup \Gamma_2)\phi } \phi }[/math]

where [math]\displaystyle{ \phi }[/math] is a most general unifier of [math]\displaystyle{ L_1 }[/math] and [math]\displaystyle{ \overline{L_2} }[/math] and [math]\displaystyle{ \Gamma_1 }[/math] and [math]\displaystyle{ \Gamma_2 }[/math] have no common variables.

Example

The clauses [math]\displaystyle{ P(x),Q(x) }[/math] and [math]\displaystyle{ \neg P(b) }[/math] can apply this rule with [math]\displaystyle{ [b/x] }[/math] as unifier.

Here x is a variable and b is a constant.

[math]\displaystyle{ \frac{P(x),Q(x) \,\,\,\, \neg P(b)} {Q(b)}[b/x] }[/math]

Here we see that

• The clauses [math]\displaystyle{ P(x),Q(x) }[/math] and [math]\displaystyle{ \neg P(x) }[/math] are the inference’s premises
• [math]\displaystyle{ Q(b) }[/math] (the resolvent of the premises) is its conclusion.
• The literal [math]\displaystyle{ P(x) }[/math] is the left resolved literal,
• The literal [math]\displaystyle{ \neg P(b) }[/math] is the right resolved literal,
• [math]\displaystyle{ P }[/math] is the resolved atom or pivot.
• [math]\displaystyle{ [b/x] }[/math] is the most general unifier of the resolved literals.