TOPICS
Search

Resolution Principle


The resolution principle, due to Robinson (1965), is a method of theorem proving that proceeds by constructing refutation proofs, i.e., proofs by contradiction. This method has been exploited in many automatic theorem provers. The resolution principle applies to first-order logic formulas in Skolemized form. These formulas are basically sets of clauses each of which is a disjunction of literals. Unification is a key technique in proofs by resolution.

If two or more positive literals (or two or more negative literals) in clause S are unifiable and eta is their most general unifier, then Seta is called a factor of S. For example, P(x) v ¬Q(f(x),b) v P(g(y)) is factored to P(g(y)) v ¬Q(f(g(y)),b). In such a factorization, duplicates are removed.

Let S_1 and S_2 be two clauses with no variables in common, let S_1 contain a positive literal L_1, S_2 contain a negative literal L_2, and let eta be the most general unifier of L_1 and L_2. Then

 (S_1eta-L_1eta) union (S_2eta-L_2eta)

is called a binary resolvent of S_1 and S_2. For example, if S_1=P(x) v Q(x) and S_2=¬P(a) v R(y), then Q(a) v R(y) is their binary resolvent.

A resolvent of two clauses S_1 and S_2 is one of the four following binary resolvents.

1. A binary resolvent of S_1 and S_2.

2. A binary resolvent of S_1 and a factor of S_2.

3. A binary resolvent of a factor of S_1 and S_2.

4. A binary resolvent of a factor of S_1 and a factor of S_2.

Generation of a resolvent from two clauses, called resolution, is the sole rule of inference of the resolution principle. The resolution principle is complete, so a set (conjunction) of clauses is unsatisfiable iff the empty clause can be derived from it by resolution.

Proof of the completeness of the resolution principle is based on Herbrand's theorem. Since unsatisfiability is dual to validity, the resolution principle is exercised on theorem negations.

Multiple strategies have been developed to make the resolution principle more efficient. These strategies help select clause pairs for application of the resolution rule. For instance, linear resolution is the following deduction strategy. Let S be the initial set of clauses. If C_0 in S, a linear deduction of C_n from S with top clause C_0 is a deduction in which each C_(i+1) is a resolvent of C_i and B_i (0<=i<=n-1), and each B_i is either in S or a resolvent C_j (with j<i).

Linear resolution is complete, so if C is a clause in an unsatisfiable set S of clauses and S-C is satisfiable, then the empty clause can be obtained by linear resolution with C as the top clause.

If the additional restriction that B_i be in S imposed, then this restricted strategy is incomplete. However, it is complete for sets of Horn clauses containing exactly one goal, and the goal is selected as the top clause. All other clauses in such sets are definite Horn clauses. Implementations of programming language Prolog conduct search within the framework of this strategy.


See also

Horn Clause, Resolution

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Clocksin W. F. and Mellish, C. S. Programming in Prolog. New York: Springer-Verlag, 1984.Robinson J. A. "A Machine-Oriented Logic Based on the Resolution Principle." J. Assoc. Comput. Mach. 12, 23-41, 1965.

Referenced on Wolfram|Alpha

Resolution Principle

Cite this as:

Sakharov, Alex. "Resolution Principle." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/ResolutionPrinciple.html

Subject classifications