Resolutionswiderlegung

Eine Resolutionswiderlegung einer Klauselmenge $\mathrm{\Phi }$ ist eine Resolutionsableitung der leeren Klausel $\square$ aus $\mathrm{\Phi }$. Sie ist ein formaler Beweis dafür, dass die Klauselmenge $\mathrm{\Phi }$ unerfüllbar ist.