Note on Paramodulation

Here's a better description of the paramodulation rule we talked about in class. Let

• $s$, $t$, and $r$ be terms
• $\gamma[r]$ be a (possibly negated) literal that contains term $r$ as a subexpression
• $\theta = {\rm Unify}(s,r)$, and
• $\alpha$ and $\beta$ be (possibly empty) sets of literals.

Then, given a clause

$$\alpha \vee (s = t)$$

and another clause

$$\beta \vee \gamma[r]\;\;,$$

you may conclude

$$(\alpha \vee \beta \vee \gamma[t])\theta\;\;.$$

Here's an example. Given

$$n(g(C)) \vee (f(g(B)) = A)$$

and

$$q(x) \vee p(h(f(x)))$$

we can conclude

$$n(g(C)) \vee q(g(B)) \vee p(h(A))$$

by setting $s = f(g(B))$, $t = A$, $r = f(x)$, $\gamma[\cdot] = p(h(\cdot))$, and $\theta = \{g(B)/x\}$.