RESOLUTION IN PREDICATE LOGIC

Two literals are contradictory if one can be unified with the negation of the other. For example man(x) and man (Himalayas) are contradictory since man(x) and man(Himalayas ) can be unified. In predicate logic unification algorithm is used to locate pairs of literals that cancel out. It is important that if two instances of the same variable occur, then they must be given identical substitutions. The resolution algorithm for predicate logic as follows

Let f be a set of given statements and S is a statement to be proved.

1. Covert all the statements of F to clause form.

2. Negate S and convert the result to clause form. Add it to the set of clauses obtained in 1.

3. Repeat until either a contradiction is found or no progress can be made or a predetermined amount of effort has been expended.

a) Select two clauses. Call them parent clauses.

b) Resolve them together. The resolvent will be the disjunction of all of these literals of both clauses. If there is a pair of literals T1 and T2 such that one parent clause contains Ti and the other contains T2 and if T1 and T2 are unifiable, then neither t1 nor T2 should appear in the resolvent. Here Ti and T2 are called complimentary literals.

© If the resolvent is the empty clause , then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.

Using resolution to produce proof is illustrated in the following statements.

1. Marcus was a man.

2. Marcus was a Pompeian

3. All pompeians were Romans

4. Caesar was a ruler

5. All Romans were either loyal to Caesar or hated him.

6. Everyone is loyal to someone.

7. People only try to assassinate rulers they are not loyal to.

8. Marcus tried to assassinate Caesar.