First-Order Resolution

In general
1. Find a literal L1 from clause C1, L2 from clause C2, and substitution θ such that L1 θ = ¬ L2 θ.
2. Form the resolvent C by including all literals from C1θ and C2θ, except for L1θ and ¬L2θ. More precisely, the set of literals occurring in the conclusion C is
  C = (C1 - {L1})θ ∪(C2 - {L2})θ
That is, θ is a unifying substitution for L1 and ¬ L2.
For example, let C1 = White(x) ← Swan(x) and C2 = Swan(Fred).
C1 can be re-written as White(x) ∨ ¬ Swan(x)
Then L1 = ¬ Swan(x), L2 = Swan(Fred) if θ ={x/Fred}
So C = White(Fred).