Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML


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.



Add Comment

No comments.