Resolution (Logik)

Die Resolution der Aussagenlogik ist ein Verfahren, um eine Formel F, die in konjunktiver Normalform vorliegt, auf Erfüllbarkeit und Gültigkeit zu testen. Resolution sollte im eigentlichen Sinne aber nur benutzt werden um die Unerfüllbarkeit einer Formel zu prüfen, da der Test auf Erfüllbarkeit nicht entscheidbar ist. Daher wird zum Beweis der Erfüllbarkeit oft einfach die Negation zum Widerspruch geführt.

Dabei sind folgende Aussagen möglich:

  1. führt Res(F) zu einem Widerspruch, ist F unerfüllbar
  2. führt Res(-F) zu einem Widerspruch, ist F gültig

Resolution bezeichnet in der Logik eine Methode, die es erlaubt, von

(A_1 \vee A_2 \vee \dots \vee A_n) \wedge (B_1 \vee B_2 \vee \dots \vee B_m \vee \neg A_1)

auf

A_2 \vee \dots \vee A_n \vee B_1 \vee \dots \vee B_m

zu schließen.

Bei der linearen Resolution wird in jedem Resolutionsschritt immer mit der Resolvente des letzten Schritts (bzw. im ersten Schritt mit einer Startklausel) resolviert. Lineare Resolution ist vollständig, d.h. wenn man die leere Klausel aus einer Klauselmenge K resolvieren kann, dann gibt es in K eine Klausel, aus der man die leere Klausel linear resolvieren kann.

Dieser Artikel behandelt denselben Inhalt wie der Artikel Resolutionskalkül und sollte bei Gelegenheit mit diesem vereinigt werden.

Dieser Artikel bedarf einer Überarbeitung. Eine Begründung befindet sich in der Regel auf der Diskussionsseite. Wenn du Lust hast, verbessere den Artikel und entferne anschließend diesen Baustein.

See also: Resolution (Logik), Aussagenlogik, Konjunktive Normalform, Logik, Resolutionskalkül