Artificial Intelligence

16

Resolution in the Predicate Calculus

16.1 Unification

I abbreviate wffs of the form (∀ξ₁, ξ₂,…, ξ_n)(λ₁ ∨ λ2 ∨ … ∨ λ_k) by λ₁ ∨ λ₂ ∨ … ∨ λ_k, where λ₁, λ₂, …, λ_k are literals that might contain occurrences of the variables ξ₁, ξ₂, …, ξ_n. That is, I simply drop the universal quantifiers and assume universal quantification of any variables in the λ_i. (Later, I will show how any existentially quantified variables can be eliminated first.) Wffs in this abbreviated form are called clauses. Sometimes I write a clause using set notation {λ₁, λ₂, …, λ_k} and assume disjunction among the elements of the set.

If two clauses have matching but complementary literals, we can resolve them—just as in the propositional calculus. If we have a literal, λ(ξ), in one ...