Resolution

Description:

Resolution provides an important operator for proving clauses.

Let
  • C1 := {A1, A2, ..., Am}
  • C2 := {¬A1, B1, ..., Bn}
be clauses, represented by sets of literals.

Then

D := { A2, ..., Am, B1, ..., Bn }.
can be derived from C1 and C2.

Incorporating Substitution

Combining the rule above with substitution leads to an even more powerful resolution rule. This is illustrated by figure 1.


Figure 1: The Resolution-"V".

Let C1 and C2 be clauses,

  • θ1 and θ2 be substitutions, and
  • let L be a literal with
    • L ∈ C1θ1 and
    • ¬L ∈ C2θ2.
Then
D := ( C1θ1 \ L ) ∪ ( C2θ2 \ ¬L )
can be derived from C1 and C2.