Catalogue of Artificial Intelligence Techniques

   

Jump to: Top | Entry | References | Comments

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 θ is the most general unifier of all the P and Q , and is obtained by Unification. Resolution is the execution mechanism of Prolog.


References:


Comments:

Add Comment

No comments.