Catalogue of Artificial Intelligence Techniques
Keywords: clause, rule of inference, unifier
Categories: Theorem Proving
Author(s): Alan Bundy
A rule of inference of Predicate Calculus, used to deduce a new formula from two old ones. It is used in Automatic Theorem Proving, in conjunction with Resolution, as an alternative to the axioms of equality. All the three formulae involved must be in Clausal Form. If C[ ] and D are clauses, where C[ ] indicates that C contains a particular occurrence of , then the rule is:
C[t'] D s=t (C[s] D) C[t'] Dt=s (C[s] D)
where is the most general unifier of and , and is obtained by Unification. C[ ] indicates that only the particular occurrence of is replaced by in C, other occurrences of are untouched.
- Bundy, A., The Computer Modelling of Mathematical Reasoning, Academic Press, London, 1983, pp.80--83, also second edition, 1986