Factoring (Logic)

Factoring is the process of reducing the complexity of a disjunctive clause by replacing predicates through unification. It can sometimes be a necessary step in predicate resolution.

Definition §

Factoring ^definition

Let $C$ be a disjunctive clause containing two unifiable predicates $A$ and $B$. Given a most general unifier, $\theta$, $C$ can be factored by substituting it with $C[\theta ]$, eliminating one of $A$ or $B$

$$C=A\vee B\vee \cdots \stackrel{Factored}{\to }C[\theta ]=\cancel{A\vee B}A[\theta ]\vee \dots$$

Examples §

Take the disjunctive clause $C=(P(x,y)\vee Q(x)\vee P(a,c))$. The predicates $P(x,y)$ and $P(a,c)$ are unifiable with $\theta =\{x\mapsto a,y\mapsto c\}$ being their MGU.

Then, we can replace $C$ with $C[\theta ]$

$$C=(P(x,y)\vee Q(x)\vee P(a,c))\approx C[\theta ]=(P(a,c)\vee Q(a))$$

where $\approx$ means equisatisfiable.