Resolution

Logik besteht aus vielen Regeln ("Modus Ponens", "Kettenschluss"...). Für Computer ist das zu kompliziert. Alan Robinson (1965) fand die eine Regel, sie alle zu knechten. Die Resolutionsregel: Wenn gilt: "A oder B". Und gilt: "Nicht A oder C". Dann gilt: "B oder C". Warum? Weil A entweder wahr oder falsch ist. Wenn A wahr -> Dann ist "Nicht A" falsch -> Also muss C wahr sein. Wenn A falsch -> Dann muss B wahr sein. Einer von beiden (B oder C) gewinnt immer. Mit dieser einen Regel kann man alles beweisen (in der Prädikatenlogik 1. Stufe).

Merksatz: Eine logische Ableitungsregel, die verwendet wird, um Beweise durch Widerspruch zu führen, indem Klauseln mit komplementären Literalen (P und nicht-P) zu einer neuen Klausel (Resolvente) verschmolzen werden.

Prolog basiert komplett darauf (SLD-Resolution). Wenn du prolog startest, macht es nichts anderes als Resolution + Unifikation. Auch automatische Beweiser (Vampire, E) nutzen Resolution.

1. Refutation Completeness

Resolution ist "widerlegungsvollständig". Das heißt: Wenn eine Formel einen Widerspruch enthält, wird Resolution ihn finden (die "Leere Klausel"). Es heißt nicht, dass es immer terminiert, wenn kein Widerspruch da ist (Halteproblem lässt grüßen).

2. Unifikation

Für Prädikatenlogik ("Alle Menschen sind sterblich") reicht einfaches String-Matching nicht. Man braucht Unifikation, um Variablen passend zu machen. Sterblich(X) und NichtSterblich(Sokrates). Unifikator: X = Sokrates. Resolution: Widerspruch!

1. Ordered Resolution & Selection

In einem großen System (z.B. Verifikation eines Kernel-Treibers) gibt es Millionen von Klauseln. Wenn man blind alles mit allem resolviert, explodiert der Speicher. Lösung: Literal Ordering. Man definiert eine Ordnung auf den Symbolen. Man darf nur das "größte" Literal einer Klausel resolvieren. Zusammen mit Literal Selection (der Solver wählt gezielt ein "schweres" Literal aus) wird der Suchbaum massiv beschnitten. Das macht den Unterschied zwischen einem Beweis, der 100 Jahre braucht, und einem, der in 2 Sekunden fertig ist.

2. Set of Support Strategy

Eine der wichtigsten Heuristiken. Man teilt das Wissen in zwei Mengen:

Axiome: Das Grundwissen ("Alle Menschen sterblich", "Sokrates ist Mensch"). Diese sind meist konsistent.
Negierte Anfrage: "Annahme: Sokrates ist NICHT sterblich." Der Solver sorgt dafür, dass mindestens eine der beiden Klauseln in jeder Resolution aus der "Anfrage-Welt" stammen muss. Man resolviert niemals Axiome miteinander, weil man weiß, dass daraus kein Widerspruch entstehen wird. Man arbeitet sich von der Anfrage "rückwärts" zu den Fakten vor.

3. Hyper-Resolution

Statt immer nur zwei Klauseln zu nehmen, nimmt man eine "Kern-Klausel" (mit vielen negativen Literalen) und klatscht sie gleichzeitig gegen mehrere "Satelliten-Klauseln" (mit positiven Literalen). In einem Schritt werden alle negativen Literale "weggeknallt". Das Ergebnis ist eine rein positive Klausel. In der Forschung (z.B. beim Otter oder Prover9 Beweiser) ist Hyper-Resolution unschlagbar, weil sie riesige logische Schritte macht, für die einfache Resolution hunderte Zwischenschritte bräuchte.