General Resolution Example

Consider the two clauses:

Cu = { p(x, f(a)), p(x, f(y)), q(y) } = { Lu1, Lu2, Lu3 }

Cv = { ¬ p(z, f(a)), ¬ q(z) } = {Lv1, Lv2}

(a) Resolve {lu1} = { p(x, f(a)) }

with {lv1} = {¬ p(z, f(a)) }

to obtain { p(z, f(y)), ¬ q(z), q(y) }
This is Binary Resolution.

(b) Resolve {lu1, lu2} = { p(x, f(a)), p(x, f(y)) }

with {lv1} = {¬ p(z, f(a)) }

to obtain { q(a), ¬ q(z) }
This is Full Resolution.

There are four possible different resolvents:

three resolving on p (two of these are binary)

one resolving on q (this is binary)