In order to prove a goal with respect to a set of program clauses, resolution seeks to show that leads to a contradiction.
A contradiction is obtained when a literal and its negation are stated at the same time. If a contradiction does not arise, a new goal is derived by unifying the current goal with a program clause, the derived goals are called resolvents.