Resolution is a method to prove logical statements. Actually it doesn't prove a statement, but it proves the unrealizability of it. But that's not a problem. If you want to prove something you just negate it, and prove the unrealizability of this formula.
Resolution works for propositional logic, predicate Logic and logical programs in the form of Horn clauses (that's why Prolog uses it).
propositional logic
To simplify the resolution algorithm, the formula should be in clause form (which is like the disjunctive normal form, but the disjunctions are lists and the whole formula is a list of lists). The algorithm works the following way:
- Choose a clause C1, which contains an atom p
- Choose a clause C2, which contains an atom not(p)
- Generate a new clause C by deleting all p from C1 and all not(p) from C2 and combining both disjunctively
- Do this until you can't generate any new clauses or till you generated an empty clause
If you generated an empty clause, the formula is unrealizable. If you negated the formula before you used the algorithm, you proved the formula. If you finished the algorithm without generating an empty clause, you either proved that it is not unrealizable or that it is wrong (if you negated it in the beginning).
Example:
Your formula is:
[ [a], [b], [c], [not a, not b, e], [not c, not e] ]
The disjunctions are numbered from 1 to 5:
res(1,4) = [not b, e] 6
res(2,6) = [e] 7
res(3,5) = [not e] 8
res(6,8) = [] 9
You just proved that the formula is unrealizable.
predicate logic
The algorithm works very similar. Again you have to have a formula in clause form (which is a bit more difficult here, as you have to convert the formula in prenex normal form, then into skolem normal form and finally into the disjunctive normal form). The algorithm again has the same rule for generating new clauses, but with the extension of the use of unification for the finding of equal atoms:
Choose a clause C1, which contains an atom p(a1,...,an)
Choose a clause C2, which contains an atom not(p(b1,...,bn)
p(a1,...,an) and (p(b1,...,bn) can be unified with an unificator U
Generate a new clause (C)U by deleting all p from C1 and all not(p) from C2 and combining both disjunctively
Do this until you can't generate any new clauses or till you generated an empty clause
But using only this rule is not enough for predicate logic, so there is another one:
you have a clause C which contains p(a1,...,an) and p(b1,...,bn)
or not(p(a1,...,an)) and not(p(b1,...,bn))
p(a1,...,an) and p(b1,...,bn) can be unified with an unificator U
generate a new clause D1 without p(a1,...,an) and p(b1,...,bn)
Horn clauses
A logical program which contains only Horn clauses is a definite program. It can be proven by using SLD-resolution (linear resolution with selection function on definite clauses). The algorithm:
you have:
<- B1 and ... and Bm
which is called a definite goal (your question to the program) and
A <- A1 and ... and An
which is a clause from your program. If a Bi and A can be unified with a unificator U, you can write:
<- (B1 and ... and Bi-1 and A1 and ... and An and ... Bm)U
Repeat this until you either get the empty clause(you've proven B1 and ... and Bm) or you can't do more resolutions (you've proven that B1 and ... and Bm is wrong).
The problem with the resolution of definite programs is, that it does not neccessarily stop.