# Catalogue of Artificial Intelligence Techniques

View Maths as: Images | MathML

## Resolution

Keywords: clause, inference rules, rule of inference, unifier

### Categories: Logic Programming , Theorem Proving

Author(s): Alan Bundy

A rule of inference of Predicate Calculus used to deduce a new formula from two old ones. It has been used extensively in automatic Theorem Proving, because it is an efficient alternative to traditional rules of inference in mathematical logic. All the three formulae involved must be in Clausal Form. If C and D are clauses and the P and Q are atomic formulae then the rule is



where $\theta$ is the most general unifier of all the P and Q , and is obtained by Unification. Resolution is the execution mechanism of Prolog.

### References:

• Chang, C. and Lee, R.C., Symbolic Logic and Mechanical Theorem Proving , Academic Press, New York, 1973.