Resolution

RESOLUTION
The resolution principle describes a way of finding contradictions in a knowledge base of clauses with minimum use of substitutions.
Resolution refutation proves a theorem (a goal) by negating the statement to be proved and adding this negated goal to the set of axioms that are known to be true.
The resolution rule of inference is used to show that it leads to a contradiction.
As it is shown that the negated goal is inconsistent with the given set of axioms, it follows that the original goal must be consistent.
Resolution refutation algorithm
1- Put the premises or axioms into clause form(conjunction of clauses).
2- Add the negation of the goal as another clause (what is to be proved) in clause form to the set of axioms. In other words, assume that the negation of the goal is true.
3- Resolve these clauses together, producing new clauses that logically follow from them.
4- Produce a contradiction by generating the empty clause.
5- The substitutions used to produce the empty clause are those under which the opposite of the negated goal is true.
6- Conclude that the negated goal is false because it causes contradiction.
7- Conclude that the goal is true.