The (general) Resolution Principle is a rule of inference for Relational Logic analogous to the Propositional Resolution Principle for Propositional Logic. Using the Resolution Principle alone (without axiom schemata or other rules of inference), it is possible to arrive at a proof method that proves the same consequences as the Fitch system given in Chapter 7. The search space using the Resolution Principle is smaller than the search space for generating Fitch proofs.
In our tour of Resolution, we look first at unification, which allows us to unify expressions by substituting terms for variables. We then move on to a definition of clausal form extended to handle variables. The Resolution Principle follows. ...