Resolution and Unification

Our results from Chapter 6 suggest that an arbitrary formula ϕ can be proved—and hence ¬ϕ can be refuted—by first converting ¬ϕ to a satisfiability-equivalent formula ψ in prenex normal form, and then refuting a set of instantiated clauses—derived from the clausal form of the matrix of F(ψ)—which is ground satisfiable over the extended Herbrand universe of ϕ iff ¬ϕ satisfiable. The existence of such a set of instantiated clauses is guaranteed by Herbrand’s Theorem, whose proof, unfortunately, provides no insight into how to actually find one. A rather straightforward method for generating a set of clauses with the required property is simply to enumerate, in turn, all ground instances of the clauses in the matrix of F(ψ) until such a set is found; in practice, however, this kind of uncontrolled enumeration emerges as considerably less than efficient. In the next section we will learn of unification, a technique for eliminating brute-force enumeration of ground clauses from our refutation method for arbitrary formulae by enabling the systematic recognition of ground instances of nonground clauses which are relevant to refutations. The remainder of this section is dedicated to describing a refutation method for ground clauses that can be used in conjunction with precisely such a brute-force enumeration; in Section 7.4 we see how to combine unification with a generalization of this method for ground clauses to arrive at an efficient refutation technique for arbitrary clauses.