Ein Beweisverfahren, das die Unerfüllbarkeit einer Menge von Klauseln demonstriert, indem wiederholt die Resolutionsregel angewandt wird, um neue Klauseln zu erzeugen, bis die leere Klausel abgeleitet ist, was einen Widerspruch anzeigt.

Prinzip

Anwendung der binären Resolutionsregel zum Kombinieren von Klauseln mit komplementären Literalien, gegebenenfalls mit Unifikation im ersten Ordnungssfall, und Steuerung der Suche (Selektion, Ordnung, Subsumption), sodass die Ableitung der leeren Klausel erreichbar ist, falls die Klauselmenge unerfüllbar ist.

Demonstration

Aus den Klauseln {p ∨ q, ¬q ∨ r, ¬r, ¬p} wird p ∨ q mit ¬p resolviert, um q abzuleiten; q wird mit ¬q ∨ r resolviert, um r abzuleiten; r wird mit ¬r resolviert, um die leere Klausel abzuleiten und damit die ursprüngliche Menge zu widerlegen.

Fehlanwendung

Propositionale Resolutionsverfahren unverändert auf unbeschränkte prädikatenlogische Klauselmengen anzuwenden, ohne Unifikation oder ohne Terminationstrategien, oder anzunehmen, Resolution liefere stets kurze oder menschenlesbare Beweise; naive Expansion kann kombinatorisch explodieren.

Konsequenz

Resolution ist korrekt und für die propositionale Logik sowie entsprechend konfigurierte erste-Ordnungseinstellungen refutationstvollständig: Ist die Klauselmenge unerfüllbar, existiert eine Widerlegung; sie bildet die Grundlage vieler automatischer Theorembeweiser und SAT-Solver (nach KNF-Umformung und ggf. zusätzlichen Mechanismen).

Umkehrung

Die Umkehr ist die konstruktive Beweissuche (z. B. Tableau oder natürliche Deduktion), die eine direkte Herleitung der Formel statt einer Widerlegung durch Widerspruch anstrebt; in der invertierten Vorgehensweise versucht man, ein Modell oder einen direkten Beweis zu konstruieren statt einen Widerspruch herzuleiten.

Abgrenzung

Anwendbar auf Klauselgestalt (KNF); reine Resolution konstruiert nicht automatisch Modelle für erfüllbare Mengen und kann in der ersten Ordnung ohne geeignete Strategien oder Einschränkungen (z. B. Ordnung, Selektion, Loop-Check) nicht terminieren.

Semantische Spannung

Es besteht Spannung zwischen Resolution und sequenten- oder deduktionsnatürlichen Stilen: Resolution zielt auf Widerlegung und algorithmische Suche über Klauseln ab, während andere Stile konstruktive Zeugenextraktion und andere Beweisformen in den Vordergrund stellen.

Synthese

Resolution-Widerlegung vereint die lokale Resolutionsregel mit Unifikation (in der ersten Ordnung) und globaler Suchsteuerung, sodass aus Klauselmengen Widersprüche abgeleitet werden; sie wandelt das Beweisproblem in eine systematische Klausel-Eliminationssuche um, die entweder die leere Klausel liefert oder keine Widerlegung findet.