# Catalogue of Artificial Intelligence Techniques

View Maths as: Images | MathML

## 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[${t}^{\prime }$ ] and D are clauses, where C[${t}^{\prime }$ ] indicates that C contains a particular occurrence of ${t}^{\prime }$ , then the rule is: 

C[t']         D s=t (C[s] D)          C[t']         Dt=s (C[s] D) 

where $\theta$ is the most general unifier of $t$ and ${t}^{\prime }$ , and is obtained by Unification. C[$s$ ] indicates that only the particular occurrence of ${t}^{\prime }$ is replaced by $s$ in C, other occurrences of ${t}^{\prime }$ are untouched.

### References:

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