Inverting Resolution

The inverse entailment operator must derive C2 given the resolvent C and C1.
Say C = A ∨ B, and C1= B ∨ D. How do we derive C2 s.t. C1 ∧ C2 → C?
Find the L that appears in C1 and not in C, then form C2 by including the following literals
C2 = (C - (C1 - {L})) ∪ {¬ L}
so
C2 = A ∨ ¬D
C2 can also be A ∨ ¬D ∨ B.
In general, inverse resolution can produce multiple clauses C2.