Schritte der Grundresolution

Dies sind die wichtigen Schritte der Grundresolution:

-       Bereinigung durch gebundene Umbenennung

-       Umwandlung in Pränexnormalform

-       Skolemisierung

-       Umwandlung der Matrix in Konjunktive Normalform

-       Anwendung des Grundresolutionsalgorithmus

Schritt 1: Bereinigung durch gebundene Umbenennung

Zu jeder Formel gibt es eine äquivalente andere Formel in bereinigter Form.

Eine Formel ist bereinigt wenn es keine Variable in der Formel gibt, die in der Formel sowohl gebunden als auch frei vorkommt, und wenn hinter allen vorkommenden Quantoren verschiedene Variablen stehen.

Schritt 2: Umwandlung in Pränexnormalform

Quantoren alle am Anfang sammeln. Im hinteren Teil der Formel dürfen am Ende keine Quantoren mehr vorkommen.

Zu jeder Formel existiert eine äquivalente Formel in Pränex-Normalform.

 Schritt 3: Skolemisierung

Existenzquantoren eliminieren durch ersetzen von Variablen durch Funktionszeichen. Ersetze nur die Variablen, die von einem Existenzquantor gebunden werden und streiche danach den Existenzquantor aus.

Schritt 4: Umwandlung der Matrix in Konjunktive Normalform

Umwandlung der Matrix erfolgt durch syntaktisches Umformen.

Schritt 5:  Anwendung des Grundresolutionsalgorithmus

Als Eingabe dient unsere Formel in Skolemform mit einer Matrix in Konjunktive Normalform. Einführung des Herbrand-Universum. Alle Elemente der Herbrand-Universums werden mittels UND verbunden. Somit ergeben sich die folgenden Grundinstanzen:

-       F1 = P(a) ^ P(f(a))

-       F2 = P(f(a)) ^ P(f(f(a)))

-       Usw.

Weiter gilt, das Beispielsweise P(f(a)) ^ ¬P(f(a)) KEINE GRUNDINSTANZ VON F ist.

Lässt sich aus der Verbindung obiger Teilformeln F1 … Fn mit UND eine leere Klausel ableiten, dann ist F unerfüllbar.