# Catalogue of Artificial Intelligence Techniques

## Paramodulation

**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.

### References:

- Bundy, A.,
*The Computer Modelling of Mathematical Reasoning*, Academic Press, London, 1983, pp.80--83, also second edition, 1986 .

### Comments:

No comments.