Resolutionsableitung

Eine Resolutionsableitung einer Klausel $C$ aus einer Klauselmenge $\mathrm{\Phi }$ ist eine endliche Folge von Klauseln $(C_1,\dots ,C_n)$, sodass $C_n=C$ und jede Klausel $C_i$ in der Folge entweder ein Element von $\mathrm{\Phi }$ ist oder eine Resolvente von zwei früheren Klauseln in der Folge ist ($C_i=\text{Res}(C_j,C_k)$ mit $j,k<i$).