Given a conjunction of two disjunctions of literals (clauses), replace the original with a single disjunction (clause) after eliminating one pair consisting of a literal in one clause and its negation in the other clause. The new clause is the resolvent of the two clauses.
(p V q) ((~ p) V r) ----------- (q V r)
The two literals which are eliminated need not be identical if they contain variables. They need only unify with one another: constants must match exactly, variables must match under certain conditions (see the page on unification), the result of which is a set of variable bindings which is then propagated through the remaining literals in the resolvent.
Last updated: 5 February 1996
URL: http://www.indiana.edu/~gasser/Q351/resolution.html
Comments:
gasser@salsa.indiana.edu
Copyright 1996,
The Trustees of
Indiana University