We now extend inference by resolution beyond the propositional case (covered, recall, in Chapter 2) to the case of first-order formulas. This means that the formulas involved in inferences are now allowed to contain quantifiers, variables, relation symbols, functors, and constants. In order for resolution to be applied to first-order formulas these formulas must first be converted to clausal form, and it is to this conversion that we now turn.