Resolution Rule

Learning Sets of Rules

The resolution rule is a sound and complete rule for deductive inference in first-order logic.
The rule is:
P ∨ L
¬L ∨ R
--------
P ∨ R
More generally
1. Given initial clauses C1 and C2, find a literal L from C1 such that ¬L is in C2.
2. Form the resolvent C by including all literals from C1 and C2 except for L and ¬L:
  C = (C1 - {L}) ∪ (C2 - {¬L})