Catalogue of Artificial Intelligence Techniques
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
- Chang, C. and Lee, R.C., Symbolic Logic and Mechanical Theorem Proving
, Academic Press, New York, 1973.