Resolution Theorem Proving (Robinson, 1965) is one proof theoretic method for proving theorems in First Order Logic (FOL).

   One of the steps in this procedure is to limit the syntax of FOL. All FOL expressions are converted to what is referred to as conjunctive normal form.

   To the right is a database for use in this example of resolution theorem proving. The statements are shown in English (top), in conjunctive normal form (middle and indented), and in the syntax of First Order Logic (bottom and most indented). (Note that for a ground expression, such as the first two expressions, the conjunctive normal form and the standard form are identical.)

Unification

   In FOL we allow expressions to have a structure (as compared to propositional logic); i.e., we have predicates which take arguments...e.g.,variables, functions, or constants. Now to determine if a logical proof can be constructed we have to pay attention to how we handle the differing variables, functions, or constants that might appear in a set of axioms used in a proof. Unification is a procedure for searching for a consistent set of substitutions of elements. The basic idea is :

To unify two literals, e.g. hate(x,y) hate(Marcus,z), first determine if the first element (the predicate which syntactically is a constant) match. If so continue with the following basic matching rules:

Different constant, functions, or predicates cannot match; identical ones can.

A variable can match another variable, any constant, or a function or predicate expression, with the restriction that the function or predicate expression must not contain any instances of the variable being matched.

This is simple enough...the complication arises because there is a more global requirement on the matching process...i.e. a single consistent substitution for the entire literal is required, not separate ones for each piece. This procedure involves searching through the space of substitutions allowed by the matching rules above (the "generators" if you will). An additional complication arises when there are several possible unifications. In order to avoid substitutions that are unnecessary, the unification procedure is designed to determine the most general unifier (mgu) at each stage in the process.

   The figure to the left shows the successful part of the search for a proof of the assertion that Marcus hates Caesar. The database is reiterated in yellow at the top of the figure. Then you will notice the statement that Marcus does not hate Caesar. Resolution theorem proving works by negating the assertion that is to be proved, and trying to prove a contradiction...or the empty set.

   The numbers refer to the item in the database which is "resolved" with the expression. This procedure involves two syntactic rules. One is substitution which is carried out by the process called unification discussed above. For example, the expression Marcus/x2 at the top of the search represents the substitution of Marcus for the variable x2. The other rule is modus ponens although that may not be so obvious. You need to remember that 'not p or q' is identical to 'p -> q'. Then clearly if you have 'p', 'not p or q' you can write down 'q'. That is what is going on in the example shown to the left. Consider the very first step. Notice that one of the disjuncts in line 5 of the database is hate(x2,Caesar). Substituting Marcus for x2 yields an expression which contradicts the expression on the left. Consequently, both expressions can be eliminated since the truth of 5 cannot depend on this disjunct if the database is consistent.

   Now, if all of the expressions can be eliminated in this manner, then all that remains is then empty set (shown as a white box in the figure on the left). This indicates that the database is inconsistent, that is it contains a contradiction.