Another way of looking at resolution is to combine left-hand and right-hand sides of both Horn clauses and then cancel those statements that match on both sides.
Thus, for the simplest example,
combine the two clauses to give
b, c ← a, b.
and canceling the b,
b, c ← a, b.
gives
c ← a.
An Example
The simplest case is when the goal is already a known fact, such as
mammal( human ).
and one asks whether a human is a mammal:
← mammal( human ).
Using resolution, the system combines the two Horn clauses into
mammal( human ) ← mammal( human ).
and then cancels both sides to obtain
←
Thus, the system has found that indeed a human is a mammal and would respond to the query with “Yes.”