Mathematische Logik und Grundlagenforschung

Vollständige Resolutionskalküle für PROLOG

Inaugural-Dissertation zur Erlangung des Doktorgrades

der Naturwissenschaften im Fachbereich Mathematik der Westfälischen Wilhelms-Universität Münster

vorgelegt von Karl Stroetmann aus Ascheberg

Dekan:  Frau Prof. Dr. E. Peveling
Erster Referent:  Herr Prof. Dr. J. Diller
Zweiter Referent:  Herr Prof. Dr. W. Pohlers
Mündliche Prüfung: 21., 24. und 25. 6. 1991
Tag der Promotion: 25. 6. 1991

Einleitung

Die Problemstellung

Ein wesentlicher Teil der Mathematik besteht in der Suche nach Algorithmen, die vorgegebene Probleme auf mechanische Weise lösen. Waren diese Probleme im Anfang auch rein arithmetischer oder geometrischer Natur, so kam doch schon relativ früh der Gedanke auf, Algorithmen zu entwickeln, die in der Lage sind, abstrakte mathematische Probleme zu lösen. Die ersten Versuche dieser Art gehen wohl auf den katalanischen Philosophen Raymundus Lullus zurück, der mit seiner “Ars magna” 1274 einen Algorithmus zur Lösung aller mathematischen Probleme gefunden zu haben glaubte. Die ersten ernsthaften Bemühungen in dieser Richtung wurden von Leibniz (1646–1716) durchgeführt, der erkannte, daß ein wesentlicher Schritt zum Auffinden eines universellen mathematischen Algorithmus in der Formalisierung der mathematischen Sprache bestand.

Der entscheidende Durchbruch gelang Kurt Gödel 1930 mit dem Beweis seines Vollständigkeitssatzes für die Prädikatenlogik erster Stufe. Damit war erstmalig ein Verfahren gefunden, das in der Lage war, jeden korrekten mathematischen Satz der ersten Stufe mechanisch zu beweisen. Das positive Resultat von Gödel wurde bald darauf durch negative Resultate abgegrenzt.

1931 zeigte der 1. Gödel’sche Unvollständigkeitssatz, daß sowohl die Zahlentheorie, als auch jede konsistente Erweiterung der Zahlentheorie notwendig unvollständig ist. Dieser Satz zeigt eine prinzipielle Grenze der klassischen Prädikatenlogik auf: Es gibt kein rekursives System von erststufigen Axiomen, das die Struktur der natürlichen Zahlen vollständig beschreibt. Dies impliziert insbesondere die Unentscheidbarkeit der Arithmetik. Das Bild der klassischen Prädikatenlogik wurde 1935 durch ein weiteres negatives Resultat abgerundet. Alonzo Church konnte zeigen, daß die klassische Prädikatenlogik mit Gleichheit im allgemeinen unentscheidbar ist.

Durch die Sätze von Gödel und Church waren die Möglichkeiten für die Realisation des Traumes von Raymundus Lullus abgesteckt. Es ging nun darum, denn Gödelschen Vollständigkeitssatz möglichst effizient zu implementieren. Den ersten wirklichen Durchbruch in diese Richtung schaffte John. A. Robinson 1965 [Rob65], indem er einen vollständigen Kalkül vorstellte, der mit einer einzigen Schlußregel, der sogenannten Resolutionsregel, arbeitet. Dieser Kalkül wurde später die Grundlage fast aller auf Rechnern implementierten Algorithmen, die zum automatischen Beweisen von mathematischen Theoremen eingesetzt wurden.

Der Resolutionskalkül wurde ebenfalls die Grundlage der Programmiersprache PROLOG. Im Gegensatz zu den bis dahin existierenden imperativen Programmiersprachen, in denen der Anwender einen Algorithmus zur Lösung des zu bearbeitenden Problems angeben muß, ist PROLOG von der Idee her eine deklarative Sprache. Im Idealfall sollte der Anwender einer deklarativen Sprache nur noch eine exakte formale Spezifikation des zu bearbeitenden Problems angeben, um den Algorithmus kümmert sich dann der Computer. Bei PROLOG dient als Spezifikationssprache ein Fragment der Prädikatenlogik ohne Gleichheit, die Menge der Hornklauseln. Diese Formelklasse wurde gewählt, weil sich der Resolutionskalkül für dieses Fragment der Prädikatenlogik in sehr effizienter Weise implementieren läßt.

Obgleich sich ein beachtliches Spektrum mathematischer Probleme durch Hornklauseln beschreiben läßt, so ist natürlich eine Erweiterung des Resolutionskalküles auf größere Formelklassen wünschenswert. Die vorliegende Arbeit beschäftigt sich mit den damit verbundenen Problemen. Es werden insbesondere zwei Ansätze vorgestellt, die geeignet sind, die Deduktionskapazität von PROLOG–Programmen zu vergrößern. Es handelt sich dabei zum einen um ein Verfahren, gewisse einfache algebraische Theorien in PROLOG zu implementieren. Zum anderen beschäftigen wir uns mit dem Problem, negative Information in PROLOG– Programmen zu berücksichtigen.

Ein Herzstück des Resolutionskalküls von J. A. Robinson besteht in dem in [Rob65] vorgeschlagenen Unifikationsalgorithmus. Mit diesem Algorithmus (insbesondere in der von [CB83] vorgeschlagenen Version) ist es in effizienter Weise möglich, abstrakte Gleichungen zwischen Termen auf der Grundlage der Leibnizschen Gleichheitsaxiome zu lösen. Da mittlerweile Unifikationsalgorithmen für anspruchsvollere algebraische Theorien entwickelt wurden (vergleiche etwa [Siek89], [FH86] oder [Knight89]), ist es ziemlich naheliegend zu versuchen, Resolutionskalküle zu entwickeln, die auf diesen Unifikationsalgorithmen aufsetzen. Dieser Aufgabe widmen wir uns im ersten Teil der Arbeit.

Im zweiten Teil befassen wir uns mit dem Problem, negative Information in PROLOG–Programmen zu berücksichtigen. Der klassische Ansatz, negative Information in PROLOG—Programmen zu verarbeiten, besteht in der von Clark

[Cl78] eingeführten SLDNF–Resolution. Bedauerlicherweise sind hier bisher nur für sehr ausdrucksschwache Fragmente der Klasse der “normalen” Programme Vollständigkeitsaussagen erzielt worden. Hier stellt sich die Frage, ob dies aus prinzipiellen Gründen so ist, oder ob sich Vollständigkeitsaussagen auch für Teilklassen der normalen Programme erzielen lassen, die deutlich über die Klasse der sogenannten zulässigen hierarchischen Programme, für die bisher positive Ergebnisse vorliegen, hinausgehen. Um die Dringlichkeit des Problems klarzumachen, zitieren wir Lloyd [Llo87]. Er schreibt auf Seite 100:

“The completeness of the negation as failure rule and SLDNF– resolution are of such importance that finding more general completeness results is an urgent priority.”

Wir stellen in dieser Arbeit die Klasse der konsistent geordneten Programme vor, für die wir die Vollständigkeit der SLDNF–Resolution nachweisen können.

Organisation der Arbeit

Die vorliegende Arbeit besteht aus zwei Teilen. Im ersten Teil, der aus den Kapiteln 1 – 4 besteht, beschäftigen wir uns mit der Suche nach einem Resolutionskalkül für algebraische Theorien, für die ein Unifikationsalgorithmus vom Typ ω bekannt ist. Die verbleibenden Kapitel 5 – 8 beschäftigen sich dann mit der SLDNF– Resolution.

Das erste Kapitel dient der Normierung von Syntax und Semantik der Prädikatenlogik. Dies erscheint uns insbesondere deswegen notwendig, weil die klassische Darstellung der Theorie, wie sie beispielsweise in [Llo87] zu finden ist, viel zu schwerfällig ist und sich der im Bereich der Prädikatenlogik verwendeten Begrifflichkeiten und Notationen nur unzureichend bedient. Zum Abschluß des ersten Kapitels stellen wir einen widerlegungsvollständigen Kalkül vor, der mit einer Variante der Schnittregel, der Kontraktionsregel und der Substitutionsregel arbeitet. Dieser Kalkül bildet später die Grundlage für einen Resolutionskalkül.

Im zweiten Kapitel wiederholen wir kurz die wichtigsten Ergebnisse der Unifikationstheorie, verweisen aber, was Beweise der zusammengestellten Tatsachen angeht, auf die Literatur.

Im dritten Kapitel sind wir in der Lage, einen Resolutionskalkül vorzustellen, der für die algebraischen Theorien Anwendungen findet, für welche ein geeigneter Unifikationsalgorithmus vorliegt. Wir schränken diesen Kalkül auf die Klasse der Hornformeln ein und zeigen, daß der Kalkül für diese Klasse besonders effizient wird.

Im vierten Kapitel analysieren wir den konstruktiven Gehalt der mit dem im dritten Kapitel vorgestellten Resolutionskalkül für Hornformeln geführten Beweise. Wir zeigen, daß der von uns vorgestellte Kalkül im Hinblick auf Existenzaussagen konstruktiv ist. Es gilt sogar mehr: Wir beweisen mit Theorem (4.8), daß sich jede korrekte Antwort als Instanz einer berechneten Antwort auffassen läßt. Dabei werden die Begriffe “korrekte Antwort” und “berechnete Antwort” analog zu [Llo87] definiert.

Der zweite Teil der Arbeit beschäftigt sich mit der Inkorporation negativer Information in PROLOG–Programme. Da aus einem PROLOG–Programm keine negativen Informationen ableitbar sind, müssen wir hier den Rahmen der klassische Prädikatenlogik verlassen und sogenannte nichtmonotone Schlußregeln untersuchen. Wir folgen dabei Clark [Cl79], der als nichtmonotone Schlußregel die “negation– as–failure”–Regel vorschlägt, da sich mit dieser Regel die von Reiter [Reit78] eingeführte CWA approximativ implementieren läßt. Die CWA beruht auf dem Prinzip, aus der Nichtableitbarkeit einer geschlossenen Primformel A auf ihre Negation ¬A zu schließen:

⊬ A ⇒ ⊢ ¬A.

Diese Regel läßt sich schon deshalb nicht implementieren, weil im allgemeinen zu gegebener Sprache L und Theorie T die Menge

{ A∈L | T ⊬ A }

nicht rekursiv aufzählbar ist. Die obige Menge ist (für rekursiv axiomatisierte Theorien T) genau dann rekursiv aufzählbar, wenn die zugrunde liegende Theorie T entscheidbar ist. Wollen wir die CWA effektiv implementieren, so wird es unser Ziel sein müssen, ein entscheidbares Fragment der Prädikatenlogik zu finden, das für unsere Zwecke ausdrucksstark genug ist.

Im fünften Kapitel stellen wir die SLDNF–Resolution vor. Wir weichen dabei von der üblichen Darstellung ab, indem wir die Auswahlregel fest vorschreiben. Durch diese Einschränkung wird die Menge der möglichen SLDNF–Bäume übersichtlicher, so daß es später möglich wird, einen Vollständigkeitssatz zu formulieren. Wir schließen das fünfte Kapitel mit einer rein syntaktischen Korrektheitsaussage ab, die ohne die Einführung einer Semantik auskommt. Diese Aussage ist stärker als die semantische Korrektheit der SLDNF–Resolution bezüglich der Vervollständigung eines Programmes, da die Vervollständigung eines konsistenten normalen Programmes (alle normalen Programme haben diese Eigenschaft!) selbst nicht konsistent sein muß.

Im sechsten Kapitel führen wir den zentralen Begriff des bezüglich einer I/O–Spezifikation konsistent geordneten normalen Programmes ein. Eine I/O– Spezifikation dient dazu, das Ein/Ausgabe–Verhalten von PROLOG–Programmen zu analysieren. Die Klasse der konsistent geordneten Programme stellt sich als eine Klasse von normalen Programmen heraus, in der das Mittel der Rekursion nur in kontrollierter Form verwendet wird. Das hat zur Folge, daß die Herleitungen zu konsistent geordneten Programmen terminieren. Es zeigt sich, daß konsistent geordnete Programme trotzdem noch ausdrucksstark genug sind, um beispielsweise alle primitiv–rekursiven Funktionen berechnen zu können.

Im siebten Kapitel ernten wir die Früchte unserer Arbeit und beweisen verschiedene Vollständigkeitssätze für die Klasse der konsistent geordneten Programme. Wir beginnen mit einem syntaktischen Vollständigkeitssatz (7.2), der zeigt, daß für ein konsistent geordnetes Programm P und eine geschlossene Primformel A entweder

P ⊢ A oder P ⊢ ¬A

gilt. Daraus ergibt sich als Korollar die Entscheidbarkeit von geschlossenen Primformeln. Damit können wir dann zeigen, daß die SLDNF–Resolution für ein konsistent geordnetes Programm P bezüglich der durch die Vervollständigung comp(P) von P gegebenen Semantik vollständig ist. Außerdem beweisen wir in Theorem 7.17, daß sich jede “korrekte Antwort” für ein konsistent geordnetes Programm als Instanz einer mit Hilfe der SLDNF–Resolution gefundenen “berechneten Antwort” auffassen läßt. Abschließend zeigen wir, daß für konsistent geordnete Programme die Theorie comp(P) konsistent ist.

Im achten und letzten Kapitel untersuchen wir die Frage, inwieweit sich die üblicherweise verwendeten PROLOG–Programme konsistent ordnen lassen. Wir argumentieren, daß eine ganze Reihe von PROLOG–Programmen automatisch konsistent geordnet sind und führen als Beispiel ein Programm zur automatischen Differentiation an. Weiterhin stellen wir eine Transformationstechnik vor, mit deren Hilfe sich Programme, die a priori nicht konsistent geordnet sind, in konsistent geordnete Programme transformieren lassen. Abschließend geben wir zwei Beispiele für Programme, die sich aus prinzipiellen Gründen nicht konsistent ordnen lassen. Das eine Programm beinhaltet eine unbeschränkte Suche, also letztlich eine Art μ–Operator, beim anderen Programm geht es um die Berechnung der Ackermann–Funktion. Die Tatsache, daß die Ackermannfunktion nicht durch ein konsistent geordnetes Programm berechenbar ist, legt die Vermutung nahe, daß die konsistent geordneten Programme im wesentlichen genau die primitiv– rekursiven Funktionen berechnen können, denn die Ackermannfunktion ist eine der einfachsten rekursiven Funktionen, die nicht mehr primitiv–rekursiv sind. Diese Hypothese wird aber nicht weiter untersucht.

Danksagungen

Ich danke Herrn Prof. Dr. J. Diller für die Betreuung dieser Arbeit und für die sorgfältige Korrektur ihrer früheren Versionen. Bei Herrn Prof. Dr. Pohlers bedanke ich mich für ein gemeinsam durchgeführtes Seminar, durch das ich auf einige der in dieser Arbeit behandelten Probleme aufmerksam wurde.

Ferner bedanke ich mich bei Dr. A. Weiermann, Dr. M. Rathjen, Dr. J. Columbus und Dipl.–Math. A. Schlüter für zahlreiche nützliche Diskussionen, die ich im Zusammenhang zur Arbeit mit ihnen geführt habe. Zum Abschluß möchte ich mich bei dem gesamten Institut für mathematische Logik und Grundlagenforschung für die Förderung meiner wissenschaftlichen Arbeit bedanken.

Inhaltsverzeichnis

I Resolution für algebraische Theorien 1

1 Normierung von Syntax und Semantik 2 1.1 Die Syntax der Prädikatenlogik . . . . . . . . . . . . . . . . . . . 3 1.2 Semantik der Prädikatenlogik . . . . . . . . . . . . . . . . . . . . 5 1.3 Herbrand–Strukturen für E–Theorien . . . . . . . . . . . . . . . . 7 1.4 Ein widerlegungsvollständiger Kalkül . . . . . . . . . . . . . . . . 12

2 Unifikationstheorie 21

3 E–Resolution 23 3.1 E–Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.2 Die E–Prolog–Regel . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.3 Die eingeschränkte E–Prolog–Regel . . . . . . . . . . . . . . . . . 31 3.4 E–Resolution für Hornformeln . . . . . . . . . . . . . . . . . . . . 36

4 Korrekte und berechnete Antworten 39 4.1 Korrektheit berechneter Antworten . . . . . . . . . . . . . . . . . 41 4.2 Berechenbarkeit korrekter Antworten . . . . . . . . . . . . . . . . 44

II Untersuchungen zur Vollständigkeit der SLDNF–Resolution 48

5 SLDNF–Resolution 49 5.1 Definition der SLDNF–Resolution . . . . . . . . . . . . . . . . . . 51 5.2 Syntaktische Korrektheit . . . . . . . . . . . . . . . . . . . . . . . 56

6 Konsistent geordnete Programme 60 6.1 Erlaubte Programme . . . . . . . . . . . . . . . . . . . . . . . . . 61 6.2 Konsistente I/O–Spezifikationen . . . . . . . . . . . . . . . . . . 63 6.3 Geordnete Programme . . . . . . . . . . . . . . . . . . . . . . . . 67 6.4 Adäquatheit konsistent geordneter Programme . . . . . . . . . . 73 7 Vollständigkeit der SLDNF–Resolution 78

7.1 Syntaktische Vollständigkeit der SLDNF–Resolution . . . . . . . 79 7.2 Die Vervollständigung eines normalen Programmes . . . . . . . . 83 7.3 Semantische Vollständigkeit der SLDNF–Resolution . . . . . . . 86 7.4 Die Konsistenz von comp(P) . . . . . . . . . . . . . . . . . . . . 93

8 Anwendungen von konsistent geordneten Programmen 98 8.1 Symbolische Differentiation . . . . . . . . . . . . . . . . . . . . . 100 8.2 Simulation von Pushdown–Automaten . . . . . . . . . . . . . . . 101 8.3 Negative Beispiele . . . . . . . . . . . . . . . . . . . . . . . . . . 106

Teil I

Kapitel 1

Resolution für algebraische Theorien Normierung von Syntax und Semantik

In diesem einführenden Kapitel normieren wir die Syntax und Semantik der Prädikatenlogik. Wir beginnen in den ersten beiden Abschnitten mit einer Definition von Syntax und Semantik der klassischen Prädikatenlogik. Diese beiden Abschnitte dienen nur dem Zweck, einige Schreibweisen und Begriffe festzulegen. Selbstverständlich wird vom Leser eine gewisse Vertrautheit mit den dort zusammengestellten Begriffen erwartet.

Im dritten Abschnitt führen wir eine spezielle Klasse von Formeln ein, die sogenannten Klauseln. Charakteristisch für Klauseln ist, daß in ihnen keine Existenzquantoren positiv auftreten. Dadurch wird es möglich, auch die Strukturen, die wir untersuchen werden, einzuschränken. Es zeigt sich, daß zur Ableitung eines Vollständigkeitssatzes bereits Termmodelle ausreichen, deren Träger nur aus geschlossenen Termen bestehen. Dazu zeigen wir, daß jede erfüllbare quantorenfreie Formelmenge ein Herbrandmodell besitzt.

Im vierten Abschnitt beschäftigen wir uns mit einem Kalkül, der lediglich mit drei Ableitungsregeln arbeitet. Dieser Kalkül ist zwar nicht vollständig, aber widerlegungsvollständig. Dabei nennen wir einen Kalkül widerlegungsvollständig, wenn er in der Lage ist, aus jeder inkonsistenten Menge von Formeln das Falsum abzuleiten. Der Kalkül, den wir vorstellen, besteht nur aus der Schnittregel, der Kontraktionsregel und der Substitutionsregel. Er wird die Grundlage für alle weiteren Überlegungen sein. Der Beweis der Widerlegungsvollständigkeit späterer Kalküle wird immer darauf hinauslaufen, daß wir Widerlegungen, die mit Schnitt-, Kontraktions– und Substitutionsregel geführt worden sind, in Widerlegungen übersetzen, die nur die Ableitungsregeln des gerade untersuchten Kalküls benutzen.

1.1 Die Syntax der Prädikatenlogik

Definition 1.1 (Alphabet) Ein Alphabet A = (Λ, Σ) ist durch zwei paarweise disjunkte Symbolmengen gegeben:

1. Die Menge Λ der Funktionszeichen.

2. Die Menge Σ der Prädikatszeichen.

Dabei ist jedem Funktions– und Prädikatszeichen eine Stellenzahl n∈N zugeordet. 0–stellige Funktionszeichen heißen Konstanten, 0–stellige Prädikatszeichen bezeichnen wir als Aussagensymbole. Ferner verlangen wir, daß das Gleicheitszeichen = kein Element von Σ ist.

Für die nun folgende Definition von Termen und quantorenfreien Formeln nehmen wir stets ein Alphabet A = (Λ, Σ) und eine abzählbar unendliche Menge V von Variablen als gegeben an.

Definition 1.2 (Terme) Die Menge T der Terme wird induktiv definiert durch:

1. Jede Variable x∈V ist ein Term.

2. Ist f ∈ Λ ein n–stelliges Funktionszeichen und sind t_{1}, ⋯, t_{n} Terme, so ist auch ft_{1} ⋯ t_{n} ein Term.

Definition 1.3 (quantorenfreie Formeln) Die Menge der quantorenfreien Formeln wird induktiv definiert durch:

1. ⊥ und ⊤ sind quantorenfreie Formeln.

2. Sind t_{1}, ⋯, t_{n} Terme und ist p∈Σ ein n–stelliges Prädikatszeichen, so ist pt_{1} ⋯ t_{n} eine quantorenfreie Formel.

3. Sind t und s Terme, so ist =ts eine quantorenfreie Formel.

4. Sind F_{1} und F_{2} quantorenfreie Formeln, so sind auch

¬F_{1}, (F_{1} ∧ F_{2}), (F_{1} ∨ F_{2}) und (F_{1} → F_{2})

quantorenfreie Formeln.

Formeln der Gestalt ⊥, ⊤, pt_{1} ⋯ t_{n} und = st nennen wir atomare Formeln oder auch Primformeln.

Eine Formel der Gestalt = ts werden wir in der Regel als s = t mitteilen. Wir treffen die üblichen Vorkehrungen, um Klammern einzusparen und vereinbaren, daß ¬ am stärksten und → am schwächsten bindet. Gelegentlich bezeichnen wir die Menge aller Formeln zu einem Alphabet A auch als Sprache L zum Alphabet A. In der Regel werden wir später das Alphabet nicht mehr erwähnen, sondern als gegeben annehmen. Wir haben bei unseren weiteren Überlegungen keinen Bedarf für Formeln, in denen Quantoren auftreten. Wenn wir daher im folgenden von Formeln sprechen werden, so meinen wir immer quantorenfreie Formeln.

Definition 1.4 (Literale) Ist P eine Primformel, so bezeichnen wir P und ¬P als Literale. Hat das Literal L die Gestalt ¬P, so steht ¬L für die Primformel P.

Ist t ein Term und F eine quantorenfreie Formel, so bezeichnen wir mit FV (t) bzw. FV (F) die Menge der in t bzw. F auftretenden Variablen. (Exakter wäre hier eine induktive Definition.) Eine Formel F bzw. ein Term t ist geschlossen, falls FV (F) = ∅ bzw. FV (t) = ∅ ist.

Definition 1.5 (Substitutionen) Eine Abbildung σ : V → T heißt eine Substitution, falls die Menge

dom(σ) := {x∈V : σ(x) ≠ x}

endlich ist. Ist σ eine Substitution, so definieren wir

var(σ) := ⋃_{x∈dom(σ)} FV (σ(x)).

Wir setzen eine Substitution σ kanonisch fort zu einer Abbildung σ^{∗} : T → T , die auf allen Termen definiert ist:

1. σ^{∗}(x) := σ(x) für alle x∈V.

2. Ist f ∈ Λ ein n–stelliges Funktionszeichen und sind t_{1}, ⋯, t_{n} Terme, so

definieren wir

σ^{∗}(ft_{1} ⋯ t_{n}) := fσ^{∗}(t_{1}) ⋯ σ^{∗}(t_{n}).

Wir werden im folgenden nicht mehr zwischen σ und σ^{∗} unterscheiden. Die Menge aller Substitutionen bezeichnen wir mit SUB.

Für Substitutionen benutzen wir später häufig die Postfix–Notation. Ist t ein Term und σ eine Substitution, so schreiben wir tσ statt σ(t). Die Komposition στ zweier Substitutionen σ und τ definieren wir als

tστ := τ(σ(t)).

Selbstverständlich gilt für diese Form der Komposition das Assoziativgesetz. Ist σ eine Substitution, für die

dom(σ) = {x_{1}, ⋯, x_{n}} und σ(x_{1}) = t_{1}, ⋯, σ(x_{n}) = t_{n}

gilt, so schreiben wir

σ = [x_{1}/t_{1}, ⋯ x_{n}/t_{n}].

Definition 1.6 (Instanz) Sind s und t zwei Terme und ist σ eine Substitution, so daß s = tσ gilt, so heißt s eine Instanz von t. Instanzen von quantorenfreien Formeln werden analog definiert.

Definition 1.7 (grund(X)) Ist X eine Menge von quantorenfreien Formeln, so definieren wir die Menge grund(X) als die Menge aller geschlossenen Instanzen von Formeln aus X:

grund(X) := {F σ : F ∈X & σ ∈SUB & FV (F σ) = ∅}.

1.2 Semantik der Prädikatenlogik

Definition 1.8 (Struktur) A = (A, (f_{A})_{f∈Λ}, (p_{A})_{p∈Σ}) heißt eine Struktur zum Alphabet A = (Λ, Σ), falls gilt:

1. A ist eine nichtleere Menge von Individuen, die wir auch als Träger der Struktur A bezeichnen.

2. (f_{A})_{f∈Λ} ist eine Familie von Funktionen, die zu jedem n–stelligen Funktionszeichen

f ∈Λ eine Funktion

f_{A} : A^{n} → A

enthält. Im Falle n = 0 ist f_{A} ein Element von A.

3. (p_{A})_{p∈Σ} ist eine Familie von Prädikaten, die zu jedem n–stelligen Prädikatszeichen

p∈Σ eine Funktion

p_{A} : A^{n} → {W, F }

enthält. Im Falle n = 0 ist p_{A} einer der Wahrheitswerte W oder F.

Ist A eine Struktur, so bezeichnen wir den Träger von A mit |A|.

Definition 1.9 (Variablenzuweisung) Ist A eine Struktur, so nennen wir eine Abbildung der Form ω : V → |A| eine Variablenzuweisung.

Variablenzuweisungen werden gelegentlich auch als Variablenbelegungen bezeichnet.

Definition 1.10 (Wert eines Termes) Ist A eine Struktur, so definieren wir induktiv den Wert eines Termes t unter einer Variablenzuweisung ω durch:

1. t = x∈V. Dann setzen wir:

wert_{A}^{ω}(t) := ω(x).

2. t = ft_{1} ⋯ t_{n}. In diesem Fall definieren wir:

wert_{A}^{ω}(t) := f_{A}(wert_{A}^{ω}(t_{1}), ⋯, wert_{A}^{ω}(t_{n})).

Falls der Term t geschlossen ist, hängt wert_{A}^{ω}(t) nicht mehr von ω ab. Dann schreiben wir für den Wert von t auch wert_{A}(t).

Definition 1.11 (Wert einer quantorenfreien Formel) Ist A eine Struktur, so definieren wir induktiv den Wert einer quantorenfreien Formel G unter einer Variablenzuweisung ω durch:

1. G = ⊥ bzw. G = ⊤. Wir definieren:

W ert_{A}^{ω}(⊥) := F und W ert_{A}^{ω}(⊤) := W.

2. G = pt_{1} ⋯ t_{n}. Dann setzen wir:

W ert_{A}^{ω}(G) := p_{A}(wert_{A}^{ω}(t_{1}), ⋯, wert_{A}^{ω}(t_{n})).

3. G hat die Form t = s. In diesem Fall setzen wir:

W ert_{A}^{ω}(G) := \{ \begin{matrix}W & falls wert_{A}^{ω}(s) = wert_{A}^{ω}(t); \\ F & sonst. \end{matrix}

4. G = ¬G_{1}. Wir vereinbaren:

W ert_{A}^{ω}(G) := \{ \begin{matrix}W & falls W ert_{A}^{ω}(G_{1}) = F; \\ F & sonst. \end{matrix}

5. G = (G_{1} ∧ G_{2}). Wir vereinbaren:

W ert_{A}^{ω}(G) := \{ \begin{matrix}W & falls W ert_{A}^{ω}(G_{1}) = W und W ert_{A}^{ω}(G_{2}) = W; \\ F & sonst. \end{matrix}

6. G = (G_{1} ∨ G_{2}). Wir vereinbaren:

W ert_{A}^{ω}(G) := \{ \begin{matrix}W & falls W ert_{A}^{ω}(G_{1}) = W oder W ert_{A}^{ω}(G_{2}) = W; \\ F & sonst. \end{matrix}

7. G = (G_{1} → G_{2}). Wir vereinbaren:

W ert_{A}^{ω}(G) := \{ \begin{matrix}W & falls W ert_{A}^{ω}(G_{1}) = F oder W ert_{A}^{ω}(G_{2}) = W; \\ F & sonst. \end{matrix}

Falls die Formel G geschlossen ist, hängt W ert_{A}^{ω}(G) nicht mehr von ω ab. Dann schreiben wir für den Wert von G auch W ert_{A}(G).

Definition 1.12 (Gültigkeit) Eine Formel F aus der Sprache L zum Alphabet A ist in einer Struktur A zum Alphabet A gültig, falls für jede Variablenbelegung ω : V → |A| gilt:

W ert_{A}^{ω}(F) = W.

In diesem Fall sagen wir, daß A ein Modell von F ist und schreiben

A ⊧ F.

Eine Formel F zum Alphabet A heißt allgemeingültig, wenn F in jeder Struktur zum Alphabet A gültig ist. Dafür schreiben wir

⊧ F.

Die Formel F heißt erfüllbar, wenn es eine Struktur A gibt, in der F gültig ist. Ist X eine Menge von Formeln und sind alle F ∈ X in A gültig, so sagen wir, daß A ein Modell von X ist und schreiben

A ⊧ X.

Definition 1.13 (logische Folgerung) Eine Formel G folgt logisch aus einer Formelmenge X (kurz: X ⊧ G), falls jedes Modell von X auch ein Modell von G ist.

Definition 1.14 (widersprüchlich) Eine Menge X von Formeln ist widersprüchlich (oder auch inkonsistent), falls X kein Modell besitzt. In diesem Fall schreiben wir:

X ⊧ ⊥.

Andernfalls heißt X konsistent.

1.3 Herbrand–Strukturen für E–Theorien

Eine der Grundlagen der Resolution ist die Erkenntnis, daß quantorenfreie Formelmengen, die erfüllbar sind und das Gleichheitszeichen nicht enthalten, schon in einer Herbrand–Struktur erfüllbar sind. Wir werden diesen Satz verschärfen und auf Theorien übertragen, die zusätzlich zu einer Menge identitätsfreier Formeln noch eine Menge E von Axiomen besitzen, die aus reinen Gleichungen bestehen. Es zeigt sich, daß dies in sehr einfacher Weise möglich ist: Es sind nur die Begriffe “erfüllbar” durch “E–erfüllbar” und “Herbrand–Struktur” durch “E–Herbrand–Struktur” zu ersetzen. Bevor wir diesen Satz zeigen können, müssen wir natürlich definieren, was wir unter der E–Erfüllbarkeit oder unter einer E– Herbrand–Struktur verstehen wollen.

Um die Schreibweise abzukürzen, vereinbaren wir für das Folgende, daß A ein festes Alphabet ist, mit dessen Hilfe sämtliche Terme und Formeln, die weiter unten erwähnt werden, gebildet werden. Von allen auftretenden Strukturen setzen wir voraus, daß es sich um Strukturen zu diesem Alphabet A handelt. E steht für eine Menge von Gleichungen, von der wir zunächst nur fordern, daß für zwei beliebige Terme s und t die Frage, ob

E ⊧ t = s

gilt, entscheidbar ist. Wir führen auf der Menge der Terme eine Äquivalenzrelation ∼ ein:

t ∼ s :⇔ E ⊧ t = s.

Die zu dem Term t gehörende Äquivalenzklasse bezeichnen wir mit [t]:

[t] := {s∈T : t ∼ s}.

Gelegentlich ist es zweckmäßig, die Äquivalenzrelation auch auf Primformeln zu übertragen. Sind P und Q zwei Primformeln der Gestalt P = ps_{1} ⋯ s_{m} und Q = qt_{1} ⋯ t_{n}, so definieren wir:

P ∼ Q :⇔ p = q & m = n & s_{1} ∼ t_{1} & ⋯ & s_{m} ∼ t_{m}.

Wir passen nun einige Begriffe der Semantik unseren Erfordernissen an.

Definition 1.15 (E–Struktur) Eine Struktur A ist eine E–Struktur, falls A ein Modell der Theorie E ist:

A ⊧ E.

Ist A eine E–Struktur, in der eine Formel F gilt, so schreiben wir

A ⊧_{E} F,

wenn wir besonders hervorheben wollen, daß A eine E–Struktur ist. Wir sagen dann auch, daß A ein E–Modell von F ist.

Definition 1.16 (E–gültig, E–erfüllbar) Eine Formel F ist E–gültig, wenn F in jeder E–Struktur A gültig ist. In diesem Fall schreiben wir:

⊧_{E} F.

Eine Formel F ist E–erfüllbar, wenn es eine E–Struktur A gibt, in der F gültig ist.

Definition 1.17 (E–Herbrand–Universum) Das E–Herbrand–Universum ist die Menge aller Äquivalenzklassen geschlossener Terme bezüglich der Äquivalenzrelation ∼. Wir bezeichnen das E–Herbrand– Universum mit U:

U := {[t] : t∈T & FV (t) = ∅}.

Wir machen dabei stillschweigend die Voraussetzng, daß unser Alphabet mindestens eine Konstante enthält. Damit wird sichergestellt, daß das Herbrand–Universum nie leer ist.

Definition 1.18 (E–Herbrand–Struktur) H ist eine E–Herbrand–Struktur, falls H eine E–Struktur ist, für die gilt:

• Der Träger von H ist das Herbrand–Universum U.

• Die Funktionszeichen aus L werden trivial interpretiert: Ist f eine n– stelliges Funktionszeichen, so gilt:

f_{H}([t_{1}], ⋯, [t_{n}]) := [ft_{1} ⋯ t_{n}].

Es ist klar, daß die Definition von f_{H} nicht von der Wahl der Repräsentanten der Äquivalenzklassen abhängt, denn es gilt:

[s_{1}] = [t_{1}] & ⋯ & [s_{n}] = [t_{n}] ⇒ [fs_{1} ⋯ s_{n}] = [ft_{1} ⋯ t_{n}].

Bemerkung: Eine E–Herbrand–Struktur ist offenbar bis auf die Interpretation der Prädikatszeichen schon vollständig festgelegt.

Vereinbarung: Im folgenden vereinbaren wir, daß eine Formelmenge, die wir mit X bezeichnen, immer eine Menge \underline{identitätsfreier} Formeln ist. Wir werden also später immer nur Mengen identitätsfreier Formeln auf E–Erfüllbarkeit untersuchen. Die Beschränkung, die wir uns damit auferlegen, sieht schlimmer aus, als sie in Wirklichkeit ist, denn es bleibt uns unbenommen, ein neues zweistelliges Prädikatszeichen, nennen wir es ≐, mit den Axiomen der Gleichheit auszustatten. Haben wir eine Theorie durch eine Menge X von Formeln gegeben, von denen einige das Gleichheitszeichen enthalten, so ersetzen wir zunächst das Gleichheitszeichen überall durch ≐. Außerdem fügen wir zu X folgende Axiome hinzu:

x ≐ x, x ≐ y → y ≐ x, x ≐ y ∧ y ≐ z → x ≐ z,

für jedes n–stellige Funktionszeichen f ein Axiom

x_{1} ≐ y_{1} ∧ ⋯ ∧ x_{n} ≐ y_{n} → fx_{1} ⋯ x_{n} ≐ fy_{1} ⋯ y_{n}

und für jedes n–stellige Prädikatszeichen p ein Axiom

x_{1} ≐ y_{1} ∧ ⋯ ∧ x_{n} ≐ y_{n} ∧ px_{1} ⋯ x_{n} → py_{1} ⋯ y_{n}.

Bezeichnen wir die auf diese Weise entstandene Formelmenge mit X̂, so sind X und X̂ E–erfüllbarkeitsgleich. Denn ist A ein E–Modell von X, so können wir A zu einem E–Modell von X̂ erweitern, indem wir das Prädikat ≐ durch die Identität interpretieren. Ist umgekehrt B ein E–Modell von X̂, so wird daraus ein E–Modell von X, wenn wir Terme s und t, für die t ≐ s gilt, identifizieren und anschließend die Interpretation von ≐ vergessen.

Definition 1.19 (E–Herbrand–Modell) Ist X eine Formelmenge und ist H eine E–Herbrand–Struktur, die Modell von X ist, so sagen wir, daß H ein E–Herbrand–Modell von X ist. In diesem Zusammenhang bezeichnen wir die Menge X als E–Theorie.

Der folgende Satz zeigt, warum wir uns für E–Herbrand–Modelle besonders interessieren:

Satz 1.20 Ist X eine Menge von quantorenfreien Formeln, so ist X genau dann E–erfüllbar, wenn X ein E–Herbrand–Modell besitzt.

Beweis: Ist X E–erfüllbar, so gibt es eine E–Struktur A, die ein Modell von X ist:

A ⊧_{E} X.

Mit Hilfe dieser Struktur konstruieren wir eine E–Herbrand–Struktur H. Zur Festlegung einer E–Herbrand–Struktur ist nur die Interpretation der Prädikatszeichen anzugeben. Ist p ein n–stelliges Prädikatszeichen, so definieren wir

(0)  p_{H}([t_{1}], ⋯, [t_{n}]) := p_{A}(wert_{A}(t_{1}), ⋯, wert_{A}(t_{n})).

An dieser Stelle müssen wir uns davon überzeugen, daß diese Definition unabhängig von der Auswahl der Repräsentanten der Äquivalenzklassen ist. Es muß

s_{1} ∼ t_{1} & ⋯ & s_{n} ∼ t_{n} ⇒
p_{A}(wert_{A}(s_{1}), ⋯, wert_{A}(s_{n})) = p_{A}(wert_{A}(t_{1}), ⋯, wert_{A}(t_{n}))

gelten. Das folgt aber sofort aus der Tatsache, daß A eine E–Struktur ist. Außerdem ist klar, daß durch (0) wirklich eine E–Struktur definiert wird, denn offenbar gilt für geschlossene Terme s_{1}, ⋯, s_{n} und t_{1}, ⋯, t_{n}:

wert_{A}(s_{1}) = wert_{A}(t_{1}) & ⋯ & wert_{A}(s_{n}) = wert_{A}(t_{n}) ⇒

(A ⊧ ps_{1} ⋯ s_{n} ⇔ A ⊧ pt_{1} ⋯ t_{n}).

Ist ω : V → U eine Belegung der Variablen in der Struktur H, so ordnen wir ω eine Substitution σ_{ω} zu, indem wir

(1)  σ_{ω}(x) := t, falls ω(x) = [t] ist,

definieren. (Streng genommen ist σ_{ω} keine Substitution, da der Definitionsbereich von σ_{ω} unendlich ist. Da wir die Endlichkeit des Definitionsbereiches aber im folgenden nicht benötigen, verzichten wir darauf, für σ_{ω} noch einen neuen Terminus, wie z.B. erweiterte Substitution oder ähnliches einzuführen.)

Um einzusehen, daß σ_{ω} wohldefiniert ist, müssen wir uns auf ein vorher festgelegtes Repräsentantensystem für die Äquivalenzklassen des E–Herbranduniversums U beziehen, von dem wir noch fordern, daß der Repräsentant einer Äquivalenzklasse, die einen geschlossenen Term enthält, selbst geschlossen ist. Wir zeigen, daß für alle Terme t und für beliebige Variablenbelegungen ω : V → U

(2)  wert_{H}^{ω}(t) = wert_{H}(tσ_{ω})

gilt. Bevor wir (2) durch Induktion nach dem Aufbau von t zeigen, notieren wir noch eine Trivialität: Ist s ein geschlossener Term, so gilt:

(3)  wert_{H}(s) = [s].

(Genau genommen müßten wir auch (3) noch durch eine Induktion nach dem Aufbau von s zeigen.) Doch nun zum Beweis von (2):

I.A.: t = x∈V. Dann gilt

wert_{H}^{ω}(t) = wert_{H}^{ω}(x) = ω(x).

Gilt ω(x) = [s], wobei s der auch in der Definition (1) von σ_{ω} benutzte Repräsentant der Äquivalenzklasse ω(x) ist, so folgt σ_{ω}(x) = s. Da s ein geschlossener Term ist, folgt weiter

wert_{H}(s) = [s] = ω(x)

und das ist die Behauptung, denn tσ_{ω} = s.

I.S.: t = ft_{1} ⋯ t_{n}. Es gilt:

wert_{H}^{ω}(ft_{1} ⋯ t_{n}) = f_{H}(wert_{H}^{ω}(t_{1}), ⋯, wert_{H}^{ω}(t_{n}))

=^{IV} f_{H}(wert_{H}(t_{1}σ_{ω}), ⋯, wert_{H}(t_{n}σ_{ω}))

= f_{H}([t_{1}σ_{ω}], ⋯, [t_{n}σ_{ω}]) = [ft_{1}σ_{ω} ⋯ t_{n}σ_{ω}]

= [(ft_{1} ⋯ t_{n})σ_{ω}] = wert_{H}((ft_{1} ⋯ t_{n})σ_{ω}).

Wir können ein zu (2) analoges Ergebnis für Primformeln formulieren. Ist P eine beliebige Primformel, so gilt

(4)  W ert_{H}^{ω}(P) = W ert_{H}(P σ_{ω}).

Wir beweisen dies. Hat P die Form pt_{1} ⋯ t_{n}, so gilt

W ert_{H}^{ω}(pt_{1} ⋯ t_{n}) = p_{H}(wert_{H}^{ω}(t_{1}), ⋯, wert_{H}^{ω}(t_{n}))

=^{(2)} p_{H}(wert_{H}(t_{1}σ_{ω}), ⋯, wert_{H}(t_{n}σ_{ω}))

= W ert_{H}(pt_{1}σ_{ω} ⋯ t_{n}σ_{ω}) = W ert_{H}((pt_{1} ⋯ t_{n})σ_{ω}).

Wir stellen nun einen Bezug zwischen den Strukturen A und H her. Für beliebige identitätsfreie Primformeln P und beliebige Belegungen ω gilt:

(5)  W ert_{H}^{ω}(P) = W ⇔ A ⊧ P σ_{ω},

wobei wir voraussetzen, daß der Zusammenhang zwischen ω und σ_{ω} durch (1) gegeben ist. Wir sehen (5) wie folgt ein: Es gilt

W ert_{H}^{ω}(P) = W ⇔^{(4)} W ert_{H}(P σ_{ω}) = W ⇔^{(0)} A ⊧ P σ_{ω}.

Eine triviale Induktion nach dem Formelaufbau zeigt, daß (5) für beliebige identitäts– und quantorenfreie Formeln F richtig bleibt:

(6)  W ert_{H}^{ω}(F) = W ⇔ A ⊧ F σ_{ω},

Damit haben wir alles Material zusammen, um zeigen zu können, daß H ein Modell von X ist: Ist F eine beliebige Formel aus X, so gilt der Allabschluß von F in A. Also gilt für beliebige Substitutionen σ auch A ⊧ F σ. Ist ω : V → U eine beliebige Belegung in H, so gilt insbesondere

A ⊧ F σ_{ω}.

Dann zeigt (6), daß für alle Belegungen ω : V → U

W ert_{H}^{ω}(F) = W

gilt. Das impliziert aber die Gültigkeit des Allabschlußes von F in H. _{□}

Bemerkung: Die Vereinbarung, daß bis auf Formeln aus E nirgends mehr das Gleichheitszeichen auftritt, ging beim Beweis des letzten Satzes entscheidend ein. Wir haben nämlich nur Primformeln der Gestalt pt_{1} ⋯ t_{n} betrachtet, denn hätten wir auch Gleichungen t = s in unsere Überlegungen miteinbeziehen müssen, so wäre der Punkt (5) in dem oberen Beweis falsch geworden.

1.4 Ein widerlegungsvollständiger Kalkül

Bevor wir einen für unser Vorhaben geeigneten Resolutionskalkül entwickeln können, empfiehlt es sich, einen Sequenzenkalkül zu formulieren. Dazu ist es zunächst notwendig, die Syntax zu normieren. Dies ist auch deshalb nützlich, weil dadurch später der Suchraum wesentlich eingeschränkt wird. Wir betrachten daher im folgenden nur Gentzenformeln. Gentzenformeln sind Formeln der Gestalt

(∗)  G = P_{1} ∧ ⋯ ∧ P_{n} → Q_{1} ∨ ⋯ ∨ Q_{m},

wobei die P_{1}, ⋯, P_{n} und die Q_{1}, ⋯, Q_{m} identitätsfreie Primformeln sind. Die Tatsache, daß wir im weiteren Verlauf unserer Überlegungen nur Gentzenformeln untersuchen, bedeutet keine echte Einschränkung. Denn ist F eine beliebige Formel aus der vollen Prädikatenlogik, (also eine Formel, die durchaus noch Quantoren enthält), so kann diese durch Überführung in pränexe Normalform, Skolemisierung und anschließender Bildung der konjunktiven Normalform in eine zu F E–erfüllbarkeitsgleiche Menge X von Gentzenformeln transformiert werden. Es hat sich gezeigt, daß die Sequenzenschreibweise für den Umgang mit Gentzenformeln besonders geeignet ist. Sequenzen wollen wir als Paare von Listen von Primformeln interpretieren. Vielfach werden Sequenzen als Paare von Mengen von Primformeln interpretiert, aber in unseren Anwendungen sind Listen vorzuziehen, da Listen wesentlich einfacher zu implementieren sind als Mengen. Hat G die Gestalt (∗), so schreiben wir in Zukunft

G = Γ : Δ mit Γ = [P_{1}, ⋯, P_{n}] und Δ = [Q_{1}, ⋯, Q_{m}].

Für Listen werden wir die in Prolog üblichen Schreibweisen verwenden: [] steht für die leere Liste und die Liste [P |Γ] hat P als erstes Element und dann folgen die Elemente der Liste Γ.

Um die folgenden Definitionen und Beweise kürzer fassen zu können, vereinbaren wir, daß in Zukunft P und Q immer für Primformeln, Γ, Δ, Λ und Σ für endliche Listen von Primformeln und X für eine Menge von Gentzenformeln bzw. Sequenzen steht.

Um später ein eher technisches Lemma besser formulieren zu können, vereinbaren wir, daß die Schreibweise

Γ = Δ(+P)

für zwei Listen von Primformeln Γ und Δ und eine Primformel P ausdrückt, daß die Liste Γ aus den selben Elementen wie die Liste Δ aufgebaut ist, die dort auch in der selben Reihenfolge wie in Δ auftreten. Zusätzlich darf Γ die Primformel P oder zu P äquivalente Primformeln an beliebig vielen Stellen enthalten. (An dieser Stelle erinnern wir daran, daß zwei Primformeln P und Q äquivalent sind, falls E ⊧ P ↔ Q gilt.)

Um die Schreibweise Γ = Δ(+P) näher zu erläutern, geben wir eine induktive Definition:

Definition 1.21 (Γ = Δ(+P))

I.A.: [] = [](+P).

I.S.: Gilt Γ = Δ(+P), so gilt für beliebige Primformeln Q:

[Q|Γ] = [Q|Δ](+P).

Ist Q ∼ P, so gilt außerdem noch:

[Q|Γ] = Δ(+P).

Sind Γ und Δ zwei Listen, so bezeichnen wir die Verkettung dieser Listen mit Γ, Δ. Mit der Schreibweise

Γ = Δ, P

drücken wir aus, daß die Liste Γ aus der Liste Δ dadurch entsteht, daß an genau einer Stelle noch das Atom P hinzugefügt wird. Auch hier zeigt eine induktive Definition genauer, was wir meinen:

Definition 1.22 (Γ = Δ, P)

I.A.: [P] = [], P.

I.S.: Gilt Γ = Δ, P, so gilt für beliebige Primformeln Q:

[Q|Γ] = [Q|Δ], P und [P |Δ] = Δ, P.

Der Unterschied zu der Definition von Γ = Δ(+P) besteht darin, daß im Falle Γ = Δ, P das Atom P in der Liste Γ genau einmal mehr vorkommt, als in der Liste Δ. Im Falle Γ = Δ(+P) kann P (oder zu P bezüglich ∼ äquivalente Primformeln) in der Liste Γ mehrmals oder auch gar nicht auftreten. Abschließend notieren wir noch, daß die Schreibwiese P ∈ Γ ausdrückt, daß die Primformel P in der Liste Γ auftritt.

Unter einer Herleitung verstehen wir einen endlichen Baum, dessen Blätter mit Axiomen markiert sind. Der Herleitungsbegriff wird dann durch die Axiome und Ableitungsregeln festgelegt. Unser Herleitungskalkül enthält keine logischen Axiome. Wir verwenden drei Ableitungsregeln:

1. Die E–Schnittregel hat die Form

\frac{Γ_{1} : Δ_{1}, P Γ_{2}, Q : Δ_{2}}{Γ_{1}, Γ_{2} : Δ_{1}, Δ_{2}} (S), falls P ∼ Q ist.

Wir bezeichnen die Schnittregel mit (S).

2. Die E–Kontraktionsregeln lauten

\frac{Γ, P, Q : Δ}{Γ, P : Δ}(Kl), falls P ∼ Q ist,

\frac{Γ : Δ, P, Q}{Γ : Δ, P}(Kr), falls P ∼ Q ist.

Die Kontraktionsregeln bezeichnen wir mit (Kl) und (Kr). Falls wir nicht zwischen linker und rechter Kontraktion unterscheiden wollen, sprechen wir von (K).

3. Die Substitutionsregel hat die Gestalt

\frac{Γ : Δ}{Γσ : Δσ} (Subst)

Dabei ist σ eine beliebige Substitution. Die Substitutionsregel erhält den Namen (Subst).

Bemerkenswert bei dem oben vorgestellten Herleitungskalkül ist die Tatsache, daß er versteckte Gleicheitsschlüsse enthält. Diese Gleichheitsschlüsse sind in Bedingungen wie P ∼ Q enthalten. Bei einer Implementierung dieses Kalküls (oder bei aus diesem Kalkül abgeleiteten effizienteren Versionen) ist der Benutzer also von der Last befreit, sich um die Gleichungen aus E zu kümmern. Diese werden von dem vorgestellten Kalkül automatisch berücksichtigt. Das kann natürlich nur funktionieren, falls P ∼ Q für beliebige Primformeln entscheidbar ist.

Wir nennen ein Regelsystem R E–widerlegungsvollständig, falls für jede Menge X von Sequenzen

X ⊧_{E} ⊥ ⇒ X ⊢_{R} []:[]

gilt. Dabei steht die Schreibweise X ⊧_{E} ⊥ für X ∪ {E} ⊧ ⊥. Für die Sequenz []:[] werden wir in Zukunft die Schreibweise □ verwenden.

Wir betrachten zunächst nur die E–Schnittregel zusammen mit den beiden E–Kontraktionsregeln. Ist eine Sequenz Γ : Δ aus einer Menge X von Sequenzen unter ausschließlicher Benutzung dieser Regeln abgeleitet worden, so schreiben wir:

X ⊢_{SK} Γ : Δ.

Lemma 1.23

Vor.: X ∪ {[]:[P]} ⊢_{SK} Γ : Δ & Γ : Δ ≠ []:[P].

Beh.: X ⊢_{SK} Λ : Δ für ein Λ mit Λ = Γ(+P).

Beweis: Wir führen den Beweis durch Induktion nach dem Aufbau der Herleitung der Sequenz Γ : Δ.

I.A.: Γ : Δ ∈ X ∪ {[] : [P]}. Da Γ : Δ ≠ [] : [P] ist, folgt Γ : Δ ∈ X und das heißt X ⊢_{SK} Γ : Δ.

I.S.: Wir betrachten zunächst den Fall, daß der letzte Schluß eine E–Kontrak-

tion der Gestalt

\frac{Γ, Q_{1}, Q_{2} : Δ}{Γ, Q_{1} : Δ}

ist. Nach IV gibt es ein Λ mit Λ = Γ(+P), so daß

X ⊢_{SK} Λ, Q_{1}, Q_{2} : Δ

gilt. Mit einer Kontraktion folgt daraus

X ⊢_{SK} Λ, Q_{1} : Δ

und wegen Λ, Q_{1} = Γ, Q_{1}(+P) ist das die Behauptung.

Ist der letzte Schluß eine E–Kontraktion der rechten Seite der Sequenz gewesen, so zeigen zum ersten Fall analoge (aber einfachere) Überlegungen, daß die Behauptung auch dann stimmt.

Abschließend betrachten wir den Fall, daß der letzte Schluß ein E–Schnitt war. Je nachdem, ob die Sequenz [] : [P] am letzten Schluß beteiligt war, müssen verschiedene Überlegungen durchgeführt werden.

1. Fall: Der letzte Schluß hat die Gestalt

\frac{Γ_{1} : Δ_{1}, Q_{1} Γ_{2}, Q_{2} : Δ_{2}}{Γ_{1}, Γ_{2} : Δ_{1}, Δ_{2}} mit Q_{1} ∼ Q_{2}

und es ist Γ_{1} : Δ_{1}, Q_{1} ≠ []:[P]. Nach IV gilt

X ⊢_{SK} Λ_{1} : Δ_{1}, Q_{1} & X ⊢_{SK} Λ_{2}, Q_{2} : Δ_{2},

wobei für i∈{1, 2} Λ_{i} = Γ_{i}(+P) gilt. Ein Schnitt liefert

X ⊢_{SK} Λ : Δ_{1}, Δ_{2}

mit Λ = Λ_{1}, Λ_{2}. Wegen Γ = Γ_{1}, Γ_{2} und Δ = Δ_{1}, Δ_{2} ist das die Behauptung, denn aus Λ_{i} = Γ_{i}(+P) folgt Λ = Γ(+P).

2. Fall Der letzte Schluß ist:

\frac{[]:[P] Γ_{2}, Q : Δ_{2}}{Γ_{2} : Δ_{2}} mit P ∼ Q

Dann ist Γ = Γ_{2} und Δ = Δ_{2}. Definieren wir Λ = Γ, Q, so ist Λ = Γ(+P), denn es ist Q ∼ P und offenbar gilt

X ⊢_{SK} Λ : Δ. _{□}

Lemma 1.24

Vor.: X ∪ {[P]:[]} ⊢_{SK} Γ : Δ & Γ : Δ ≠ [P]:[].

Beh.: X ⊢_{SK} Γ : Λ für ein Λ mit Λ = Δ(+P).

Beweis: Der Beweis verläuft analog zum Beweis von Lemma (1.23). _{□}

Die letzten beiden Lemmata werden für das folgende Konsistenzlemma benötigt:

Lemma 1.25 (Konsistenzlemma)

Vor.: X ∪ {[]:[P]} ⊢_{SK} □ & X ∪ {[P]:[]} ⊢_{SK} □.

Beh.: X ⊢_{SK} □.

Beweis: Aus den Voraussetzungen folgt mit Lemma (1.23) bzw. Lemma (1.24)

X ⊢_{SK} Γ : [] und X ⊢_{SK} [] : Δ

und es gilt:

(∗)  Γ = [](+P) und Δ = [](+P).

Aus (∗) folgt, daß es natürliche Zahlen n und m gibt, so daß Γ = [m ∗ P] und Δ = [n ∗ P] ist. Dabei steht die Schreibweise [n ∗ P] für die Liste

[\underbrace{P, ⋯, P}_{n}].

(Streng genommen ist das nur richtig, wenn wir äquivalente Primformeln identifizieren, was aber gefahrlos möglich ist.) Falls m = 0 oder n = 0 gilt, sind wir fertig. Sonst liefert die E–Kontraktionsregel

X ⊢_{SK} []:[P] und X ⊢_{SK} [P]:[].

Die Behauptung folgt nun mit einem Schnitt. _{□}

Das Konsistenzlemma versetzt uns in die Lage, im aussagenlogischen Fall einen Vollständigkeitssatz formulieren zu können.

Satz 1.26 Ist X eine Menge von geschlossenen Gentzenformeln, so gilt:

X ⊧_{E} ⊥ ⇒ X ⊢_{SK} □.

Beweis: Wir führen den Beweis durch Kontraposition und machen die Annahme:

(1)  X ⊬_{SK} □.

Mit Hilfe dieser Annahme konstruieren wir ein E–Modell H von X. Zunächst sei (P_{n})_{n} eine Aufzählung aller geschlossenen identitätsfreien Primformeln der zugrundeliegenden Sprache. Wir konstruieren induktiv eine Folge (X_{n})_{n} von Mengen von Sequenzen:

I.A.: n = 0. Wir setzen X_{0} := X.

I.S.: n → n + 1. Wir definieren

X_{n+1} := \{ \begin{matrix}X_{n} ∪ \{[]:[P_{n}]\} & falls & X_{n} ∪ \{[]:[P_{n}]\} ⊬_{SK} □; \\ X_{n} ∪ \{[P_{n}]:[]\} & sonst. \end{matrix}

Wir zeigen durch Induktion nach n, daß für alle n ∈ N X_{n} ⊬_{SK} □ gilt. Für n = 0 ist das wegen (1) klar. Für den Induktionsschritt überlegen wir: Ist X_{n+1} = X_{n} ∪ {[P_{n}]:[]}, so gilt X_{n} ∪ {[]:[P_{n}]} ⊢_{SK} □. Würde X_{n+1} ⊢_{SK} □, also X_{n} ∪ {[P_{n}]:[]} ⊢_{SK} □ gelten, so zeigt das Konsistenzlemma (1.25), daß dann im Widerspruch zur IV auch X_{n} ⊢_{SK} □ gelten müßte.

Wir definieren nun X̂ := ⋃_{n} X_{n}. Würde X̂ ⊢_{SK} □ gelten, so würde die Herleitung von □ mit endlich vielen Sequenzen {G_{1}, ⋯, G_{k}} aus X̂ auskommen. Jede Sequenz G_{i} würde in einer Menge X_{n_{i}} liegen. Wir definieren n_{0} := max{n_{1}, ⋯, n_{k}}. Da die Folge (X_{n})_{n} monoton aufsteigend ist, gilt

{G_{1}, ⋯, G_{k}} ⊆ X_{n_{0}}.

Das würde aber X_{n_{0}} ⊢_{SK} □ erzwingen und somit gilt:

(2)  X̂ ⊬_{SK} □.

Damit sind wir in der Lage, eine E–Herbrand–Struktur H zu konstruieren. Sind [t_{1}], ⋯, [t_{n}] Äquivalenzklassen aus dem E–Herbrand–Universum und ist p ein n–stelliges Prädikatszeichen, so definieren wir

p_{H}([t_{1}], ⋯, [t_{n}]) := \{ \begin{matrix}W & falls gilt ([]:[pt_{1} ⋯ t_{n}]) ∈ X̂; \\ F & sonst. \end{matrix}

An dieser Stelle müssen wir uns klarmachen, daß diese Definition unabhängig von der Wahl der Repräsentanten der beteiligten Äquivalenzklassen ist. Wir führen den Nachweis der Wohldefiniertheit von p_{H} indirekt und nehmen an, daß es geschlossene Terme s_{1}, ⋯, s_{n} und t_{1}, ⋯, t_{n} gibt, so daß

[s_{1}] = [t_{1}] & ⋯ & [s_{n}] = [t_{n}] und
([]:[ps_{1} ⋯ s_{n}]) ∈ X̂ aber ([]:[pt_{1} ⋯ t_{n}]) ∉ X̂

gilt. Aus ([]:[pt_{1} ⋯ t_{n}]) ∉ X̂ folgt nach Konstruktion von X̂

([pt_{1} ⋯ t_{n}]:[]) ∈ X̂.

Also ist {[]:[ps_{1} ⋯ s_{n}], [pt_{1} ⋯ t_{n}]:[]} eine Teilmenge von X. Da

{[]:[ps_{1} ⋯ s_{n}], [pt_{1} ⋯ t_{n}]:[]} ⊢_{SK} □

gilt, wäre das ein Widerspruch zu (2).

Wir behaupten, daß die oben definierte E–Herbrand–Struktur ein Modell von X̂ ist. Wir argumentieren indirekt und nehmen an, daß eine Sequenz Γ : Δ in X̂ existiert, die in H nicht gültig ist. Das heißt aber:

\begin{aligned}& ∀P ∈Γ(H ⊧_{E} P) & & & ∀Q∈Δ(H |̸=_{E} Q) \\ ⇒ & ∀P ∈Γ([]:[P] ∈ X̂) & & & ∀Q∈Δ([] : [Q] ∉ X̂) \end{aligned}

Die Konstruktion von X̂ war gerade so angelegt, daß für alle geschlossenen identitätsfreien Primformeln R aus der zugrundeliegenden Sprache L

[]:[R] ∈ X̂ oder [R]:[] ∈ X̂

gilt. Damit folgt:

(3)  ∀P ∈Γ([]:[P] ∈ X̂) & ∀Q∈Δ([Q]:[] ∈ X̂).

Andererseits ist klar, daß

{Γ : Δ} ∪ {[]:[P] | P ∈Γ} ∪ {[Q]:[] | Q∈Δ} ⊢_{SK} □

gilt. Aus (3) folgt, daß {Γ : Δ} ∪ {[] : [P] | P ∈ Γ} ∪ {[Q] : [] | Q ∈ Δ} eine Teilmenge von X̂ ist, und das ist ein Widerspruch zu (2). Dieser Widerspruch zeigt, daß H ein Modell von X̂ ist. Da X ⊆ X̂ ist, ist H auch ein Modell von X, und daraus folgt

X |̸=_{E} ⊥. _{□}

Um den letzten Satz auf beliebige, nicht notwendig geschlossene, Gentzenformeln übertragen zu können, bedarf es noch einiger Vorbereitung. Das nächste Lemma dient dazu.

Lemma 1.27 Ist X eine Menge von Gentzenformeln, so gilt:

X ⊧_{E} ⊥ ⇒ grund(X) ⊧_{E} ⊥.

Beweis: Wir führen den Beweis durch Kontraposition und nehmen an, daß grund(X) ein E–Modell hat. Nach Lemma (1.20) hat grund(X) dann auch ein E–Herbrand–Modell H. Da der Träger von H nur aus Äquivalenzklassen geschlossener Terme besteht, läßt sich jede Variablenbelegung ω : V → U als geschlossene Substitution σ_{ω} auffassen:

ω(x) = [t] → σ_{ω}(x) = t.

(Dabei ist es gleichgültig, welchen Vertreter der Äquivalenzklasse wir auswählen, wir müssen uns nur für einen entscheiden.) Durch Induktion nach dem Aufbau der Terme zeigen wir zunächst

wert_{H}^{ω}(t) = wert_{H}(tσ_{ω})

für alle Terme t und anschließend

W ert_{H}^{ω}(A) = W ert_{H}(Aσ_{ω})

für alle Formeln A. Wir führen hier den Beweis nicht näher aus, da wir ihn de facto beim Beweis von Satz (1.20) schon gegeben haben.

Ist G∈X, so ist Gσ_{ω} ∈grund(X) und damit gilt für jede Belegung ω:

W ert_{H}^{ω}(G) = W ert_{H}(Gσ_{ω}) = W.

Dies zeigt, daß H auch ein E–Modell von X ist und daraus folgt X |̸=_{E} ⊥. _{□} Lemma 1.28 Ist R eine Menge von Ableitungsregeln, so gilt:

grund(X) ⊢_{R} Γ : Δ ⇒ X ⊢_{R∪{Subst}} Γ : Δ

Beweis: Wir führen den Beweis durch Herleitungsinduktion.

I.A.: Γ : Δ ∈ grund(X). In diesem Fall gibt es eine Sequenz Λ : Σ in X und eine Substitution μ, so daß Γ : Δ = (Λ : Σ)μ ist. Eine Anwendung von (Subst) auf Λ : Σ liefert die Behauptung.

I.S.: R ist eine Regel aus R und der letzte Schluß hat die Gestalt:

\frac{Γ_{1} : Δ_{1}  ⋯  Γ_{n} : Δ_{n}}{Γ : Δ} (R)

Nach Voraussetzung gilt also

grund(X) ⊢_{R} Γ_{1} : Δ_{1} & ⋯ & grund(X) ⊢_{R} Γ_{n} : Δ_{n}.

Die IV zeigt

X ⊢_{R∪{Subst}} Γ_{1} : Δ_{1} & ⋯ & X ⊢_{R∪{Subst}} Γ_{n} : Δ_{n}.

Durch einen Schluß mit der Regel R folgt daraus die Behauptung. _{□}

Satz 1.29 (Lifting–Theorem) Ist R ein System von Ableitungsregeln, das für geschlossene Gentzenformeln E–widerlegungsvollständig ist, so ist R∪{Subst} E– widerlegungsvollständig für Gentzenformeln.

Beweis: Es sei X eine E–widersprüchliche Menge von Gentzenformeln. Dann gilt:

X ⊧_{E} ⊥  nach Annahme
⇒ grund(X) ⊧_{E} ⊥ nach Lemma (1.27)
⇒ grund(X) ⊢_{R} □ nach Voraussetzung
⇒ X ⊢_{R∪{Subst}} □ nach Lemma (1.28). _{□}

Unser eigentliches Hauptergebnis erhalten wir nun als Korollar zu Satz (1.26) und Satz (1.29):

Theorem 1.30 {S, K, Subst} ist E–widerlegungsvollständig für Gentzenformeln.

Unifikationstheorie

In diesem Kapitel stellen wir übersichtsartig einige Begriffe und Ergebnisse der allgemeinen Unifikationstheorie zusammen. Bei unseren weiteren Betrachtungen ist E immer eine feste Menge von Gleichungen.

Definition 2.1 (E–Gleichheit, E–Subsumtion) Die Substitutionen σ und τ heißen E–gleich (geschrieben σ =_{E} τ) genau dann, wenn für alle Variablen x∈V

⊧_{E} σ(x) = τ(x)

gilt. σ E–subsumiert τ (geschrieben σ ≤_{E} τ) genau dann, wenn es eine Substitution ϱ mit σϱ =_{E} τ gibt.

Definition 2.2 (E–Unifikation) Eine Substitution σ ist ein E–Unifikator der Terme t und s genau dann, wenn

⊧_{E} sσ = tσ

gilt. In diesem Fall heißen s und t E–unifizierbar. Entsprechend heißt σ E– Unifikator für eine Termmenge M = {t_{1}, ⋯, t_{n}}, falls für alle i, j ∈{1, ⋯ n}

⊧_{E} t_{i}σ = t_{j}σ

gilt. In diesem Fall nennen wir M E–unifizierbar. Die Menge aller E–Unifikatoren von M bezeichnen wir mit U_{E}(M).

Im Falle der Unifikation besteht zwischen Termen und Primformeln kein Unterschied. Wir werden daher im folgenden zwei Primformeln P und Q E–unifizierbar nennen, falls es eine Substitution σ gibt, so daß P σ ∼ Qσ gilt.

Definition 2.3 (Vollständige Mengen von minimalen E–Unifikatoren) Eine Menge U von Substitutionen ist eine vollständige Menge von minimalen E–Unifikatoren für eine Menge M von Termen, falls gilt:

1. U ⊆ U_{E}(M). (Korrektheit)

2. ∀τ ∈U_{E}(M) ∃σ ∈U(σ ≤_{E} τ). (Vollständigkeit)

3. ∀σ, τ ∈U(σ ≤_{E} τ ⇒ τ = σ). (Minimalität)

In diesem Fall schreiben wir U = μcU_{E}(M).

Bemerkung: Die Schreibweise U = μcU_{E}(M) ist mit Vorsicht zu genießen, denn μcU_{E}(M) ist nicht eindeutig. Es kann also durchaus zwei verschiedene Mengen U_{1} und U_{2} geben, so daß

U_{1} = μcU_{E}(M) und U_{2} = μcU_{E}(M)

gilt.

Definition 2.4 (Unifikationstyp ω) Wir sagen, daß die Theorie E den Unifikationstyp ω hat, falls für jede E–unifizierbare Menge M eine \underline{endliche} Menge U mit U = μcU_{E}(M) existiert.

Ist M = {s, t} eine E–unifizierbare Menge und ist U = μcU_{E}(M), so schreiben wir

σ = mgu_{E}(s, t)

um auszudrücken, daß σ∈U ist. Auch diese Schreibweise stellt eigentlich einen Mißbrauch des Gleichheitszeichens dar, denn aus σ_{1} = mgu_{E}(s, t) und σ_{2} = mgu_{E}(s, t) folgt natürlich nicht σ_{1} = σ_{2}. Wir haben diese Schreibweise nur gewählt, um in der Notation nicht zwischen E = ∅ und E ≠ ∅ unterscheiden zu müssen. Die Schreibweise soll insbesondere \underline{nicht} implizieren, daß es eine Funktion mgu_{E} gibt, die zu jeder E–unifizierbaren Menge M ein Element aus μcU_{E}(M) auswählt.

In den folgenden Abschnitten wollen wir voraussetzen, daß E eine Theorie vom Unifikationstyp ω ist, für die sich für jede E–unifizierbare Menge M eine Menge μcU_{E}(M) von vollständigen Unifikatoren effektiv berechnen läßt. Mit der Schreibweise U = μcU_{E}(M) meinen wir im folgenden immer, daß U diejenige vollständige Menge von minimalen E–Unifikatoren ist, die uns durch einen festen gewählten Algorithmus geliefert wird. Ein solcher Algorithmus existiert beispielsweise für E = ∅ und für die Theorien

C(∗), I(∗), AC(∗) und ACI(∗).

(Dabei steht C für die Kommutativität von ∗, A für die Assoziativität und I für Idempotenz. AC(∗) besteht also aus den Axiomen:

x ∗ y = y ∗ x,
(x ∗ y) ∗ z = x ∗ (y ∗ z).

Nähere Informationen zur Unifikationstheorie finden sich z.B. in dem Übersichtsartikel [Siek89] von Siekmann.)

E–Resolution

In diesem Kapitel zeigen wir zunächst, daß die E–Resolution zusammen mit der E–Faktorisierungsregel E–widerlegungsvollständig ist. Anschließend überlegen wir uns, inwieweit sich unsere Ergebnisse verschärfen lassen, wenn wir es ausschließlich mit Hornformeln zu tun haben. Es zeigt sich, daß wir im Falle der Hornformeln auf die Faktorisierungsregel verzichten können.

Nachdem wir im ersten Abschnitt die E—Widerlegungsvollständigkeit von E–Resolution und E–Faktorisierungsregel nachweisen, zeigen wir im zwieten Abschnitt , daß eine für Hornformeln naheliegende Einschränkung der Schnittregel, die als Prolog–Regel bekannt ist, für Hornformeln widerlegungsvollständig ist. Die dabei benutzten Methoden sind im wesentlichen die gleichen wie im ersten Abschnitt.

Im dritten Abschnitt untersuchen wir dann eine Einschränkung der E–Prolog– Regel, die der in Prolog implementierten Ableitungsregel näher kommt. Wir zeigen, daß diese Regel für geschlossenen Hornformeln widerlegungsvollständig ist. Der Beweis läuft darauf hinaus, daß wir zeigen, wie Beweise die mit der uneingeschränkten Prolog–Regel geführt worden sind, in Beweise, die nur die eingeschränkte Prolog–Regel benutzen, transformiert werden können.

Im letzten Abschnitt zeigen wir, wie wir den Unifikationsalgorithmus mit der eingeschränkten Prolog–Regel verheiraten können, um daraus einen Resolutionskalkül zu erhalten, der dem Resolutionskalkül des ersten Abschnittes ähnelt. Dieser Kalkül wird mit einer einzigen Regel auskommen und entspricht genau dem, was in Prolog implementiert ist.

3.1 E–Resolution

Wir beginnen mit einer Definition:

Definition 3.1 (E–Resolution) Der Schluß

\frac{Γ_{1} :Δ_{1}, P Γ_{2}, Q:Δ_{2}}{(Γ_{1}, Γ_{2} :Δ_{1}, Δ_{2})μ} (Res)

ist eine Anwendung der E–Resolutionsregel (Res), falls gilt:

1. μ = mgu_{E}(P, Q).

2. FV (Γ_{1} :Δ_{1}, P) ∩ FV (Γ_{2}, Q:Δ_{2}) = ∅.

Die zweite Bedingung in der Definition der E–Resolution nennen wir die Variablenbedingung. Die Variablenbedingung läßt sich durch geeignete Umbenennungen immer sicherstellen. Damit das glatt geht, müssen wir unseren Ableitungsbegriff etwas verallgemeinern, denn es ist nun notwendig, in einer Herleitung

X ⊢_{R} Γ:Δ

als Axiome nicht nur Sequenzen aus X, sondern auch Umbenennungen von Sequenzen aus X zuzulassen. In unseren weiteren Überlegungen gehen wir immer stillschweigend davon aus, daß die Variablenbedingung sichergestellt ist. Dies ist stets möglich, nachdem wir unsere Anforderungen an die Sequenzen, die wir als Axiome zulassen wollen, wie oben dargelegt abgeschwächt haben.

Definition 3.2 (E–Faktorisierung) Die Schlüsse

\frac{Γ, P, Q:Δ}{(Γ, P:Δ)μ}(Fak) und \frac{Γ:Δ, P, Q}{(Γ:Δ, P )μ}(Fak)

sind Anwendungen der E–Faktorisierungsregel (Fak), falls gilt:

μ = mgu_{E}(P, Q).

Der nächste Satz zeigt, daß Herleitungen, die nur mit der E–Schnittregel, den E–Kontraktionsregeln und der Substitutionsregel arbeiten, in Herleitungen transformiert werden können, die mit E–Resolution und E–Faktorisierung auskommen.

Satz 3.3 (Transformationssatz)

Vor.: X ⊢_{{S,K,Subst}} Γ:Δ.

Beh.: ∃ Γ̂, Δ̂ ∃σ(X ⊢_{{Res,Fak}} Γ̂:Δ̂ & Γ = Γ̂σ & Δ = Δ̂σ).

Beweis: Wir führen den Beweis durch Induktion nach der Länge der Herleitung.

1. Fall: Γ : Δ ∈ X. In diesem Fall setzen wir Γ̂ := Γ, Δ̂ := Δ und σ := id. Damit folgt die Behauptung sofort.

2. Fall: Wir betrachten nun den Fall, daß der letzte Schluß ein Schnitt ist:

\frac{Γ_{1} :Δ_{1}, P Γ_{2}, Q:Δ_{2}}{Γ_{1}, Γ_{2} :Δ_{1}, Δ_{2}} (S) mit P ∼ Q.

Nach IV gibt es Γ̂_{1}, Δ̂_{1}, Γ̂_{2}, Δ̂_{2}, P̂ und Q̂, sowie zwei Substitutionen τ_{1}, τ_{2}, so daß

X ⊢_{{Res,Fak}} Γ̂_{1} :Δ̂_{1}, P̂ & X ⊢_{{Res,Fak}} Γ̂_{2}, Q̂:Δ̂_{2}

und Γ_{1} :Δ_{1}, P = (Γ̂_{1} :Δ̂_{1}, P̂)τ_{1} sowie Γ_{2}, Q:Δ_{2} = (Γ̂_{2}, Q̂:Δ̂_{2})τ_{2} gilt. Nach geeigneter Umbennung beispielsweise der Variablen der Herleitung

X ⊢_{{Res,Fak}} Γ̂_{1} :Δ̂_{1}, P̂

können wir erreichen, daß

FV (Γ̂_{1} :Δ̂_{1}, P̂) ∩ FV (Γ̂_{2}, Q̂:Δ̂_{2}) = ∅

gilt. Dann können wir o.B.d.A. annehmen, daß τ_{1} und τ_{2} disjunkte Definitionsbereiche haben. Wir definieren eine neue Substitution τ durch:

τ := \{ \begin{matrix}τ_{1}(x) & falls x∈dom(τ_{1}); \\ τ_{2}(x) & sonst. \end{matrix}

Mit dieser Definition ist klar, daß

Γ_{1} :Δ_{1}, P = (Γ̂_{1} :Δ̂_{1}, P̂)τ und Γ_{2}, Q:Δ_{2} = (Γ̂_{2}, Q̂:Δ̂_{2})τ

gilt. Da P̂τ = P ∼ Q = Q̂τ ist, sind P̂ und Q̂ E–unifizierbar. Also existiert eine Substitution μ mit μ = mgu_{E}(P̂, Q̂) und eine Substitution σ, so daß

P̂μ ∼ Q̂μ und τ = μσ

gilt. Daher ist

\frac{Γ̂_{1} :Δ̂_{1}, P̂  Γ̂_{2}, Q̂:Δ̂_{2}}{(Γ̂_{1}, Γ̂_{2} :Δ̂_{1}, Δ̂_{2})μ} (Res)

eine korrekte Anwendung der E–Resolutionsregel. Definieren wir Γ̂ := (Γ̂_{1}, Γ̂_{2})μ und Δ̂ := (Δ̂_{1}, Δ̂_{2})μ, so gilt

X ⊢_{{Res,Fak}} Γ̂:Δ̂

und es ist Γ:Δ = (Γ̂:Δ̂)σ.

3. Fall: Der letzte Schluß ist eine Kontraktion der Form

\frac{Γ_{1}, P, Q:Δ_{1}}{Γ_{1}, P:Δ_{1}} (Kl) mit P ∼ Q.

Nach IV gibt es Γ̂_{1}, Δ̂_{1}, P̂ und Q̂, sowie eine Substitution τ, so daß

X ⊢_{{Res,Fak}} Γ̂_{1}, P̂, Q̂:Δ̂_{1}

und Γ_{1}, P, Q : Δ_{1} = (Γ̂_{1}, P̂, Q̂ : Δ̂_{1})τ gilt. Da P̂τ = P ∼ Q = Q̂τ ist, sind P̂ und Q̂ E–unifizierbar. Also existiert eine Substitution μ mit μ = mgu_{E}(P̂, Q̂) und eine Substitution σ, so daß

P̂μ ∼ Q̂μ und τ = μσ

ist. Daher ist

\frac{Γ̂_{1}, P̂, Q̂:Δ̂_{1}}{(Γ̂_{1}, P̂:Δ̂_{1})μ}(Fak)

eine korrekte Anwendung der E–Faktorisierungsregel. Definieren wir Γ̂ := (Γ̂_{1}, P̂)μ und Δ̂ := Δ̂_{1}μ, so gilt

X ⊢_{{Res,Fak}} Γ̂:Δ̂,

und es ist Γ = Γ_{1}, P = (Γ̂_{1}, P̂)τ = Γ̂σ und Δ = Δ_{1} = Δ̂_{1}τ = Δ̂σ.

4. Fall: Der letzte Schluß ist eine Kontraktion der Form

\frac{Γ_{1} :Δ_{1}, P, Q}{Γ_{1}, P:Δ_{1}}(Kr) mit P ∼ Q.

Dieser Fall wird analog zum dritten Fall behandelt.

5. Fall: Der letzte Schluß ist eine Anwendung der Substitutionsregel:

\frac{Γ_{1} :Δ_{1}}{Γ_{1}τ:Δ_{1}τ} (Subst).

Nach IV gibt es eine Sequenz Γ̂:Δ̂ und eine Substitution ϱ mit

X ⊢_{{Res,Fak}} Γ̂:Δ̂

und es ist Γ_{1} = Γ̂ϱ und Δ_{1} = Δ̂ϱ. Definieren wir σ := ϱτ, so gilt Γ = Γ_{1}τ = Γ̂ϱτ = Γ̂σ und ebenso Δ = Δ̂σ. _{□}

Da wir in Theorem (1.30) gezeigt hatten, daß das System {S, K, Subst} ein E–widerlegungsvollständiges System von Ableitungsregeln für Gentzenformeln ist, erhalten wir nun als Korollar zum Transformationssatz unser eigentliches Hauptergebnis:

Theorem 3.4 {Res, Fak} ist E–widerlegungsvollständig für Gentzenformeln.

Bemerkung: Das letzte Theorem wurde für den Fall E = ∅ zuerst von J.A. Robinson in [Rob65] gezeigt. Unsere Darstellung orientiert sich eher an [HK89].

3.2 Die E–Prolog–Regel

Hornformeln sind Sequenzen der Form

Γ:[P] und Γ:[].

Dabei werden wir Sequenzen der Form Γ:[P] als positive Hornformeln bezeichnen. Ist Γ = [], so sprechen wir auch von Fakten. Die Sequenzen der Gestalt Γ : [] werden oft als negative Hornformeln oder (in der Sprache der Prolog–Gemeinde) als “Goals” bzw. Ziele bezeichnet. Wir formulieren nun eine Spezialisierung der Schnittregel, die wir als E–Prolog–Regel oder kurz (PR) bezeichnen:

\frac{Γ:[P] Δ, Q : []}{Γ, Δ:[]}(PR) mit P ∼ Q.

Es wird sich zeigen, daß diese Regel für geschlossene Hornformeln E–widerlegungsvollständig ist. Bevor wir das allerdings beweisen können, bedarf es noch einiger Vorbereitung. Zur Abkürzung der Schreibweise vereinbaren wir, daß X im Rest dieses Paragraphen für eine Menge von Hornformeln steht. Läßt sich eine Sequenz Γ : Δ mit der Prolog–Regel aus einer Menge X von Hornformeln ableiten, so schreiben wir

X ⊢_{PR} Γ:Δ.

Es ist klar, daß die Liste Δ dann höchstens einelementig ist. Falls die Herleitung nicht trivial ist, falls also nicht Γ:Δ ∈ X ist, so muß schon Δ = [] gelten.

Lemma 3.5

Vor.: X ∪ {[]:[P]} ⊢_{PR} Γ : [].

Beh.: Es gibt ein Λ mit X ⊢_{PR} Λ:[] und es ist Λ = Γ(+P).

Beweis: Wir führen den Beweis durch Induktion nach dem Aufbau der Herleitung der Sequenz Γ:[].

I.A.: Γ:[] ∈ X ∪ {[]:[P]}.

Da Γ:[] ≠ []:[P] ist, folgt Γ:[] ∈ X und das heißt X ⊢_{PR} Γ:[].

I.S.: Der letzte Schluß hat die Gestalt

\frac{Γ_{1} :[Q_{1}] Γ_{2}, Q_{2} :[]}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2}.

Da wir mit der Prolog–Regel nur negative Hornformeln ableiten können, muß

Γ_{1} : [Q_{1}] ∈ X ∪ {[]:[P]}

sein. Wir führen eine Fallunterscheidung durch:

1. Fall: Γ_{1} : [Q_{1}] ≠ [] : [P]. Dann folgt Γ_{1} : [Q_{1}] ∈ X. Nach IV gibt es ein Λ_{2} mit Λ_{2} = Γ_{2}(+P), so daß

X ⊢_{PR} Λ_{2}, Q_{2} :[]

gilt. Die Prolog–Regel liefert nun:

\frac{Γ_{1} :[Q_{1}] Λ_{2}, Q_{2} :[]}{Γ_{1}, Λ_{2} :[]}(PR).

Definieren wir Λ := Γ_{1}, Λ_{2}, so folgt Λ = Γ(+P) und

X ⊢_{PR} Λ:[].

2. Fall: Γ_{1} :[Q_{1}] = []:[P]. Also ist Γ_{1} = [], Q_{1} = P und Γ = Γ_{2}. Nach IV gibt es ein Λ_{2} mit Λ_{2} = Γ_{2}(+P) und

X ⊢_{PR} Λ_{2}, Q_{2} :[].

Definieren wir Λ = Λ_{2}, Q_{2}, so ist Λ = Γ(+P) und

X ⊢_{PR} Λ:[]. _{□}

Falls wir in dem letzten Lemma die Voraussetzung []:[P] in [P]:[] abändern, so läßt sich nicht ohne weiteres sehen, wie die Behauptung modifiziert werden muß, um die Richtigkeit der Aussage zu erhalten. Um eine geeignete Variante finden zu können, müssen wir zunächst einmal etwas mehr über die Struktur von Herleitungen erfahren, die nur mit der Prolog–Regel arbeiten. Ist X eine Menge von Hornformeln, so bezeichnen wir in Zukunft mit X^{+} alle in X auftretenden positiven Hornformeln:

X^{+} := {Γ:[P] | Γ:[P] ∈ X}.

Entsprechend steht X^{−} für die Menge der negativen Hornformeln aus X:

X^{−} := {Γ:[] | Γ:[] ∈ X}.

Es sind zwei Beobachtungen, die für das spätere Vorgehen von entscheidender Bedeutung sind:

Zum einen folgt aus

X ⊢_{PR} Γ:Δ,

daß entweder Δ = [] oder Γ:Δ ∈ X ist, denn mit der Prolog–Regel können nur negative Hornformeln abgeleitet werden. (Diese Beobachtung haben wir schon beim Beweis des letzten Lemmas verwendet.)

Zum anderen kann in einer Herleitung X ⊢_{PR} Γ : [] nur genau eine Formel aus X^{−} verwendet worden sein. Diese Beobachtung ist Gegenstand des nächsten Lemmas:

Lemma 3.6 Vor.: X ⊢_{PR} Γ : []. Beh.: Es gibt ein G ∈ X^{−} mit X^{+} ∪ {G} ⊢_{PR} Γ:[]. Beweis durch Herleitungsinduktion: I.A.: In diesem Fall ist Γ:[] ∈ X und wir können G := Γ:[] setzen. I.S.: Der letzte Schluß hat die Gestalt

\frac{Γ_{1} :[Q_{1}] Γ_{2}, Q_{2} :[]}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2}.

Nach der oben gemachten Bemerkung ist Γ_{1} :[Q_{1}] ∈ X^{+} und nach IV gibt es ein G ∈ X^{−} mit

X^{+} ∪ {G} ⊢_{PR} Γ_{2}, Q_{2} :[].

Durch eine Anwendung der Prolog–Regel sehen wir sofort:

X^{+} ∪ {G} ⊢_{PR} Γ:[]. _{□}

Das nächste Lemma zeigt, wie sich Herleitungen bei Abschwächung der negativen Prämisse ändern. Lemma 3.7 Vor.: X ∪ {Γ:[]} ⊢_{PR} Λ : []. Beh.: X ∪ {Γ, Δ:[]} ⊢_{PR} Λ, Δ:[] oder X ∪ {Γ, Δ:[]} ⊢_{PR} Λ : []. Beweis: Falls die Sequenz Γ : [] gar nicht an der Herleitung von Λ : [] beteiligt war, so ist die Aussage trivial. Andernfalls können wir nach dem letzten Lemma voraussetzen, daß

X^{+} ∪ {Γ:[]} ⊢_{PR} Λ:[]

gilt. Wir zeigen durch eine Herleitungsinduktion, daß daraus

X^{+} ∪ {Γ, Δ:[]} ⊢_{PR} Λ, Δ:[]

folgt. I.A.: In diesem Fall ist Γ = Λ und die Aussage ist trivial. I.S.: Der letzte Schluß hat die Gestalt

\frac{Γ_{1} :[Q_{1}] Γ_{2}, Q_{2} :[]}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2}.

In diesem Fall gilt nach IV

X^{+} ∪ {Γ, Δ:[]} ⊢_{PR} Γ_{2}, Q_{2}, Δ:[]. Da Γ_{2}, Q_{2}, Δ = Γ_{2}, Δ, Q_{2} ist, zeigt eine Anwendung der Prolog–Regel

X^{+} ∪ {Γ, Δ:[]} ⊢_{PR} Γ_{1}, Γ_{2}, Δ:[]

und da Λ = Γ_{1}, Γ_{2} ist, ist das die Behauptung. _{□} Das nächste Lemma dient der Vorbereitung des Beweises eines Konsistenzlemmas.

Lemma 3.8 Vor.: X ∪ {[P]:[]} ⊢_{PR} □. Beh.: X ∪ {[nP]:[]} ⊢_{PR} □ für alle n∈N. Beweis durch Induktion nach n: I.A.: n = 0. In diesem Fall gilt aus trivialen Gründen X ∪ {[0P] : []} ⊢_{PR} □,

denn □ war ja als []:[] definiert. I.S.: n → n + 1. Da nach IV X ∪ {[nP]:[]} ⊢_{PR} □ gilt, zeigt das letzte Lemma,

daß

X ∪ {[(n + 1)P]:[]} ⊢_{PR} □ oder X ∪ {[(n + 1)P]:[]} ⊢_{PR} [P]:[]

gilt. Im ersten Fall sind wir fertig, im zweiten folgt aus der Voraussetzung X ∪{[P]:[]} ⊢_{PR} □ und einem Hilfssatz, den wir gleich zeigen werden, daß X ∪ {[(n + 1)P]:[]} ⊢_{PR} □

gilt. _{□} Hilfssatz 3.9 (Herleitungssubstitution) Vor.: G ist eine negative Hornformel, so daß

X ⊢_{PR} G und X ∪ {G} ⊢_{PR} Γ:Δ gilt.

Beh.: Dann gilt schon X ⊢_{PR} Γ:Δ. Beweis: Wir führen den Beweis durch Induktion nach dem Aufbau der Herleitung der Sequenz Γ:Δ. I.A.: Γ : Δ ∈ X ∪ {G}. Falls Γ : Δ ∈ X ist, ist die Behauptung sofort klar. Ist

Γ:Δ = G, so liefert die erste Voraussetzung die gewünschte Aussage.

I.V.: Der letzte Schluß hat die Gestalt

\frac{Γ_{1} :[Q_{1}] Γ_{2}, Q_{2} :[]}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2}.

Nach IV gilt dann

X ⊢_{PR} Γ_{2}, Q_{2} :[] und X ⊢_{PR} Γ_{1} :[Q_{1}].

Nun liefert eine Anwendung der Prolog–Regel die Behauptung. _{□}

Lemma 3.10 (Konsistenzlemma)

Vor.: X ∪ {[]:[P]} ⊢_{PR} □ und X ∪ {[P]:[]} ⊢_{PR} □.

Beh.: X ⊢_{PR} □.

Beweis: Zunächst folgt aus der Voraussetzung X ∪ {[] : [P]} ⊢_{PR} □ mit Lemma (3.5), daß es ein n∈N mit

(1)  X ⊢_{PR} [nP]:[]

gibt. Die zweite Voraussetzung zeigt zusammen mit Lemma (3.8), daß

(2)  X ∪ {[nP]:[]} ⊢_{PR} □

gilt. Aus (1) und (2) folgt unter Verwendung von Hilfssatz (3.9) die Behauptung.

□

Das Konsistenzlemma versetzt uns in die Lage, im aussagenlogischen Fall einen Vollständigkeitssatz formulieren zu können.

Satz 3.11 Ist X eine Menge von geschlossenen Hornformeln, so gilt:

X ⊧_{E} ⊥ ⇒ X ⊢_{PR} □.

Beweis: Der Beweis verläuft nach dem selben Schema wie der Beweis von Satz (1.26). Es ist dort nur überall das Zeichen ⊢_{SK} durch ⊢_{PR} zu ersetzen. Entscheidend ist dann, daß wir mit dem Konsistenzlemma (3.10) ein Analogon zum Konsistenzlemma (1.25) haben. _{□}

3.3 Die eingeschränkte E–Prolog–Regel

So, wie wir die E–Prolog–Regel definiert haben, entspricht sie noch nicht dem, was in der Sprache Prolog implementiert ist. Wir definieren daher noch eine weitere Regel, die wir als eingeschränkte E–Prolog–Regel (SP) bezeichnen:

\frac{Γ:[Q_{1}] [Q_{2}|Δ] : []}{Γ, Δ:[]}(SP) mit Q_{1} ∼ Q_{2}.

Die eingeschränkte E–Prolog–Regel ist ein Spezialfall der Prolog–Regel. Der wesentliche Unterschied zur Prolog–Regel besteht darin, daß das Atom Q_{2}, das geschnitten wird, nun an erster Stelle in der negativen Sequenz stehen muß. Dadurch werden die Möglichkeiten, die wir zur Konstruktion von Herleitungen haben, wesentlich eingeschränkt. Als Konsequenz davon verkleinert sich der Suchraum, in dem beim automatischen Beweisen nach einer Herleitung gesucht werden muß. Erfreulicherweise reicht es aus, in diesem verkleinerten Suchraum nach einer Herleitung zu suchen, denn für die eingeschränkte E–Prolog–Regel gilt ein Analogon zum Vollständigkeitssatz (3.11). Bevor wir die E–Widerlegungsvollständigkeit der eingeschränkten E–Prolog–Regel allerdings zeigen können, bedarf es einiger Vorarbeit.

Zur Vereinfachung der Schreibweise vereinbaren wir für das Folgende, daß P immer für eine Menge von positiven Hornformeln steht. Weiter definieren wir die Länge einer Herleitung in der üblichen induktiven Weise, wobei Herleitungen, die nur aus Axiomen bestehen, definitionsgemäß die Länge 0 haben. Ist Δ : [] mit einer Herleitung der Länge n aus P ∪ {Γ:[]} mit Hilfe der eingeschränkten E–Prolog–Regel abgeleitet worden, so schreiben wir

P ∪ {Γ:[]} ⊢_{SP}^{n} Δ:[].

Wir notieren zunächst eine häufig benötigte Trivialität:

Lemma 3.12 (Transitivitätslemma)

Vor.: P ∪ {Γ:[]} ⊢_{SP}^{n} Δ:[] & P ∪ {Δ:[]} ⊢_{SP}^{m} Λ:[].

Beh.: P ∪ {Γ:[]} ⊢_{SP}^{n+m} Λ:[].

Beweis: Dieses Lemma wird durch Induktion nach m bewiesen. Da der Beweis trivial und außerdem im wesentlichen der gleiche wie bei dem Hilfssatz (3.9) ist, gehen wir hier nicht näher darauf ein.

Das nächste Lemma zeigt uns, daß wir Herleitungen aneinander hängen können.

Lemma 3.13 (Verklebungslemma)

Vor.: P ∪ {Γ:[]} ⊢_{SP}^{n} □ & P ∪ {Δ:[]} ⊢_{SP} Λ:[].

Beh.: P ∪ {Γ, Δ:[]} ⊢_{SP} Λ:[].

Beweis: Wir führen den Beweis durch Induktion nach n.

I.A.: n = 0. In diesem Fall ist Γ : [] = □, also Γ = []. Damit ist Γ, Δ = Δ und die Behauptung ist mit der zweiten Voraussetzung identisch.

I.S. n → n + 1.

Wir betrachten den \underline{ersten} Schluß der Herleitung P ∪ \{Γ:[]\} ⊢_{SP}^{n+1} □:

\frac{Γ_{1} :[Q_{1}] [Q_{2}|Γ_{2}] : []}{Γ_{1}, Γ_{2} :[]}(SP) mit Q_{1} ∼ Q_{2}.

Dann ist Γ = [Q_{2}|Γ_{2}] und es gilt

P ∪ {Γ_{1}, Γ_{2} :[]} ⊢_{SP}^{n} □.

Aufgrund der IV können wir annehmen, daß

(1)  P ∪ {Γ_{1}, Γ_{2}, Δ:[]} ⊢_{SP} Λ:[]

gilt. Die Herleitung

\frac{Γ_{1} :[Q_{1}] [Q_{2}|Γ_{2}, Δ]:[]}{Γ_{1}, Γ_{2}, Δ:[]}(SP)

verifiziert

(2)  P ∪ {[Q_{2}|Γ_{2}, Δ]:[]} ⊢_{SP} Γ_{1}, Γ_{2}, Δ:[],

und aus (1) und (2) folgt die Behauptung nun mit dem Transitivitätslemma (3.12). _{□}

Das nächste Lemma bezieht sich wieder auf die ursprüngliche E–Prolog– Regel (PR). Um es formulieren zu können, führen wir den Begriff der Teilliste ein. Anschaulich ist Λ dann eine Teilliste von Γ, wenn Λ aus Γ durch Streichung einiger Elemente hervorgeht.

Definition 3.14 (Λ ⊆ Γ) Eine Liste Λ ist eine Teilliste der Liste Γ (geschrieben Λ ⊆ Γ) genau dann, wenn sich diese Relation aus der folgenden induktiven Definition ableiten läßt.

I.A.: [] ⊆ Γ für alle Listen Γ.

I.S.: Gilt Λ ⊆ Γ und ist Q eine beliebige Primformel, so folgt:

[Q|Λ] ⊆ [Q|Γ] & Λ ⊆ [Q|Γ].

Lemma 3.15 (Verschärfungslemma)

Vor.: P ∪ {Γ:[]} ⊢_{PR}^{n} □ & Δ ⊆ Γ & Δ ≠ Γ.

Beh.: Es gibt ein m < n mit P ∪ {Δ:[]} ⊢_{PR}^{m} □.

Beweis durch Induktion nach n:

I.A.: n = 0. In diesem Fall gilt Γ:[] = □, also Γ = []. Dann gibt es kein Δ ⊆ Γ mit Δ ≠ Γ.

I.S.: n → n + 1.

Wir betrachten den \underline{ersten} Schluß der Herleitung P ∪ \{Γ:[]\} ⊢_{PR}^{n+1} □:

\frac{Γ_{1} :[Q_{1}] Γ_{2}, Q_{2} : []}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2}.

Je nachdem, ob Q_{2} ∈ Δ ist oder nicht, müssen wir verschiedene Überlegungen durchführen:

1. Fall: Δ ⊆ Γ_{2}. Dann gilt auch Δ ⊆ Γ_{1}, Γ_{2}. Falls Δ ≠ Γ_{1}, Γ_{2} ist, so zeigt die IV, daß es ein m < n mit

P ∪ {Δ:[]} ⊢_{PR}^{m} □

gibt. Wegen m < n < n + 1 ist das die Behauptung. Ist Δ = Γ_{1}, Γ_{2}, so muß Γ_{1} = ∅ sein und Δ = Γ_{2}. Da nach Voraussetzung

P ∪ {Γ_{1}, Γ_{2} :[]} ⊢_{PR}^{n} □

gilt, erhalten wir die Behauptung mit m := n < n + 1.

2. Fall: Δ ⊈ Γ_{2}. In diesem Fall gibt es ein Δ_{2} mit Δ = Δ_{2}, Q_{2}. Wir betrachten den folgenden Schluß mit der E–Prolog–Regel:

\frac{Γ_{1} :[Q_{1}] Δ_{2}, Q_{2} :[]}{Γ_{1}, Δ_{2} :[]}(PR).

Er zeigt, daß

(1)  P ∪ {Δ:[]} ⊢_{PR}^{1} Γ_{1}, Δ_{2} :[]

gilt. Da Γ_{1}, Δ_{2} ⊆ Γ_{1}, Γ_{2} ist und Γ_{1}, Δ_{2} ≠ Γ_{1}, Γ_{2} gilt, zeigt die IV, daß es ein m < n mit

(2)  P ∪ {Γ_{1}, Δ_{2} :[]} ⊢_{PR}^{m} □

gibt. Ein zu (3.12) analoges Transitivitätslemma für (PR) zeigt nun, daß aus (1) und (2)

P ∪ {Δ:[]} ⊢_{PR}^{m+1} □

folgt. Wegen m + 1 < n + 1 ist das die Behauptung. _{□}

Wir haben jetzt alles Material zusammen, um Widerlegungen, die mit der Regel (PR) geführt worden sind, in Widerlegungen zu transformieren, die mit der Spezialisierung (SP) der Regel (PR) auskommen.

Lemma 3.16 (Spezialisierungslemma)

Vor.: P ∪ {Γ:[]} ⊢_{PR}^{n} □.

Beh.: P ∪ {Γ:[]} ⊢_{SP} □.

Beweis durch Induktion nach n:

I.A.: n = 0. In diesem Fall gilt Γ:[] = □ und die Aussage ist trivial.

I.S.: n → n + 1.

Wir betrachten den \underline{ersten} Schluß der Herleitung von □ mit der Regel (PR). Er hat die Form

(0)  \frac{Γ_{1} :[Q_{1}]  Γ_{2}, Q_{2} : []}{Γ_{1}, Γ_{2} :[]}(PR) mit Q_{1} ∼ Q_{2},

wobei Γ = Γ_{2}, Q_{2} ist. Γ hat die Form Γ = [Q|Δ]. Je nachdem, ob Γ_{2}, Q_{2} = [Q_{2}|Γ_{2}] ist oder nicht, führen wir verschiedene Überlegungen durch:

1. Fall: Γ_{2}, Q_{2} ≠ [Q_{2}|Γ_{2}]. Dann ist klar, daß

Δ ⊆ Γ_{2}, Q_{2} aber Δ ≠ Γ_{2}, Q_{2} und [Q] ⊆ Γ_{2}, Q_{2} aber [Q] ≠ Γ_{2}, Q_{2}

gilt. Nun zeigt das Verschärfungslemma (3.15), daß es k, m ∈ N gibt, so daß

(1)  P ∪ {[Q]:[]} ⊢_{PR}^{k} □ & k < n + 1 und
(2)  P ∪ {Δ:[]} ⊢_{PR}^{m} □ & m < n + 1

gilt. Die IV zeigt, daß aus (1) und (2)

(3)  P ∪ {[Q]:[]} ⊢_{SP} □ und
(4)  P ∪ {Δ:[]} ⊢_{SP} □

folgt. Wenden wir auf (3) und (4) das Verklebungslemma (3.13) an, so folgt die Behauptung.

2. Fall: Γ_{2}, Q_{2} = [Q_{2}|Γ_{2}]. Da nach Voraussetzung

P ∪ {Γ_{1}, Γ_{2} :[]} ⊢_{PR}^{n} □

gilt, folgt mit der IV

(5)  P ∪ {Γ_{1}, Γ_{2} :[]} ⊢_{SP} □.

Da sich der Schluß (0) bei näherem Hinsehen als eine korrekte Anwendung von (SP) herausstellt, wissen wir

(6)  P ∪ {Γ:[]} ⊢_{SP} Γ_{1}, Γ_{2} :[].

Die Behauptung folgt nun mit dem Transitivitätslemma (3.12) aus (6) und (5). _{□} Bemerkung: Das Spezialisierunglemma läßt sich ohne Mühe dahin gehend verschärfen, daß die Herleitungsordnungen erhalten bleiben:

P ∪ {Γ:[]} ⊢_{PR}^{n} □ ⇒ P ∪ {Γ:[]} ⊢_{SP}^{n} □.

Da wir dieses Ergebnis aber im folgenden nicht benötigen, verzichten wir auf einen Beweis.

Da die E–Prolog–Regel nach Satz (3.11) für geschlossene Hornformeln E– widerlegungsvollständig ist, erhalten wir als Korollar:

Satz 3.17 Ist X eine Menge von geschlossenen Hornformeln, so gilt:

X ⊧_{E} ⊥ ⇒ X ⊢_{SP} □.

Unser Ziel ist es natürlich, diesen Satz auf beliebige Hornformeln zu übertragen. Zu diesem Zweck formulieren wir ein Analogon zum Lifting–Theorem (1.29).

Satz 3.18 (Lifting–Theorem) Ist R ein System von Ableitungsregeln, das für geschlossene Hornformeln E–widerlegungsvollständig ist, so ist R ∪ {Subst} für beliebige Hornformeln E–widerlegungsvollständig.

Beweis: Es sei X eine E–widersprüchliche Menge von Hornformeln. Dann gilt:

X ⊧_{E} ⊥  nach Annahme
⇒ grund(X) ⊧_{E} ⊥ nach Lemma (1.27)
⇒ grund(X) ⊢_{R} □ nach Voraussetzung
⇒ X ⊢_{R∪{Subst}} □ nach Lemma (1.28).

Um die Richtigkeit dieser Ableitung einzusehen, müssen wir uns nur klarmachen, daß sowohl Lemma (1.27) als auch Lemma (1.28) richtig bleiben, wenn X dort für eine Menge von Hornformeln steht. Das liegt einfach daran, daß Hornformeln spezielle Gentzenformeln sind. _{□}

Mit dem eben bewiesenen Lifting–Theorem für Hornformeln erhalten wir:

Theorem 3.19 {SP, Subst} ist E–widerlegungsvollständig für Hornformeln.

3.4 E–Resolution für Hornformeln

In diesem Abschnitt untersuchen wir, wie sich die Ergebnisse aus dem Abschnitt über die E–Resolution verschärfen lassen, wenn wir es mit Hornformeln zu tun haben. Es wird sich zeigen, daß in diesem Fall bereits ein Spezialfall der E– Resolution E–widerlegungsvollständig ist. Auf die E–Faktorisierungsregel können wir ganz verzichten. Wir definieren diesen Spezialfall der E–Resolution:

Definition 3.20 (Eingeschränkte E–Resolution) Der Schluß

\frac{Γ_{1} :[Q_{1}] [Q_{2}|Γ_{2}]:[]}{(Γ_{1}, Γ_{2} :[])μ}(SR)

ist eine Anwendung der eingeschränkten E–Resolutionsregel (SR), falls gilt:

1. μ = mgu_{E}(Q_{1}, Q_{2}).

2. FV (Γ_{1} :[Q_{1}]) ∩ FV ([Q_{2}|Γ_{2}]:[]) = ∅.

Für die zweite Bedingung in der Definition der eingeschränkten E–Resolution gilt das gleiche, was wir auch schon im Anschluß an die Definition der E–Resolution gesagt haben. Der wesentliche Unterschied zwischen der E–Resolution und ihrer eingeschränkten Version, die wir auch SLD–Resolution hätten nennen können, besteht darin, daß das Atom Q_{2}, das durch den Resolutionsschritt weggeschnitten wird, im Falle der eingeschränkten E–Resolution immer das erste Atom der an dem Schnitt beteiligten negativen Hornformel sein muß. Dadurch wird die Zahl der Möglichkeiten, zwei Sequenzen miteinander zu schneiden, stark eingeschränkt.

Der nächste Satz zeigt, daß Herleitungen, die nur mit der eingeschränkten E– Prolog–Regel und der Substitutionsregel arbeiten, in Herleitungen transformiert werden können, die mit der eingeschränkten E–Resolution auskommen. Im Rest dieses Abschnittes steht X für eine Menge von Hornformeln.

Satz 3.21 (Transformationssatz)

Vor.: X ⊢_{{SP,Subst}} Γ:[].

Beh.: ∃ Γ̂ ∃σ(X ⊢_{SR} Γ̂:[] & Γ = Γ̂σ).

Beweis: Wir führen den Beweis durch Induktion nach der Länge der Herleitung. Der aufmerksame Leser wird bemerken, daß sich der Beweis nur in wenigen Punkten von dem Beweis des analogen Satzes (3.3) für Gentzenformeln unterscheidet.

1. Fall: Γ : [] ∈ X. In diesem Fall setzen wir Γ̂ := Γ und σ := id. Damit folgt sofort die Behauptung.

2. Fall: Der letzte Schluß war eine Anwendung der Regel (SP):

\frac{Γ_{1} :[Q_{1}] [Q_{2}|Γ_{2}]:[]}{Γ_{1}, Γ_{2} :[]}(SP) mit Q_{1} ∼ Q_{2}.

Nach IV gibt es eine Liste Γ̂_{2}, ein Atom Q̂_{2} und eine Substitution τ_{2}, so daß

X ⊢_{SR} [Q̂_{2}|Γ̂_{2}]:[] & Q_{2} = Q̂_{2}τ_{2} & Γ_{2} = Γ̂_{2}τ_{2}

gilt. Die lineare Struktur einer Herleitung, die nur die Regeln (Subst) und (SP) verwendet, bedingt, daß die Sequenz Γ_{1} : [Q_{1}] entweder ein Element von X ist, oder aber durch alleiniges Anwenden der Substitutionsregel aus einem Element von X hergeleitet worden ist. In jedem Fall gibt es also eine Substitution τ_{1} und eine Sequenz Γ̂_{1} :[Q̂_{1}] ∈ X, so daß

Γ_{1} = Γ̂_{1}τ_{1} und Q_{1} = Q̂_{1}τ_{1}

gilt. Nach geeigneter Umbenennung der Variablen der Sequenz

Γ̂_{1} :[Q̂_{1}]

können wir davon ausgehen, daß diese Sequenz keine Variablen enthält, die auch in der Sequenz [Q̂_{2}|Γ̂_{2}]:[] vorkommen. Dann können wir o.B.d.A voraussetzen, daß τ_{1} und τ_{2} disjunkte Definitionsbereiche haben. Wir definieren eine neue Substitution τ durch:

τ := \{ \begin{matrix}τ_{1}(x) & falls x∈dom(τ_{1}); \\ τ_{2}(x) & sonst. \end{matrix}

Es ist klar, daß

Γ_{1} :[Q_{1}] = (Γ̂_{1} :[Q̂_{1}])τ und [Q_{2}|Γ_{2}]:[] = ([Q̂_{2}|Γ̂_{2}]:[])τ

ist. Da Q̂_{1}τ = Q_{1} ∼ Q_{2} = Q̂_{2}τ ist, sind Q̂_{1} und Q̂_{2} E–unifizierbar. Also existieren Substitutionen μ und σ so daß

μ = mgu_{E}(Q̂_{1}, Q̂_{2}), Q̂_{1}μ ∼ Q̂_{2}μ und τ = μσ

gilt. Daher ist

\frac{Γ̂_{1} :[Q̂_{1}] [Q̂_{2}|Γ̂_{2}] : []}{(Γ̂_{1}, Γ̂_{2} : [])μ}(SR)

eine korrekte Anwendung der eingeschränkten E–Resolutionsregel. Definieren wir Γ̂ := (Γ̂_{1}, Γ̂_{2})μ, so gilt

X ⊢_{SR} Γ̂:[]

und es ist Γ:[] = (Γ̂:[])σ.

3. Fall: Der letzte Schluß ist eine Anwendung der Substitutionsregel:

\frac{Γ_{1} :[]}{Γ_{1}τ : []}(Subst).

Nach IV gibt es eine Sequenz Γ̂:[] und eine Substitution ϱ mit

X ⊢_{SR} Γ̂:[]

und es ist Γ_{1} = Γ̂ϱ. Definieren wir σ := ϱτ, so gilt Γ = Γ_{1}τ = Γ̂ϱτ = Γ̂σ. Das schließt den Beweis ab. _{□}

Da wir in Theorem (3.19) gezeigt hatten, daß das System {SP, Subst} ein E–widerlegungsvollständiges System von Ableitungsregeln für Hornformeln ist, erhalten wir nun als Korollar zum Transformationssatz unser eigentliches Hauptergebnis:

Theorem 3.22 (SR) ist E–widerlegungsvollständig für Hornformeln.

Korrekte und berechnete Antworten

Bisher haben wir einen E–widerlegungsvollständigen Kalkül konstruiert. In der Praxis besteht die Aufgabe aber nicht darin, eine gegebene Menge von Hornformeln auf Widersprüchlichkeit zu untersuchen, sondern wir möchten beispielsweise wissen, ob sich aus den positiven Hornformeln eines Prolog–Programmes P die Existenz von Objekten, die gewissen Eigenschaften genügen, beweisen läßt. Wir präzesieren diese Fragestellung. Gegeben sei ein Prolog–Programm P. P ist eine Menge von positiven Hornformeln. Weiter seien Q_{1}, ⋯, Q_{n} Primformeln und es gelte FV (Q_{1} ∧ ⋯ ∧ Q_{n}) = {x_{1}, ⋯, x_{m}}. Die zu klärende Frage lautet: Gilt

(1)  P ⊧_{E} ∃x_{1} ⋯ ∃x_{m}(Q_{1} ∧ ⋯ ∧ Q_{n}) ?

Sollte die Antwort auf die Frage (1) positiv ausfallen, so wäre es wünschenswert, wenn wir den mit der Beantwortung von (1) verbundenen Existenzbeweis so führen könnten, daß wir in der Lage sind Terme t_{1}, ⋯, t_{m} zu berechnen, für die

(2)  P ⊧_{E} (Q_{1} ∧ ⋯ ∧ Q_{n})[x_{1}/t_{1}, ⋯, x_{m}/t_{m}]

gilt. Es wird sich herausstellen, daß wir sogar eine Verschärfung von (2) zeigen können. Um diese Verschärfung formulieren zu können, benötigen wir die Begriffe “korrekte Antwort” und “berechnete Antwort”.

Definition 4.1 (korrekte Antwort) Ist P ein Prolog–Programm, Γ : [] ein Goal und ϑ eine Substitution mit dom(ϑ) ⊆ FV (Γ), so ist ϑ eine korrekte Antwort für P ∪ {Γ:[]} genau dann, wenn

P ⊧_{E} ∀((Q_{1} ∧ ⋯ ∧ Q_{n})ϑ)

gilt, falls Γ = [Q_{1}, ⋯, Q_{n}] ist.

Ist ϑ eine korrekte Antwort für P ∪ {Γ:[]}, so ist die Frage (1) offenbar positiv zu beantworten. Darüber hinaus können wir dann durch die Definitionen

t_{1} := ϑ(x_{1}) & ⋯ & t_{m} := ϑ(x_{m})

Terme angeben, die (2) erfüllen. Unser Ziel wird es daher sein, einen Algorithmus zu entwickeln, mit dem wir zu gegebenen P ∪ {Γ : []} eine korrekte Antwort berechnen können.

Da wir nur einen widerlegungsvollständigen Kalkül zur Verfügung haben, besteht die einzige Möglichkeit, eine Antwort auf die Frage (1) zu erhalten, darin, daß wir (1) in eine äquivalente Konsistenzaussage überführen. Es gilt

P ⊧_{E} ∃(Q_{1} ∧ ⋯ ∧ Q_{n}) ⇔ P ∪ {∀(Q_{1} ∧ ⋯ ∧ Q_{n} → ⊥)} ⊧_{E} ⊥.

Also ist (1) äquivalent zu der Frage, ob die Menge

(3)  E ∪ P ∪ {∀(Q_{1} ∧ ⋯ ∧ Q_{n} → ⊥)}

inkonsistent ist. Da es sich bei (3) um eine Menge von Hornformeln handelt, zeigt der zuletzt bewiesene Vollständigkeitssatz (3.22), daß die Frage der Inkonsistenz von (3) äquivalent zu

(4)  P ∪ {Γ:[]} ⊢_{SR} □

ist, falls Γ durch Γ := [Q_{1}, ⋯, Q_{n}] definiert ist.

Der Schlüssel, um den Beweis von (1) konstruktiv führen zu können, besteht darin, daß wir die in der Widerlegung (4) benutzten Substitutionen analysieren. Zu diesem Zweck definieren wir für Herleitungen, die nur mit der Regel (SR) arbeiten, das Konzept der berechneten Antwort. Solche Herleitungen werden wir im übrigen in Zukunft als E–SLD–Herleitungen bezeichnen. Handelt es sich bei der hergeleiteten Formel um den Widerspruch □, so sprechen wir von einer E–SLD–Widerlegung.

Wir definieren nun den Begriff der berechneten Antwort. Sind in einer gegebenen E–SLD–Herleitung H μ_{1}, ⋯, μ_{n} die MGUs der in H verwendeten SR–Schlüsse, so ist ϑ = μ_{1} ⋯ μ_{n} die berechnete Antwort dieser Herleitung. Die formale Definition lautet:

Definition 4.2 (berechnete Antwort) Wir definieren für eine E–SLD–Herleitung den Begriff der berechneten Antwort induktiv. Ist ϑ eine berechnete Antwort der Herleitung von P ∪ {Γ:[]} ⊢_{SR} Δ:[], so schreiben wir:

P ∪ {Γ:[]} ⊢_{SR}^{ϑ} Δ:[].

I.A.: Ist Δ:[] = Γ:[], so ist die berechnete Antwort die Identität:

P ∪ {Γ:[]} ⊢_{SR}^{id} Γ:[].

I.S.: Ist

\frac{Δ_{1} :[Q_{1}] [Q_{2}|Δ_{2}]:[]}{(Δ_{1}, Δ_{2} :[])μ}(SR)

der letzte Schluß der Herleitung von P ∪ {Γ:[]} ⊢_{SR} Δ:[] und gilt

P ∪ {Γ:[]} ⊢_{SR}^{ϑ} [Q_{2}|Γ_{2}]:[],

so gilt auch

P ∪ {Γ:[]} ⊢_{SR}^{ϑμ} Δ:[].

4.1 Korrektheit berechneter Antworten

In der berechneten Antwort werden alle Substitutionen aufgesammelt, die erforderlich sind, um die bei der Herleitung benutzten Schnitte durchführen zu können. Würden diese Substitutionen direkt am Anfang der Herleitung durchgeführt, so würde der Rest der Herleitung mit rein aussagenlogischen Schlüssen auskommen. Um diesen Gedanken formalisieren zu können, ordnen wir jedem Programm P ein Programm P^{+} zu, daß neben den positiven Hornformeln aus P auch alle Instanzen von positiven Hornformeln aus P enthält. Es gilt also

P^{+} := {Rσ : R∈P und σ ist eine Substitution}.

Der Herleitungsbegriff

P^{+} ∪ {Γ : []} ⊢_{SP} Δ : []

hat eine interessante Stabilitätseigenschaft: Er läßt sich mit einer Substitution multiplizieren. Wie das im Detail funktioniert, zeigt uns das nächste Lemma.

Lemma 4.3 (Multiplikationslemma)

Vor.: P^{+} ∪ {Γ:[]} ⊢_{SP} Δ:[].

Beh.: P^{+} ∪ {Γτ:[]} ⊢_{SP} Δτ:[] für jede Substitution τ.

Beweis durch Herleitungsinduktion:

I.A.: Δ:[] = Γ:[]. Dieser Fall ist trivial.

I.V.: Der letzte Schluß hat die Gestalt

\frac{Δ_{1} :[Q_{1}] [Q_{2}|Δ_{2}]:[]}{Δ_{1}, Δ_{2} :[]}(SP) mit Q_{1} ∼ Q_{2}.

Nach Definition von (SP) ist klar, daß Δ_{1} : [Q_{1}] ein Element der Menge P^{+} ist. Es gibt also Δ̂_{1} und Q̂_{1}, sowie eine Substitution σ, so daß

Δ_{1} = Δ̂_{1}σ und Q_{1} = Q̂_{1}σ

gilt. Daraus folgt sofort

Δ_{1}τ = Δ̂_{1}στ und Q_{1}τ = Q̂_{1}στ und das zeigt, daß auch die Sequenz (Δ_{1} : [Q_{1}])τ ein Element der Menge P^{+} ist. Nach IV gilt andererseits

P^{+} ∪ {Γτ:[]} ⊢_{SP} ([Q_{2}|Δ_{2}]:[])τ

und daraus folgt die Behauptung durch einen Schnitt gemäß der eingeschränkten E–Prolog–Regel, denn Q_{1} ∼ Q_{2} impliziert offenbar Q_{1}τ ∼ Q_{2}τ. _{□}

Wir zeigen nun, wie sich die Substitutionen einer E–SLD–Herleitung vorziehen lassen. Lemma 4.4 (Vorziehen von Substitutionen) Vor.: P ∪ {Γ:[]} ⊢_{SR}^{ϑ} Δ:[]. Beh.: P^{+} ∪ {Γϑ:[]} ⊢_{SP} Δ:[]. Beweis durch Herleitungsinduktion: I.A.: Δ:[] = Γ:[]. Dann ist ϑ = id und die Behauptung ist trivial. I.V.: Der letzte Schluß hat die Gestalt

\frac{Δ_{1} :[Q_{1}] [Q_{2}|Δ_{2}]:[]}{(Δ_{1}, Δ_{2} :[])μ}(SR),

es gilt P ∪ {Γ:[]} ⊢_{SR}^{τ} [Q_{2}|Δ_{2}]:[] und es ist ϑ = τμ. Die IV zeigt, daß P^{+} ∪ {Γτ:[]} ⊢_{SP} [Q_{2}|Δ_{2}]:[]

gilt. Mit dem Multiplikationslemma folgt daraus

P^{+} ∪ {Γτμ:[]} ⊢_{SP} ([Q_{2}|Δ_{2}]:[])μ.

Da (Δ_{1} :[Q_{1}])μ eine Instanz einer Regel aus P ist, zeigt der Schluß

\frac{(Δ_{1} :[Q_{1}])μ ([Q_{2}|Δ_{2}]:[])μ}{(Δ_{1}, Δ_{2} :[])μ}(SP)

die Behauptung. _{□} Der nächste Satz stellt eine Verbindung zwischen berechneten und korrekten

Antworten her und zeigt so, welche zusätzlichen Informationen die berechnete Antwort einer E–SLD–Widerlegung liefert. Satz 4.5 (Korrektheit der berechneten Antwort)

Vor.: P ∪ {Γ:[]} ⊢_{SR}^{ϑ} □.

Beh.: ϑ|FV (Γ) ist eine korrekte Antwort für P ∪ {Γ:[]}.

Beweis: Aus der Voraussetzung folgt mit dem Lemma (4.4) über das Vorziehen der Substitutionen, daß

(1)  P^{+} ∪ {Γϑ:[]} ⊢_{SP} □

gilt. Da der Kalkül (SP) mit rein aussagenlogischen Mitteln arbeitet, können wir die in Γϑ noch auftretenden freien Variablen durch neue Konstanten ersetzen. Ist FV (Γϑ) = {x_{1}, ⋯, x_{n}}, so wählen wir eine Menge {c_{1}, ⋯, c_{n}} von neuen Konstanten und definieren eine Substution σ durch

σ := [x_{1}/c_{1}, ⋯, x_{n}/c_{n}].

Mit der Definition

Γ̂ := Γϑ[x_{1}/c_{1}, ⋯, x_{n}/c_{n}]

und dem Multiplikationslemma folgt aus (1), daß

(2)  P^{+} ∪ {Γ̂:[]} ⊢_{SP} □

gilt. Da der Kalkül (SP) E–korrekt ist, zeigt (2), daß

(3)  P^{+} ∪ {Γ̂:[]} ⊧_{E} ⊥

gilt. Die Sequenz Γ̂ enthält nach Konstruktion keine freien Variablen mehr. Daher ist (3) äquivalent zu

(4)  P^{+} ⊧_{E} ¬(Γ̂:[]).

In dieser Formel können wir die Konstanten c_{1}, ⋯, c_{n} wieder durch die freien Variablen x_{1}, ⋯, x_{n} ersetzen. Dann haben wir

(5)  P^{+} ⊧_{E} ¬(Γϑ:[]).

Ist Γ = [Q_{1}, ⋯, Q_{n}], so ist (5) logisch äquivalent zu

(6)  P^{+} ⊧_{E} (Q_{1} ∧ ⋯ ∧ Q_{n})ϑ.

Da die E–Gültigkeit einer Formel nach unserer Definition gleichwertig mit der E–Gültigkeit ihres Allabschlußes ist, zeigt (6), daß

(7)  P ⊧_{E} ∀((Q_{1} ∧ ⋯ ∧ Q_{n})ϑ)

gilt, denn jede E–Struktur, die ein Modell von P ist, ist auch ein Modell von P^{+}. Damit haben wir aber die Behauptung gezeigt, denn selbstverständlich können wir ϑ in (7) durch ϑ|FV ((Q_{1} ∧ ⋯ ∧ Q_{n})) ersetzen. _{□}

4.2 Berechenbarkeit korrekter Antworten

In diesem Abschnitt beschäftigen wir uns mit der Frage, in welcher Weise der letzte Satz umkehrbar ist. Wir untersuchen also die Frage, in welcher Weise korrekte Antworten berechenbar sind. Wünschenswert wäre ein Ergebnis, das zeigen würde, daß es für jede korrekte Antwort ϑ eine berechnete Antwort τ gibt, so daß ϑ und τ auf dom(ϑ) übereinstimmen. Eine kurze Überlegung zeigt uns aber, daß diese Aussage so falsch sein muß. Das liegt daran, daß berechnete Antworten immer möglichst allgemein sind. Ein kurzes Beispiel erläutert das Problem. Wir setzen für den Augenblick E = ∅, nehmen an, daß p ein einstelliges Prädikatszeichen und c eine Konstante ist und definieren

P := {[]:[p(x)]},

was äquivalent zu der Formel ∀x p(x) ist. Dann ist

ϑ(x) := \{ \begin{matrix}c & falls x = x_{0}; \\ x & sonst. \end{matrix}

eine korrekte Antwort für P ∪ {[p(x_{0})] : []}, aber offenbar ist die Identität die einzige berechnete Antwort für P ∪ {[p(x_{0})]:[]}.

Obwohl das obige Beispiel unsere ursprüngliche Hoffnung zunichte macht, so zeigt es uns auch einen möglichen Ausweg. In dem oberen Beispiel ist die berechnete Antwort allgemeiner als die korrekte Antwort, und darüber hinaus läßt sich jede korrekte Antwort durch Instanziierung der berechneten Antwort erhalten. Wir werden zeigen, daß diese Beobachtung nicht auf das letzte Beispiel beschränkt ist. Vorher ist allerdings noch ein nützliches Lemma zu beweisen.

Lemma 4.6 (Lifting–Lemma)

Vor.: P ∪ {Γτ:[]} ⊢_{SR}^{ϑ} Δ:[].

Beh.: ∃Δ̂ ∃ϑ̂, σ(P ∪ {Γ:[]} ⊢ϑ̂ ; SR Δ̂:[] und τϑ = ϑ̂σ und Δ = Δ̂σ).

Beweis durch Herleitungsinduktion:

I.A.: Δ = Γτ und ϑ = id. In diesem Fall definieren wir Δ̂ := Γ, ϑ̂ := id und σ := τ. Damit wird die Behauptung offenbar erfüllt.

I.V.: Der letzte Schluß hat die Gestalt

\frac{Δ_{1} :[Q_{1}] [Q_{2}|Δ_{2}]:[]}{(Δ_{1}, Δ_{2} :[])μ}(SR),

und es gilt P ∪ {Γτ:[]} ⊢_{SR}^{φ} [Q_{2}|Δ_{2}]:[]. Dann ist ϑ = φμ und nach IV gibt es Q̂_{2}, Δ̂_{2} und zwei Substitutionen ϱ und φ̂, so daß

P ∪ {Γ:[]} ⊢φ̂ ; SR [Q̂_{2}|Δ̂_{2}]:[] & τφ = φ̂ϱ & [Q_{2}|Δ_{2}] = [Q̂_{2}|Δ̂_{2}]ϱ

gilt. Wir können o.B.d.A. davon ausgehen, daß

FV (Δ_{1} :[Q_{1}]) ∩ dom(ϱ) = ∅

ist. Die Gleichungskette

Q_{1}ϱμ = Q_{1}μ ∼ Q_{2}μ = Q̂_{2}ϱμ

zeigt, daß Q_{1} und Q̂_{2} E–unifizierbar sind und daß darüber hinaus ϱμ ein E–Unifikator von Q_{1} und Q̂_{2} ist. Es gibt also Substitutionen ν und σ mit ν = mgu_{E}(Q_{1}, Q̂_{2}) und ϱμ = νσ. Außerdem ist

\frac{Δ_{1} :[Q_{1}] [Q̂_{2}|Δ̂_{2}]:[]}{(Δ_{1}, Δ̂_{2} :[])ν}(SR)

eine korrekte Anwendung der Regel (SR), die zeigt, daß

(∗)  P ∪ {Γ:[]} ⊢ϑ̂ ; SR (Δ_{1}, Δ̂_{2} :[])ν

gilt, wenn wir ϑ̂:= φ̂ν definieren. Da

Δ = Δ_{1}μ, Δ_{2}μ = Δ_{1}ϱμ, Δ̂_{2}ϱμ = (Δ_{1}, Δ̂_{2})νσ

ist, definieren wir Δ̂ := (Δ_{1}, Δ̂_{2})ν. Dann folgt Δ = Δ̂σ, und aus der Gleichungskette

τϑ = τφμ = φ̂ϱμ = φ̂νσ = ϑ̂σ

folgt zusammen mit (∗) der Rest der Behauptung. _{□}

Falls die Identität eine korrekte Antwort für P ∪ {Γ:[]} ist, so zeigt das nächste Lemma, daß diese Antwort auch berechnet werden kann. Auf diesen Spezialfall werden wir später die allgemeine Berechenbarkeit korrekter Antworten zurückführen.

Lemma 4.7

Vor.: Die Identität id ist eine korrekte Antwort für P ∪ {Γ:[]}.

Beh.: Es gibt eine Substitution ϑ, so daß gilt:

P ∪ {Γ:[]} ⊢_{SR}^{ϑ} □ und ϑ|FV (Γ) = id.

Beweis: Wir nehmen an, daß Γ = [Q_{1}, ⋯, Q_{n}] ist. Aus der Voraussetzung folgt

(1)  P ⊧_{E} ∀(Q_{1} ∧ ⋯ ∧ Q_{n}).

Sind x_{1}, ⋯, x_{m} alle in Γ frei auftretenden Variablen, so wählen wir neue Konstanten c_{1}, ⋯, c_{m}, von denen wir voraussetzen, daß sie weder in P noch in Γ auftreten. Wir definieren eine Substitution σ durch

σ := [x_{1}/c_{1}, ⋯, x_{m}/c_{m}].

Wegen (1) gilt

P ⊧_{E} (Q_{1} ∧ ⋯ ∧ Q_{n})σ.
⇒ P ∪ {Γσ:[]} ⊧_{E} ⊥.

Da die eingeschränkten E–Resolution nach Theorem (3.22) E–widerlegungsvollständig ist, gibt es eine E–SLD–Widerlegung von P ∪ {Γσ:[]}. Es gibt also eine Substitution ϑ̂, so daß gilt:

P ∪ {Γσ:[]} ⊢ϑ̂ ; SR □.

Da die Konstanten c_{1}, ⋯, c_{m} weder in P noch in Γ auftreten, können wir die Substitution σ rückgängig machen und finden mit der Definition ϑ := ϑ̂σ^{−1}

P ∪ {Γ:[]} ⊢_{SR}^{ϑ} □,

wobei wir mit σ^{−1} die zu σ inverse “Substitution” [c_{1}/x_{1}, ⋯, c_{m}/x_{m}] bezeichnen. Wegen FV (Γσ) = ∅ gilt ϑ̂|FV (Γσ) = id und daraus folgt

ϑ|FV (Γ) = id. _{□}

Wir sind nun in der Lage, das Hauptergebnis dieses Kapitels zu formulieren.

Theorem 4.8 (Berechenbarkeit korrekter Antworten)

Vor.: Die Substitution τ ist eine korrekte Antwort für P ∪ {Γ:[]}.

Beh.: Es gibt Substitutionen ϑ̂ und τ̂, so daß gilt:

P ∪ {Γ:[]} ⊢ϑ̂ ; SR □ & ϑ̂ ≤_{E} τ̂ & τ̂|FV (Γ) = τ.

Beweis: Ist Γ = [Q_{1}, ⋯, Q_{n}], so folgt aus der Voraussetzung, daß

P ⊧_{E} ∀((Q_{1} ∧ ⋯ ∧ Q_{n})τ)

gilt. Das ist aber zu der Aussage äquivalent, daß die Identität eine korrekte Antwort für P ∪ {Γτ:[]} ist. Nach dem letzten Lemma gibt es eine Substitution φ, so daß

P ∪ {Γτ:[]} ⊢_{SR}^{φ} □ und φ|FV (Γτ) = id

gilt. Nach dem Lifting–Lemma (4.6) gibt es eine Substitution ϑ̂, so daß

(2)  P ∪ {Γ:[]} ⊢ϑ̂ ; SR □ & ϑ̂ ≤_{E} τφ

gilt. Definieren wir τ̂ := τφ, so folgt wegen φ|FV (Γτ) = id, daß

(3)  τ̂|FV (Γ) = τ

gilt. Nach Definition von τ̂ folgt aus (2)

(4)  ϑ̂ ≤_{E} τ̂

und aus (2), (3) und (4) folgt jetzt die Behauptung. _{□}

Bemerkung: Für den Fall E = ∅ wurde ein zu Theorem (4.8) analoges Ergebnis zuerst von Clark [Cl79] gefunden. So, wie dieses Ergebnis in Lloyd [Llo87] zitiert wird, ist es allerdings falsch. Lloyd definiert den Begriff der berechneten Antwort etwas anders, als wir das hier getan haben. Gilt in unserer Terminologie

P ∪ {Γ:[]} ⊢_{SR}^{ϑ} ⊥,

so definiert Lloyd die berechnete Antwort als ϑ|FV (Γ). Er behauptet, daß es für jede korrekte Antwort ϑ eine berechnete Antwort σ und eine Substitution γ gibt, so daß ϑ = σγ ist. Wir widerlegen diese Behauptung durch ein Gegenbeispiel. Es sei

P := {[]:[p(f(y))]} und G := [p(x)]:[].

Dann ist σ = [x/f(y)] eine berechnete und ϑ = [x/f(c)] für eine beliebige Konstante c eine korrekte Antwort für P ∪ {G}. Gäbe es eine Substitution γ mit ϑ = σγ, so würde die Gleichungskette

f(c) = ϑ(x) = γ(σ(x)) = γ(f(y)) = f(γ(y))

implizieren, daß γ die Bindung y/c enthält. Dann zeigt

ϑ(y) = γ(σ(y)) = γ(y) = c,

daß ϑ(y) = c ist, was offenbar falsch ist.

Das oben geschilderte Problem hat uns dazu geführt, den Begriff der berechneten Antwort anders zu formulieren, als das in der Literatur üblich ist. Der mißtrauisch gewordene Leser möge sich davon überzeugen, daß das obere Beispiel bei unserer Definition der berechneten Antwort keine Schwierigkeiten macht.

Teil II

Untersuchungen zur Vollständigkeit der SLDNF–Resolution SLDNF–Resolution

Obwohl sich viele interessante Theorien durch Hornformeln axiomatisieren lassen, vergleiche etwa Padawitz [Pad88], haben Hornformeln doch nicht die volle Ausdruckskraft der Prädikatenlogik. So läßt sich beispielsweise die Aussage, daß für alle x entweder p(x) oder q(x) gilt, nicht durch Hornformeln beschreiben. Die obige Aussage ist äquivalent zu

∀x(¬q(x) → p(x)).

In dieser Schreibweise sehen wir, wie der Begriff der Hornformel zu verallgemeinern ist, um auch negative Information berücksichtigen zu können. Wir definieren:

Definition 5.1 (normale Programme) Sequenzen der Gestalt

Γ:[P] oder Γ:[]

sind normale Hornformeln, wenn P eine Primformel und Γ eine Liste von Literalen ist. Ein normales Programm P ist eine Menge normaler Hornformeln der Gestalt Γ : [P]. Eine Sequenz der Form Γ : [] bezeichnen wir als normales Goal.

Bemerkung: Ist [Q_{1}, ⋯, Q_{m}, ¬R_{1}, ⋯, ¬R_{n}]:[P] eine normale Hornformel, so ist sie in unserer bisherigen Interpretation äquivalent zu der quantorenfreien Formel

(∗)  Q_{1} ∧ ⋯ ∧ Q_{m} → R_{1} ∨ ⋯ ∨ R_{n} ∨ P.

Wir führen normale Hornformeln als neue Formelklasse ein, weil wir dadurch in der Lage sind, die SLD–Resolution auf diese Formelklasse zu erweitern. Der Kalkül, den wir dabei entwickeln, wird allerdings weder korrekt noch vollständig sein, falls wir normale Hornformeln analog zu (∗) interpretieren. Aus diesem Grunde entwickeln wir später für normale Programme eine alternative Semantik.

Im folgenden werden wir gelegentlich normale Hornformeln als Klauseln bezeichnen. Das ist zwar, wie die obige Bemerkung zeigt, eigentlich nicht richtig, aber den aufmerksamen Leser sollte es trotzdem nicht verwirren.

Auch normale Programme haben noch nicht die volle Ausdruckskraft der Prädikatenlogik. So kann aus einem normalen Programm P beispielsweise keine negative Information abgeleitet werden, denn die Herbrand–Basis B ist immer ein Modell von P. Wollen wir trotzdem negative Informationen aus normalen Programmen ableiten, so müssen wir den Rahmen der klassischen Prädikatenlogik verlassen. Daher lassen sich unsere folgenden Überlegungen nicht mehr zum Gebiet des automatischen Beweisens rechnen, sondern sie gehören in den Rahmen der künstlichen Intelligenz. Aus diesem Grund (und um unsere weiteren Überlegungen nicht zu umständlich werden zu lassen) setzen wir im folgenden immer E = ∅ voraus.

Ein möglicher Weg um aus normalen Programmen negative Informationen abzuleiten, ist die von Reiter [Reit78] vorgeschlagene “closed world assumption”, die wir mit CWA abkürzen. Der Kerngedanke bei der CWA besteht in der Annahme, daß all das falsch ist, was nicht aus den zur Verfügung stehenden Fakten und Regeln abgeleitet werden kann. Die bei der CWA benutzte Schlußregel lautet: Ist P ein normales Programm und Q eine geschlossene Primformel, für die P |̸= Q gilt, so kann auf ¬Q geschlossen werden.

Die CWA ist für Datenbanken eine sehr natürliche Schlußregel. Da aber die Frage, ob P ⊧ Q gilt, im allgemeinen unentscheidbar ist, ist die CWA in der oben vorgestellten Form nicht zu implementieren. Eine Möglichkeit, die CWA näherungsweise zu realisieren bietet die “negation as failure”–Regel, abgekürzt NF. Diese von Clark [Cl78] eingeführte Regel sieht vor, eine geschlossene Primformel Q dann als falsch anzusehen, wenn der Suchbaum, der bei der Suche nach einer Widerlegung von P ∪ {[Q]:[]} entsteht, endlich und erfolglos ist.

Im ersten Abschnitt präzisieren wir den Begriff der SLDNF–Herleitung. Im wesentlichen ist eine SLDNF–Herleitung eine SLD–Herleitung, die zusätzlich mit der NF–Regel arbeitet. Da die NF–Regel auf Suchbäume für andere SLDNF– Herleitungen zurückgreift, ist das Konzept der SLDNF–Herleitung wesentlich komplexer als das Konzept der SLD–Herleitung.

Im zweiten Abschnitt zeigen wir auf syntaktischem Wege die Widerspruchsfreiheit der SLDNF–Resolution. Der von uns bewiesene Satz geht über das von Clark in [Cl78] gezeigte Ergebnis hinaus. Dieser beweist einen Korrektheitssatz, in dem er das Konzept der Vervollständigung comp(P) eines Programmes P als semantisches Gegenstück zur SLDNF–Resolution einführt. Dieses Konzept werden wir in einem späteren Kapitel analysieren.

Im Rest dieses Kapitel steht P immer für ein normales Programm und G für ein normales Goal. Γ und Δ stehen für endliche Listen von Literalen und Q werden wir (evt. mit Indizes) benutzen, um Literale zu bezeichnen.

5.1 Definition der SLDNF–Resolution

Um den Begriff der SLDNF–Resolution definieren zu können, müssen wir zunächst die beiden Konzepte “SLDNF–Herleitung vom Rang k” und “SLDNF– Baum vom Rang k” durch eine simultane Induktion nach k festlegen.

Da es sehr ermüdend ist, ständig von einer SLDNF–Herleitung vom Rang k oder einem SLDNF–Baum vom Rang k zu sprechen, vereinbaren wir die Schreibweise SLDNF(k): Eine SLDNF(k)–Herleitung ist also eine SLDNF–Herleitung vom Rang k, und der Ausdruck SLDNF(k)–Baum ist analog zu verstehen.

Betrachten wir eine SLD–Herleitung, so stellen wir fest, daß ihre Struktur linear ist. Die wesentliche Information zur Rekonstruktion der Herleitung ist bereits in der Folge der negativen Sequenzen enthalten, die an den einzelnen Schlüssen beteiligt sind. Wir machen uns diese Beobachtung bei der Definition der SLDNF(0)–Herleitung zunutze. Als SLDNF(0)–Herleitung bezeichnen wir diejenigen Folgen, die nach der weiter unten gegebenen induktiven Definition konstruiert worden sind. Um die Notation zu vereinfachen, vereinbaren wir vorab, daß die Schreibweise

H zeigt P ∪ {Γ:[]} ⊢_{0}^{ϑ} Δ:[]

ausdrücken soll, daß die Folge H eine SLDNF(0)–Herleitung von Δ : [] aus P ∪ {Γ:[]} mit der berechneten Antwort ϑ ist.

Definition 5.2 (SLDNF–Herleitung vom Rang 0)

I.A.: Die Folge [Γ:[]] ist eine SLDNF(0)–Herleitung der Sequenz Γ:[] aus P ∪ {Γ:[]} mit der Identität als berechneter Antwort. Mit der oben festgelegten Schreibweise gilt also:

[Γ:[]] zeigt P ∪ {Γ:[]} ⊢_{0}^{id} Γ:[].

I.S.: Ist H eine SLDNF(0)–Herleitung der Sequenz [Q_{2}|Δ_{2}]:[] aus P ∪ {Γ:[]} mit ϑ als berechneter Antwort und ist Δ_{1} :[Q_{1}] eine Klausel aus P, so daß Q_{1} und Q_{2} unifizierbar sind, so gilt:

H, [(Δ_{1}, Δ_{2} :[])μ] zeigt P ∪ {Γ:[]} ⊢_{0}^{ϑμ} (Δ_{1}, Δ_{2} :[])μ,

falls μ durch μ := mgu(Q_{1}, Q_{2}) definiert ist. _{□}

Ist der Widerspruch □ die hergeleitete Formel einer SLDNF(0)–Herleitung, so sprechen wir von einer SLDNF(0)–Widerlegung. Dem Leser wird aufgefallen sein, daß der einzige Unterschied zwischen einer SLDNF(0)–Widerlegung und einer SLD–Widerlegung in der Schreibweise liegt. Wir haben die Definition der SLDNF(0)–Herleitung hier aus zwei Gründen gegeben. Zum einen benötigen wir den Begriff gleich und müssen ihn daher griffbereit haben. Zum anderen wird es durch die neue Schreibweise möglich, den Begriff der SLDNF(k)–Herleitung in einer bezüglich k homogenen Gestalt zu formulieren.

Wir geben nun eine induktive Definition der SLDNF(0)–Bäume. SLDNF– Bäume sind Bäume, bei denen sowohl die Knoten als auch die Kanten zwischen den Knoten markiert sind. Die Knoten sind mit normalen, negativen Sequenzen markiert, während die Kanten mit Substitutionen markiert sind.

Definition 5.3 (SLDNF–Baum vom Rang 0)

I.A.: Der Baum, der nur aus der mit Γ : [] markierten Wurzel besteht, ist ein SLDNF(0)–Baum zu P ∪ {Γ:[]}.

I.S.: Wir setzen voraus, daß B ein SLDNF(0)–Baum zu P ∪ {Γ : []} und L ein Blatt von B ist, das mit [Q_{2}|Δ_{2}] : [] markiert ist. Außerdem soll Q_{2} eine Primformel sein. Falls es Klauseln Δ_{1} : [Q_{1}] in P gibt, so daß Q_{1} und Q_{2} unifizierbar sind, können wir B zu einem SLDNF(0)–Baum B̂ erweitern, indem wir für jede Klausel Δ_{1} : [Q_{1}] aus P, deren Kopf Q_{1} mit Q_{2} unifizierbar ist, einen mit (Δ_{1}, Δ_{2} : [])μ markierten Knoten an L hängen, wobei μ durch μ := mgu(Q_{1}, Q_{2}) gegeben sein muß. Die zu dem neuen Knoten führende Kante markieren wir mit μ. Gibt es keine Klausel in P, deren Kopf mit Q_{2} unfizierbar ist, so sagen wir, daß das Blatt L ausgewachsen ist. _{□}

Wir nennen einen SLDNF(0)–Baum ausgewachsen, wenn alle seine Blätter ausgewachsen sind. Ein SLDNF(0)–Baum ist erfolglos, wenn er ausgewachsen ist, aber keines seiner Blätter mit der widersprüchlichen Sequenz □ markiert ist. Diese Redeweise wird klarer, wenn wir uns davon überzeugen, daß SLDNF(0)–Bäume nichts anderes als endliche Suchbäume für SLDNF(0)–Herleitungen sind. Wir präzisieren diese Behauptung: Ist B ein SLDNF(0)–Baum zu P ∪ {Γ:[]} und ist (f_{i})_{0≤i≤n} ein Faden in B, dessen Knoten mit Γ_{0} : [], Γ_{1} : [], ⋯, Γ_{n}: [] und dessen Kanten mit ϑ_{1}, ⋯, ϑ_{n} markiert sind, so gilt offenbar

(∗)  [Γ_{0} :[], ⋯, Γ_{n}:[]] zeigt P ∪ {Γ_{0} :[]} ⊢_{0}^{ϑ} Γ_{n}:[],

falls wir ϑ := ϑ_{1} ⋯ ϑ_{n} definieren. Jeder Zweig von B läßt sich also als Herleitung auffassen. Aber es gilt noch mehr: Ist H eine SLDNF(0)–Herleitung der Sequenz Δ:[] aus P ∪{Γ_{0} :[]}, so gibt es einen SLDNF(0)–Baum, der einen Zweig besitzt, welcher diese Herleitung in dem Sinne von (∗) repräsentiert. Auf einen exakten Beweis dieser Behauptungen verzichten wir an dieser Stelle, da wir später für SLDNF(k)–Herleitungen und SLDNF(k)–Bäume einen analogen Zusammenhang herleiten werden.

Existiert für ein normales Programm P und ein normales Goal [Q] : [] ein erfolgloser SLDNF(0)–Baum zu P ∪{[Q]:[]}, so kann es keine SLD–Widerlegung von P ∪ {[Q]:[]} geben, es gilt also

(1)  P ⊬ Q.

Daher gestattet es die NF–Regel, auf

(2)  P ⊢ ¬Q

zu schließen. Der Schluß von (1) nach (2) mit der NF–Regel ist von einer wesentlich anderen Natur, als die bisher verwendeten Schlußregeln. Diese waren lokal, es war nur zu prüfen, ob die endlich vielen Prämissen in einem durch die Form der Schlußregel genauer festgelegten Verhältnis zu der Konklusion standen. Jetzt ist die Sache anders, weil nun das ganze zugrunde liegende Programm P und alle mit P denkbaren Herleitungen in die Überlegungen mit einbezogen werden müssen. Da diese Herleitungen prinzipiell beliebig lang werden können, können wir im allgemeinen ohne zusätzliche Informationen nicht entscheiden, ob die NF–Regel überhaupt anwendbar ist.

Ein weiterer wesentlicher Unterschied zu unseren bisherigen Ableitungsregeln ist der nicht–monotone Charakter der NF–Regel. Bisher war es so, daß aus der Herleitbarkeit gewisser Prämissen auf die Herleitbarkeit einer bestimmten Konklusion geschlossen werden konnte, bei der NF–Regel ist das gerade umgekehrt. Den beiden oben angeführten Eigenschaften der NF–Regel ist es zu verdanken, daß wir bei der Definition der SLDNF–Herleitungen einen beträchtlich höheren Aufwand treiben müssen, als wir das bisher gewöhnt sind.

Wir legen zunächst den Begriff “SLDNF(k)–Baum” durch eine induktive Definition nach k fest. Der Induktionsanfang wird durch die Definitionen (5.3) gegeben. Im Induktionsschritt definieren wir:

Definition 5.4 (SLDNF–Baum vom Rang k+1)

I.A.: Der Baum, der nur aus der mit Γ : [] markierten Wurzel besteht, ist ein SLDNF(k+1)–Baum zu P ∪ {Γ:[]}.

I.S.: Ist B ein SLDNF(k+1)–Baum zu P ∪ {Γ : []} und ist L ein Blatt von B, das mit [Q_{2}|Δ_{2}]:[] markiert ist, so unterscheiden wir zwei Fälle:

1. Fall: Q_{2} ist ein positives Literal.

Falls es Klauseln Δ_{1} : [Q_{1}] in P gibt, so daß Q_{1} und Q_{2} unifizierbar sind, können wir B zu einem SLDNF(k+1)–Baum B̂ erweitern, indem wir für jede Klausel Δ_{1} :[Q_{1}] aus P, deren Kopf Q_{1} mit Q_{2} unifizierbar ist, einen mit (Δ_{1}, Δ_{2} : [])μ markierten Knoten an L hängen, wobei wir μ := mgu(Q_{1}, Q_{2}) setzen. Die zu dem neuen Knoten führende Kante markieren wir mit μ. Gibt es keine Klausel in P, deren Kopf mit Q_{2} unifizierbar ist, so sagen wir, daß das Blatt L ausgewachsen ist.

2. Fall: Q_{2} ist ein negatives Literal, Q_{2} = ¬Q̂_{2}. Ist Q_{2} nicht geschlossen, so sagen wir, daß das Blatt L hängt. Im folgenden setzen wir voraus, daß Q_{2} geschlossen ist. Gibt es einen erfolglosen SLDNF(k)–Baum zu P ∪ {[Q̂_{2}] : []}, so erhalten wir aus B einen neuen SLDNF(k+1)–Baum B̂, indem wir an das Blatt L einen Knoten, der mit der Sequenz Δ_{2} : [] markiert ist, hängen. Die zu diesem Knoten führende Kante markieren wir mit der Identität id.

Gibt es einen SLDNF(k)–Baum zu P ∪ {[Q̂_{2}] : []}, der ein mit dem Widerspruch □ markiertes Blatt enthält, so nennen wir das Blatt L ausgewachsen. _{□}

Wir nennen einen SLDNF(k+1)–Baum ausgewachsen, wenn alle seine Blätter ausgewachsen sind. Das impliziert insbesondere, daß keines seiner Blätter hängt. Ein SLDNF(k+1)–Baum ist erfolglos, wenn er ausgewachsen ist, aber keines seiner Blätter mit der widersprüchlichen Sequenz □ markiert ist.

Nun sind wir in der Lage, den Begriff der SLDNF(k+1)–Herleitung durch eine induktive Definition festzulegen. Ähnlich wie beim Begriff der SLDNF(0)– Herleitung vereinbaren wir, daß die Schreibweise

H zeigt P ∪ {Γ:[]} ⊢_{k+1}^{ϑ} Δ:[]

ausdrücken soll, daß die Folge H eine SLDNF(k+1)–Herleitung von Δ : [] aus P ∪ {Γ:[]} mit der berechneten Antwort ϑ ist.

Definition 5.5 (SLDNF–Herleitung vom Rang k+1)

I.A.: Es gilt

[Γ:[]] zeigt P ∪ {Γ:[]} ⊢_{k+1}^{id} Γ:[].

I.S.: Gilt

H zeigt P ∪ {Γ:[]} ⊢_{k+1}^{ϑ} [Q_{2}|Δ_{2}]:[],

so unterscheiden wir zwei Fälle:

1. Fall: Q_{2} ist ein positives Literal, also eine Primformel. Ist Δ_{1} : [Q_{1}] eine Klausel aus P, so daß Q_{1} und Q_{2} unifizierbar sind, so gilt

H, [(Δ_{1}, Δ_{2} :[])μ] zeigt P ∪ {Γ:[]} ⊢_{k+1}^{ϑμ} (Δ_{1}, Δ_{2} :[])μ,

falls μ durch μ := mgu(Q_{1}, Q_{2}) definiert ist. In diesem Fall sagen wir, daß der letzte Schluß der Herleitung ein Schnitt ist.

2. Fall: Q_{2} ist ein negatives Literal, und es gilt Q_{2} = ¬Q̂_{2}. Ist Q_{2} geschlossen und gibt es einen erfolglosen SLDNF(k)–Baum zu P ∪ {[Q̂_{2}] : []}, so gilt:

H, [Δ_{2} :[]] zeigt P ∪ {Γ:[]} ⊢_{k+1}^{ϑ} Δ_{2} :[].

In diesem Fall sprechen wir von einer Anwendung der NF–Regel. Ist Q_{2} nicht geschlossen, so sagen wir, daß die Herleitung H hängt.

Wie im Falle der SLDNF(0)–Herleitungen sprechen wir von einer SLDNF(k+1)– Widerlegung, falls die hergeleitete Formel der Widerspruch □ ist.

Wir kommen nun zum eigentlichen Ziel des Abschnittes, der Definition der SLDNF–Widerlegung.

Definition 5.6 (SLDNF–Widerlegung) H ist eine SLDNF–Widerlegung von P ∪{Γ:[]} mit berechneter Antwort ϑ, falls es ein k ∈N gibt, so daß gilt:

H zeigt P ∪ {Γ:[]} ⊢_{k}^{ϑ} □.

In diesem Fall schreiben wir

P ∪ {Γ:[]} ⊢_{ω}^{ϑ} □.

Falls die Angabe von ϑ unerheblich ist, unterdrücken wir sie.

Bemerkung: Unsere Definition der SLDNF–Widerlegung weicht von der in Lloyd [Llo87] gegebenen Darstellung in zwei wesentlichen Punkten ab.

Zum einen erzwingen wir, daß immer das erste Literal in einem Goal ausgewählt wird. Diese Festlegung der Auswahlregel ist notwendig, um später einen Vollständigkeitssatz beweisen zu können. Im übrigen ist das auch die Auswahlregel, die in den vorhandenen Prolog–Implementationen verwendet wird.

Ein weiterer wesentlicher Unterschied zur Darstellung in Lloyd besteht darin, daß bei uns die SLDNF–Herleitungen und –Bäume immer endlich sind, während diese Strukturen bei Lloyd auch unendlich sein können. Außerdem sind die Bäume, die dort als SLDNF–Bäume bezeichnet werden, immer “ausgewachsen”. Da wir SLDNF–Bäume und –Herleitungen induktiv definiert haben, sind diese Strukturen notwendig endlich. Sie stimmen nur in dem Fall, daß sie “ausgewachsen” sind, mit den von Lloyd definierten Begriffen überein. Die oben dargelegten Unterschiede sind allerdings unwichtig, denn der zentrale Begriff der SLDNF– Widerlegung ist in beiden Fällen endlich und, wie der geübte Leser sich leicht klarmacht, erfreulicherweise auch identisch.

Zum Abschluß dieses Abschnittes überlegen wir uns, inwieweit unsere Definition der SLDNF–Widerlegung dem Konzept “negation as failure” gerecht wird. In diesem Zusammenhang stellen sich zwei Fragen:

1. Angenommen, es gibt eine SLDNF–Widerlegung von P ∪ {[¬Q]:[]}. Folgt dann, daß es keine SLDNF–Widerlegung von P ∪ {[Q]:[]} gibt?

2. Angenommen, es gibt \underline{keine} SLDNF–Widerlegung von P ∪ \{[Q]:[]\}. Folgt dann, daß es eine SLDNF–Widerlegung von P ∪ {[¬Q]:[]} gibt?

Die erste Frage zielt auf die syntaktische Widerspruchsfreiheit des SLDNF– Kalküls ab, während es bei der zweiten Frage um eine Art syntaktischer Vollständigkeit geht. Die erste Frage werden wir im nächsten Abschnitt ausführlich untersuchen. Die zweite Frage beantworten wir negativ, indem wir ein Gegenbeispiel konstruieren:

Es sei p ein nullstelliges Prädikatszeichen und P bestehe nur aus der Klausel [p]:[p]. Durch eine einfache Induktion nach der Länge der Herleitung sehen wir sofort, daß jeder Versuch, aus P ∪ {[p]:[]} eine Herleitung zu konstruieren, eine Folge der Form

[[p]:[], [p]:[], ⋯, [p]:[]]

liefert. Also gibt es keine SLDNF–Widerlegung von P ∪ {[p] : []}. Es gibt aber auch keine SLDNF–Widerlegung von P ∪ {[¬p] : []}, denn dann müßte es einen erfolglosen SLDNF–Baum zu P ∪ {[p]:[]} geben. Jeder SLDNF–Baum zu P ∪ {[p] : []} hat nur einen einzigen Zweig, dessen sämtliche Knoten mit der Sequenz [p]:[] markiert sind. Dann ist insbesondere auch jedes Blatt des Baumes mit dieser Sequenz markiert. Da es in P eine Klausel gibt, deren Kopf mit p unifizierbar ist, folgt, daß kein Blatt des Baumes ausgewachsen ist. Damit gibt es keinen ausgewachsenen und erst recht keinen erfolglosen Baum zu P ∪{[p]:[]}.

5.2 Syntaktische Korrektheit

In diesem Abschnitt wollen wir zeigen, daß es keine Primformel Q und kein normales Programm P gibt, so daß sowohl P ∪ {[Q] : []} als auch P ∪ {[¬Q] : []} eine SLDNF–Widerlegung haben. Bei der oberen Aussage handelt es sich offenbar um eine Korrektheitseigenschaft. Üblicherweise werden Beweise von Korrektheitsaussagen dadurch geführt, daß eine Struktur definiert wird, in der die verwendeten Schlußregeln als korrekt erkannt werden können. Wir werden später den Begriff der Vervollständigung eines normalen Programmes P einführen. Dadurch wären wir in der Lage, eine für die SLDNF–Resolution adäquate Semantik einzuführen. Bedauerlicherweise ist die auf diesem Wege erhaltene Korrektheitsaussage schwächer als das Ergebnis, das wir zeigen wollen. Das liegt daran, daß für ein konsistentes, normales Programm P die Vervollständigung von P nicht mehr konsistent zu sein braucht. Daher wird sich der Beweis der Widerspruchsfreiheit der SLDNF–Resolution als schwieriger herausstellen, als wir das bei einer Korrektheitsaussage normalerweise gewohnt sind. Wir beginnen unsere Überlegungen damit, daß wir einige triviale Korollare aus der Definition der SLDNF(k)–Herleitungen und – Bäume ziehen.

Lemma 5.7 (Monotonie–Eigenschaft der SLDNF(k)–Bäume)

Vor.: B ist ein SLDNF(k)–Baum zu P ∪ {Γ:[]}.

Beh.: B ist ein SLDNF(l)–Baum zu P ∪ {Γ:[]} für alle l ≥ k.

Beweis: Eigentlich müßten wir dieses Lemma durch eine Induktion nach k beweisen, wobei dann noch eine Nebeninduktion nach dem Aufbau der SLDNF(k)–Bäume fällig wäre. Da diese Induktionen aber genau wie die entsprechenden Induktionen bei der Definition dieses Begriffs geführt werden und darüberhinaus völlig klar sind, ersparen wir uns einen ausführlichen Beweis. Wir überzeugen uns lediglich durch einen kurzen Blick auf die Definitionen von der Tatsache, daß jeder SLDNF(k)–Baum auch ein SLDNF(k+1)–Baum ist. Daraus folgt die Behauptung.

□

Ein kurzer Blick auf die Definitionen zeigt:

Korollar 5.8 Ist B ein ausgewachsener SLDNF(k)–Baum und ist l ≥ k, so ist B auch als SLDNF(l)–Baum ausgewachsen.

Beweis: Genau genommen muß dieses Korollar bei dem induktiven Beweis des letzten Lemmas mitbewiesen werden. Da wir dort den Beweis nicht ausgeführt haben, können wir das hier natürlich auch nicht tun. _{□}

Lemma 5.9 (Monotonie–Eigenschaft der SLDNF(k)–Herleitungen)

Vor.: H zeigt P ∪ {Γ:[]} ⊢_{k}^{ϑ} Δ:[].

Beh.: H zeigt P ∪ {Γ:[]} ⊢_{l}^{ϑ} Δ:[] für alle l ≥ k.

Beweis: Auch dieses Lemma ist eine direkte Konsequenz der Definitionen. _{□}

Bemerkung: Die letzten beiden Lemmata sowie das letzte Korollar zeigen, daß die Eigenschaft von P ∪ {Γ : []}, eine SLDNF(k)–Widerlegung oder einen erfolglosen SLDNF(k)–Baum zu haben, in gewisser Weise von k unabhängig sind, sofern k nur hinreichend groß gewählt wird. Dies ist eine Absolutheitseigenschaft, die uns in späteren Beweisen das Leben erheblich vereinfachen wird, denn wissen wir beispielsweise, daß es natürliche Zahlen k und l gibt, so daß ein SLDNF(k)– Baum und ein SLDNF(l)–Baum mit gewissen Eigenschaften existiert, so können wir ohne weiteres voraussetzen, daß k = l ist, wir müssen dann für k und l nur ihr Maximum einsetzen. (Wie dies genau zu verstehen ist, wird dem Leser spätestens bei den entsprechenden Beweisen klar werden.)

An dieser Stelle möchten wir klarstellen, daß unser Kalkül eine Monotonieeigenschaft \underline{nicht} hat, die normalerweise in der Prädikatenlogik üblich ist. Sind P und P̂ zwei normale Programme mit P ⊆ P̂ und gibt es eine SLDNF–Widerlegung von P ∪ {Γ : []}, so folgt daraus nicht, daß es auch eine SLDNF–Widerlegung von P̂ ∪ {Γ:[]} gibt.

Wir klären nun die Zusammenhänge zwischen SLDNF–Bäumen und –Herleitungen.

Lemma 5.10 Ist B ein SLDNF(k)–Baum zu P ∪ {Γ_{0} : []} und ist die Folge (k_{i})_{0≤i≤n} ein Zweig in B, dessen Knoten mit Γ_{0} : [], ⋯, Γ_{n} : [] und dessen Kanten mit ϑ_{1}, ⋯, ϑ_{n} markiert sind, so gilt

[Γ_{0} :[], ⋯, Γ_{n}:[]] zeigt P ∪ {Γ_{0} :[]} ⊢_{k}^{ϑ} Γ_{n}:[],

falls wir ϑ := ϑ_{1} ⋯ ϑ_{n} definieren.

Beweis: Wir führen den Beweis durch eine Induktion nach dem Aufbau des SLDNF(k)–Baumes B.

I.A.: Der Baum besteht nur aus der mit Γ : [] markierten Wurzel. Dann ist n = 0, Γ_{0} = Γ = Γ_{n}, ϑ = ∅ = id und die Behauptung ist trivial.

I.S.: Der Baum ist aus einem Baum B̂ dadurch entstanden, daß letzterer an einem Blatt L̂ erweitert worden ist. Falls das Blatt L̂ nicht zu dem Zweig (k_{i})_{0≤i≤n} gehört, folgt die Behauptung sofort aus der IV. Wir können also o.B.d.A. voraussetzen, daß L̂ mit dem Knoten k_{n−1} identisch ist. Dieser Knoten sei mit der Sequenz Γ_{n−1} = [Q_{2}|Δ_{2}] markiert. Unsere weitere Argumentation hängt davon ab, ob das Literal Q_{2} positiv oder negativ ist.

1. Fall: Q_{2} ist positiv. Dann gibt es eine Sequenz Δ_{1} : [Q_{1}] in P, so daß Q_{1} und Q_{2} unifizierbar sind, es ist μ = mgu(Q_{1}, Q_{2}), es gilt

Γ_{n}:[] = (Δ_{1}, Δ_{2} :[])μ,

der Knoten k_{n} ist mit Γ_{n} markiert und die Kante von k_{n−1} nach k_{n} trägt die Marke μ. Dann gilt ϑ_{n} = μ. Da nach IV

[Γ_{0} :[], ⋯, Γ_{n−1} :[]] zeigt P ∪ {Γ:[]} ⊢ϑ̂ ; k Γ_{n−1} :[]

mit ϑ̂ = ϑ_{1} ⋯ ϑ_{n−1} gilt, folgt die Behauptung aus der induktiven Definition der SLDNF(k)–Herleitung.

2. Fall: Q_{2} ist negativ, Q_{2} = ¬Q̂_{2}. In diesem Fall gilt Γ_{n} = Δ_{2} und ϑ_{n} = id. Außerdem gibt es einen erfolglosen SLDNF(k-1)–Baum zu P ∪ {[Q̂_{2}]:[]}. Nach IV wissen wir:

[Γ_{0} :[], ⋯, Γ_{n−1} :[]] zeigt P ∪ {Γ:[]} ⊢ϑ̂ ; k Γ_{n−1} :[]

mit ϑ̂ = ϑ_{1} ⋯ ϑ_{n−1}, und dann zeigt die Definition der SLDNF(k)– Herleitung die Behauptung. _{□}

Eigentlich ist sowohl dieses Lemma als auch sein Beweis eine triviale Konsequenz der Definitionen. Das gilt auch für die Umkehrung, die wir jetzt formulieren.

Lemma 5.11 Gilt

[Γ_{0} :[], ⋯, Γ_{n}:[]] zeigt P ∪ {Γ_{0} :[]} ⊢_{k}^{ϑ} Γ_{n}:[],

so gibt es für jeden SLDNF(k)–Baum B zu P ∪ {Γ_{0} :[]} einen SLDNF(k)–Baum B̂, der aus B durch Erweiterungen hervorgeht und einen Zweig (k_{i})_{0≤i≤m} der Länge m ≥ n enthält, so daß die Knoten k_{0}, ⋯, k_{n} mit Γ_{0} :[], ⋯, Γ_{n}:[] markiert sind, die Kanten von k_{i−1} nach k_{i} für i ∈ {1, ⋯, n} die Marken ϑ_{i} tragen und ϑ := ϑ_{1} ⋯ ϑ_{n} ist.

Der Beweis dieses Lemmas wird wie beim letzten Lemma durch eine Induktion, diesmal nach dem induktiven Aufbau der SLDNF–Bäume, geführt. Da der Beweis trivial aber länglich ist, verzichten wir darauf.

Wir kommen nun zum Hauptergebnis dieses Abschnittes, dem Nachweis der Widerspruchsfreiheit der SLDNF–Resolution.

Theorem 5.12 (Widerspruchsfreiheit der SLDNF–Resolution) Für keine Primformel Q und kein normales Programm P gilt

(∗)  P ∪ {[Q]:[]} ⊢_{ω} □ und P ∪ {[¬Q]:[]} ⊢_{ω} □.

Beweis: Wir führen den Beweis indirekt und machen die Annahme, daß (∗) gilt. Dann gibt es k, l ∈N und Substitutionen ϑ und φ, so daß

(1)  P ∪ {[Q]:[]} ⊢_{k}^{ϑ} □ und

(2)  P ∪ {[¬Q]:[]} ⊢_{l}^{φ} □

gilt. Definieren wir m := max(k, l+1), so gelten (1) und (2) auch mit m anstelle von k bzw. l. Aus (2) folgt, daß es einen erfolglosen SLDNF(m)–Baum B zu P ∪ {[Q]:[]} gibt. Aus (1) folgt, daß es eine SLDNF(m)–Herleitung H gibt, für die

H zeigt P ∪ {[Q]:[]} ⊢_{m}^{ϑ} □

gilt. Nach dem letzten Lemma läßt sich B zu einem SLDNF(m)–Baum B̂ mit folgenden Eigenschaften erweitern: B̂ enthält einen Zweig (k_{i})_{0≤i≤m} der Länge m ≥ n, so daß die Knoten k_{0}, ⋯, k_{n} mit Γ_{0}, ⋯, Γ_{n} markiert sind und

H = [Γ_{0} :[], ⋯, Γ_{n}:[]]

gilt. Die Kanten von k_{i−1} nach k_{i} tragen für i ∈ {1, ⋯, n} die Marken ϑ_{i} und es gilt ϑ := ϑ_{1} ⋯ ϑ_{n}. Da B ein erfolgloser Baum ist, ist B insbesondere ausgewachsen. Also ist B gleich B̂ und der Zweig (k_{i})_{0≤i≤m} ist schon in B enthalten. Da das letzte Blatt dieses Zweiges mit □ markiert ist, kann B nicht erfolglos sein. Dieser Widerspruch zeigt die Behauptung. _{□}

Konsistent geordnete Programme

Unser Ziel ist es, für eine bestimmte, noch näher zu definierende Klasse von normalen Programmen einen Vollständigkeitssatz für die SLDNF–Resolution zu beweisen. Wie wir später sehen werden, besteht eine notwendige Bedingung für die Ableitung eines Vollständigkeitssatzes darin, daß zu jedem normalen Programm P und zu jedem normalen Goal G, für die P ∪{G} zu dem Fragment der Sprache gehört, für das wir den Vollständigkeitssatz zeigen wollen, ein “ausgewachsener” SLDNF–Baum für P ∪ {G} existiert. Die Konstruktion eines ausgewachsenen SLDNF–Baumes kann an zwei Stellen scheitern:

1. Die Berechnung kann an einem negativen Literal L, das nicht geschlossen ist, “hängen” bleiben. (Mit Berechnung meinen wir hier und im folgenden immer den Versuch, einen ausgewachsenen SLDNF–Baum zu konstruieren.)

2. Es kann passieren, daß es zu P ∪ {G} Herleitungen gibt, die beliebig lange fortgesetzt werden können. Dadurch kann der SLDNF–Baum zu P ∪{G} nie “auswachsen”. (Ein triviales Beispiel dafür kennen wir bereits aus dem letzten Kapitel: P = {[p]:[p]} und G = [p]:[].)

In diesem Kapitel werden wir uns mit den beiden oben dargestellten Problemen auseinandersetzen. Dadurch sind wir dann im nächsten Kapitel in der Lage, einen Vollständigkeitssatz für die SLDNF–Resolution zu zeigen.

Ein klassischer Ansatz, der dazu dient, das Hängenbleiben einer Berechnung zu vermeiden, besteht darin, die Aufmerksamkeit auf sogenannte erlaubte Programme zu beschränken. Dieses Konzept geht auf Clark [Cl78] zurück. Wir werden uns im ersten Abschnitt mit diesem Begriff beschäftigen. Bedauerlicherweise ist die Klasse der erlaubten Programme viel zu klein, um von großem praktischen Nutzen sein zu können. So darf beispielsweise ein Fakt in einem erlaubten Programm keine freien Variablen enthalten.

Im zweiten Abschnitt stellen wir den Begriff der konsistenten Input/Output– Spezifikation (im folgenden immer mit I/O–Spezifikation abgekürzt) vor. Dieser Begriff wird sich als wesentlich tragfähiger als das alte Konzept der erlaubten Programme herausstellen. Das wesentliche Ergebnis dieses Abschnittes wird sein, daß eine Rechnung für P ∪{G} nie hängen bleibt, wenn es für P ∪{G} eine konsistente I/O–Spezifikation gibt.

Im dritten Abschnitt führen wir die bezüglich einer I/O–Spezifikation geordneten Programme ein. Hier zeigen wir, daß Herleitungen zu geordneten Programmen immer irgendwann abbrechen müssen.

Nachdem wir im zweiten und im dritten Abschnitt zwei Teilklassen der normalen Programme eingeführt haben, die gewisse, erstrebenswerte Eigenschaften besitzen, zeigen wir im letzten Abschnitt, daß der Schnitt dieser beiden Teilklassen ausdrucksstark genug ist, um die primitiv–rekursiven Funktionen berechnen zu können.

In diesem Kapitel steht P immer für ein normales Programm, G für ein normales Goal und K und L (evt. mit Indizes) stehen für Literale. Primformeln bezeichnen wir mit Q.

6.1 Erlaubte Programme

In diesem Abschnitt stellen wir die “erlaubten” Programme vor. Die wesentliche Eigenschaft erlaubter Programme besteht darin, daß bei erlaubten Programmen die Berechnungen zu erlaubten Goals nie hängen bleiben können. Die Definitionen und Ergebnisse dieses Abschnittes werden im folgenden nicht benötigt. Der Abschnitt dient nur dazu, unsere eigenen Ergebnisse abzugrenzen.

Definition 6.1 (erlaubte Programme) Es sei P ein normales Programm und G ein normales Goal.

Eine Programm–Klausel [L_{1}, ⋯, L_{n}]:[Q] aus P heißt zulässig, wenn jede Variable, die in der Klausel auftritt, in Q oder in einem positiven Literal L_{i} auftritt.

Eine Programm–Klausel [L_{1}, ⋯, L_{n}]:[Q] aus P heißt erlaubt, wenn jede Variable, die in der Klausel auftritt, in einem positiven Literal L_{i} auftritt.

Hat das Goal G die Gestalt [L_{1}, ⋯, L_{n}] : [], so heißt G erlaubt, wenn jede Variable, die in G auftritt, in einem positiven Literal L_{i} auftritt.

Wir nennen P ∪ {G} erlaubt, wenn folgende Bedingungen erfüllt sind:

1. Jede Klausel in P ist zulässig.

2. Ist p ein Prädikatssymbol, das in einem positiven Literal im Rumpf des Goals G oder in einem positiven Literal im Rumpf einer Klausel aus P auftritt und ist C eine Klausel aus der Definition von p, so ist C erlaubt.

3. G ist erlaubt.

(Mit der Definition von p meinen wir die Menge aller der Klauseln, in deren Kopf p auftritt.)

Bei Lloyd [Llo87] findet sich der folgende Satz, der die Bedeutung der Definition des Begriffes “ P ∪ {G} ist erlaubt” klärt:

Es sei P ein normales Programm und G sei ein normales Goal, so daß P ∪ {G} erlaubt ist. Dann gilt:

a) Keine Berechnung zu P ∪ {G} kann hängen bleiben.

b) Ist ϑ eine berechnete Antwort für P ∪ {G} , so gilt

FV (Gϑ) = ∅.

Um die Richtigkeit des obigen Satz sicherzustellen, benötigen wir als zusätzliche Voraussetzung, daß eine sogenannte “sichere” Auswahlregel bei der SLDNF– Resolution benutzt wird. Die von uns verwendete Auswahlregel ist keine sichere Auswahlregel im Sinne von Lloyd. Der Satz wird auch falsch, wenn wir ihn auf unsere Definition der SLDNF–Resolution anwenden. Dies zeigt das Beispiel

P := {[]:[p(c)], []:[q(c)]} und G := [¬p(x), q(x)]:[].

Eine Berechnung zu P ∪ {G} bleibt sofort hängen.

Es gibt zwei Möglichkeiten, die Voraussetzungen dieses Satzes so abzuändern, daß er auch mit der von uns vorgestellten Form der SLDNF–Resolution gültig bleibt.

Zum einen können wir die Definition der bei der SLDNF–Resolution verwendeten normalen Hornformeln so abändern, daß wir verlangen, daß die positiven Literale immer vor den negativen Literalen aufgeführt werden. Dieser Weg wurde in

[Str90] beschritten. In diesem Fall erweist sich das dort eingeführte Konzept der normalen Programme mit konsistenter I/O–Spezifikation als echte Verallgemeinerung der erlaubten Programme.

Eine andere Möglichkeit besteht darin, die Definition der erlaubten Programme abzuändern. Die Definitionen müssen wie folgt geändert werden:

zulässige Klauseln: Eine Programm–Klausel [L_{1}, ⋯, L_{n}] : [Q] aus P heißt zulässig, wenn jede Variable, die in einem L_{i} auftritt, in Q oder in einem positiven Literal L_{j} mit j ≤ i auftritt.

erlaubte Klauseln: Eine Programm–Klausel [L_{1}, ⋯, L_{n}] : [Q] aus P heißt erlaubt, wenn gilt:

1. Jede Variable, die in Q auftritt, tritt in einem positiven Literal L_{i} auf.

2. Jede Variable, die in einem L_{i} auftritt, tritt in einem positiven Literal L_{j} mit j ≤ i auf. erlaubte Goals: Hat das Goal G die Gestalt [L_{1}, ⋯, L_{n}]:[], so heißt G erlaubt,

wenn jede Variable, die in einem L_{i} auftritt, in einem positiven Literal L_{j} mit j ≤ i auftritt.

Mit dieser Definition kann der oben zitierte Satz mit den gleichen Methoden bewiesen werden, mit denen wir im nächsten Abschnitt einen analogen Satz über die noch zu definierenden Programme mit konsistenter I/O–Spezifikation zeigen werden. Da wir das Ergebnis nicht weiter benötigen werden, verzichten wir hier auf einen Beweis.

Bemerkung: Ist []:[Q] ein Fakt aus einem normalen Programm P, ist weiter q das in Q auftretende Prädikatszeichen und tritt q in dem Goal G auf, so folgt aus der Erlaubtheit von P ∪ {G} , daß die Klausel [] : [Q] zulässig sein muß. Dann müssen alle Variablen aus Q in einem positiven Literal im Rumpf dieser Klausel auftreten. Da der Rumpf leer ist, geht das nur gut, wenn in Q keine freien Variablen auftreten. Dies zeigt, daß die Klasse der erlaubten Programme nur ein sehr ausdrucksschwaches Fragment der Klasse der normalen Programme ist.

Die in diesem Abschnitt vorgestellten Ergebnisse gehen auf Lloyd und Topor [LT86] und Shepherdson [Shep85] zurück.

6.2 Konsistente I/O–Spezifikationen

In diesem Abschnitt stellen wir den Begriff der I/O–Spezifikation vor. Dieser Begriff ermöglicht es, zwischen Variablen, die als Eingabe dienen, und solchen, die für die Ausgabe bestimmt sind, zu differenzieren. Für unsere folgenden Ausführungen sei P immer ein normales Programm und G ein normales Goal. Die Menge der in P ∪ {G} auftretenden Prädikatszeichen bezeichnen wir mit Σ.

Definition 6.2 (I/O–Spezifikation) Eine I/O–Spezifikation ist eine Abbildung σ : Σ → {+, −}^{∗}, die jedem n– stelligen in P auftretenden Prädikatszeichen p ein Wort der Länge n aus dem Alphabet {+, −} zuordnet. Dabei steht ein +–Zeichen für eine Stelle, die als Eingabe benutzt werden soll, während ein −–Zeichen für eine Stelle steht, die der Ausgabe dient.

Formal ist eine I/O–Spezifikation für ein Prädikatszeichen p also ein Wort aus dem Alphabet {+, −}. Zur Vereinfachung der Schreibweise vereinbaren wir, daß wir Worte als Hintereinanderreihung ihrer Buchstaben schreiben, was ja auch der im täglichen Leben gängigen Praxis entspricht. Ist w ein Wort der Länge n und i ∈ {1, ⋯, n}, so soll (w)_{i} für den i–ten Buchstaben des Wortes w stehen, es gilt also:

w = (w)_{1} ⋯ (w)_{n}.

Eine I/O–Spezifikation ermöglicht es uns, zwischen Eingabevariablen und Ausgabevariablen zu unterscheiden. Wir formalisieren diese Begriffe wie folgt:

Definition 6.3 (FV^{+}(L), FV^{−}(L)) Es sei σ ein I/O–Spezifikation und p∈Σ ein n–stelliges Prädikatszeichen. Ist Q eine Primformel der Gestalt Q = pt_{1} ⋯ t_{n}, so vereinbaren wir:

FV^{+}(Q) := ⋃{FV (t_{i}) : i∈{1, ⋯, n} & (σ(p))_{i} = +}
FV^{−}(Q) := ⋃{FV (t_{i}) : i∈{1, ⋯, n} & (σ(p))_{i} = −}

Ist L ein negatives Literal, so setzen wir

FV^{+}(L) := FV (L) und FV^{−}(L) := ∅.

Die Elemente von FV^{+}(L) bezeichnen wir auch als Eingabevariablen, die Elemente aus FV^{−}(L) heißen Ausgabevariablen.

Hat ein Goal G die Gestalt [Γ] : [], so bezeichnen wir das erste in der Liste Γ auftretende Literal als das “aufgerufene” Literal. Die Idee bei einer konsistenten I/O–Spezifikation (was das ist, definieren wir gleich) besteht darin, sicherzustellen, daß die Eingabevariablen eines “aufgerufenen” Literals immer mit geschlossenen Termen belegt sind. (Dies wird durch die Forderung erreicht, daß alle die Variablen, die in einem Goal an einem Punkt als Eingabevariablen auftreten, bereits vorher als Ausgabevariablen aufgetreten sein müssen.) Da in einem negativen Literal definitionsgemäß alle Variablen als Eingabevariablen gezählt werden, stellt dies später sicher, daß keine Berechnung zu P ∪{G} hängen bleibt. Diesen Gedanken sollte der Leser bei der Lektüre der nun folgenden Definition der Konsistenz einer I/O–Spezifikation im Hinterkopf behalten.

Definition 6.4 (konsistente I/O–Spezifikationen) Es sei P ein normales Programm und G ein normales Goal. σ : Σ → {+, −}^{∗} sei eine I/O–Spezifikation für P ∪ {G} . Eine Programm–Klausel [L_{1}, ⋯, L_{n}]:[Q] aus P heißt σ–erlaubt, falls gilt:

1. x∈FV^{−}(Q) ⇒ x∈FV^{+}(Q) oder ∃j ∈{1, ⋯, n}(x∈FV (L_{j})).

2. x∈FV^{+}(L_{i}) ⇒ x∈FV^{+}(Q) oder ∃j ∈{1, ⋯, i − 1}(x∈FV (L_{j})).

Ein Goal G der Gestalt [L_{1}, ⋯, L_{n}]:[] heißt σ–erlaubt, wenn

x∈FV^{+}(L_{i}) ⇒ ∃j ∈{1, ⋯, i − 1}(x∈FV (L_{j}))

gilt. P ∪ {G} ist σ–konsistent falls gilt:

1. Jede Klausel aus P ist σ–erlaubt.

2. G ist σ–erlaubt.

In diesem Fall sagen wir auch, daß σ eine konsistente I/O–Spezifikation für P ∪ {G} ist. _{□}

Wir werden später des öfteren Gebrauch von der folgenden Beobachtung machen:

(∗) Ist P ∪ {[L_{1}, ⋯, L_{n}]:[]} σ–konsistent , so gilt FV^{+}(L_{1}) = ∅.

Dies zeigt, daß eine Berechnung zu P ∪ {G} unter der Voraussetzung, daß P ∪ {G} σ–konsistent ist, zumindest nicht sofort hängt, denn damit dies der Fall wäre, müßte das aufgerufene Literal L_{1} negativ sein und freie Variablen enthalten. Für ein negatives Literal ist aber FV (L) = FV^{+}(L), und (∗) zeigt, daß FV^{+}(L_{1}) = ∅ ist. Das nächste Lemma zeigt, daß die Eigenschaft von P ∪ {G} , σ–konsistent zu sein, sich bei SLDNF–Herleitungen vererbt.

Lemma 6.5 Es gelte:

1. P ∪ {Γ_{0} :[]} ist σ–konsistent.

2. [Γ_{0} :[], ⋯, Γ_{n} : []] zeigt P ∪ {Γ_{0} :[]} ⊢_{k}^{ϑ_{n}} Γ_{n} : [].

Dann ist auch P ∪ {Γ_{n} : []} σ–konsistent.

Beweis: Wir führen den Beweis durch Induktion nach n. Der Induktionsanfang n = 0 ist offenbar trivial. Im Induktionsschritt von n nach n + 1 ist Γ_{n} ≠ [], und unsere weiteren Überlegungen hängen von der Gestalt des ersten Literals in Γ_{n} ab.

1. Fall: Γ_{n} = [Q_{2}|Δ_{2}].

In diesem Fall gibt es eine Klausel Δ_{1} : [Q_{1}] in P, so daß Q_{1} und Q_{2} unifizierbar sind. Es sei μ := mgu(Q_{1}, Q_{2}). Dann gilt

Γ_{n+1} = (Δ_{1}, Δ_{2})μ und ϑ_{n+1} = ϑ_{n}μ.

Weiter sei

Δ_{1} = [K_{1}, ⋯, K_{m}] und Δ_{2} = [L_{1}, ⋯, L_{k}].

Dann ist Γ_{n+1} = [K_{1}μ, ⋯, K_{m}μ, L_{1}μ, ⋯, L_{k}μ]. Um die σ–Konsistenz von P ∪ {Γ_{n+1} : []} zu zeigen, weisen wir nach, daß Γ_{n+1} : [] σ–erlaubt ist. Zu diesem Zweck zeigen wir:

1. x∈FV^{+}(K_{i}μ) ⇒ ∃j ∈{1, ⋯, i − 1}(x∈FV (K_{j}μ)).

2. x∈FV^{+}(L_{i}μ) ⇒ ∃j ∈{1, ⋯, m}(x∈FV (K_{j}μ)) oder

∃j ∈{1, ⋯, i − 1}(x∈FV (L_{j}μ)).

Sei also x∈FV^{+}(K_{i}μ). Dann gibt es ein y ∈FV^{+}(K_{i}), so daß x∈FV (μ(y)) gilt. Da die Klausel [K_{1}, ⋯, K_{m}]:[Q_{1}] σ–erlaubt ist, gilt:

(1)  y ∈FV^{+}(Q_{1}) oder ∃j ∈{1, ⋯, i − 1}(y ∈FV (K_{j})).

Wir zeigen, daß der erste Fall nicht eintreten kann. Denn aus

Q_{1}μ = Q_{2}μ, y ∈FV^{+}(Q_{1}) und x∈FV (μ(y))

folgt x ∈ FV^{+}(Q_{1}μ) und also auch x ∈ FV^{+}(Q_{2}μ). Dann müßte es ein z ∈ FV^{+}(Q_{2}) mit x ∈ FV (μ(z)) geben. Da nach IV [Q_{2}|Δ_{2}] : [] σ–erlaubt ist, wissen wir nach der im Anschluß an die Definition der konsistenten I/O–Spezifikation gemachten Bemerkung, daß FV^{+}(Q_{2}) = ∅ ist. Dieser Widerspruch zeigt, daß in (1) der zweite Fall eintritt. Folglich gilt

∃j ∈{1, ⋯, i − 1}(y ∈FV (K_{j})).

Daraus folgt x∈FV (K_{j}μ) und wegen j < i ist das die Behauptung.

Wir untersuchen nun den Fall, daß x ∈ FV^{+}(L_{i}μ) ist. Dann gibt es ein y ∈FV^{+}(L_{i}) mit x∈FV (μ(y)). Da das Goal

[Q_{2}, L_{1}, ⋯, L_{k}]:[]

σ–erlaubt ist, gilt

a) y ∈FV (Q_{2}) oder

b) ∃j ∈{1, ⋯, i − 1}(y ∈FV (L_{j})).

Fall a): y ∈FV (Q_{2})

Da FV^{+}(Q_{2}) = ∅ ist, folgt y ∈FV^{−}(Q_{2}). Dann ist x∈FV^{−}(Q_{2}μ) und wegen Q_{1}μ = Q_{2}μ auch x∈FV^{−}(Q_{1}μ). Also gibt es ein z ∈FV^{−}(Q_{1}) mit x∈F V (μ(z)). Da

[K_{1}, ⋯, K_{m}]:[Q_{1}]

σ–erlaubt ist, gilt

(2)  z ∈FV^{+}(Q_{1}) oder ∃j ∈{1, ⋯, m}(z ∈FV (K_{j})).

Der Fall z ∈FV^{+}(Q_{1}) führt zu einem Widerspruch, denn wegen

Q_{1}μ = Q_{2}μ und x∈FV (μ(z))

wäre dann x ∈ FV^{+}(Q_{2}μ) und das kann wegen FV^{+}(Q_{2}) = ∅ nicht sein. Also ist in (2) die zweite Alternative richtig und es gilt z ∈ FV (K_{j}). Daraus folgt x∈(K_{j}μ), und wir sind zufrieden.

Fall b): ∃j ∈{1, ⋯, i − 1}(y ∈FV (L_{j}))

In diesem Fall gilt x ∈ FV (L_{j}μ) für ein j < i, und das wollten wir zeigen.

2. Fall: Γ_{n} = [¬Q_{2}|Δ_{2}] In diesem Fall gibt es einen erfolglosen SLDNF–Baum zu P ∪ {[Q_{2}] : []}, es ist Γ_{n+1} = Δ_{2} und ϑ_{n+1} = ϑ_{n}. Wir zeigen, daß Γ_{n+1} : [] erlaubt ist. Es sei

Δ_{2} = [L_{1}, ⋯, L_{k}].

Ist x∈FV^{+}(L_{i}) für ein i∈{1, ⋯, n}, so folgt aus der Tatsache, daß Γ_{n} : [] σ–erlaubt ist:

x∈FV (¬Q_{2}) oder ∃j ∈{1, ⋯, i − 1}(x∈FV (L_{j})).

Da FV (¬Q_{2}) = ∅ und FV^{+}(¬Q_{2}) = FV (Q_{2}) ist, liegt die zweite Alternative vor, und es gibt ein j ∈{1, ⋯, i − 1} mit x∈FV (L_{j}). _{□}

Das Hauptergebnis dieses Abschnittes folgt nun als Korollar.

Korollar 6.6 Falls P ∪ {G} σ–konsistent ist, bleibt keine Berechnung zu P ∪ {G} hängen.

Beweis: Ist H eine Herleitung, so daß

H zeigt P ∪ {G} ⊢_{k}^{ϑ} Δ:[]

gilt und ist P ∪ {G} σ–konsistent, so folgt aus dem letzten Lemma zunächst die σ–Konsistenz von P ∪ {Δ : []}. Also ist Δ : [] σ–erlaubt und das impliziert insbesondere, daß das erste Literal aus Δ keine Negation einer Primformel ist, die noch freie Variablen enthält. Also kann die Berechnung bei einer Herleitung zu P ∪ {G} nicht hängen bleiben.

Da wir jeden Zweig eines SLDNF–Baumes als SLDNF–Herleitung auffassen können, kann auch die Berechnung eines SLDNF–Baumes zu P ∪ {G} nie hängen bleiben. _{□}

6.3 Geordnete Programme

Ist P ein normales Programm und G ein normales Goal, so kann es passieren, daß eine SLDNF–Herleitung zu P ∪ {G} beliebig oft fortgesetzt werden kann. Ein einfaches Beispiel dafür ist

P = {[p]:[p]} und G = [p]:[].

In diesem Fall sprechen wir von einer unendlichen SLDNF–Berechnung. Wir präzisieren diesen Begriff.

Definition 6.7 (unendliche SLDNF–Berechnung) Eine Folge (H_{n})_{n} von normalen Goals ist eine unendliche SLDNF–Berechnung zu P, falls es für alle n∈N ein k ∈N und eine Substitution ϑ gibt, so daß gilt:

[H_{0}, ⋯, H_{n}] zeigt P ∪ {H_{0}} ⊢_{k}^{ϑ} H_{n}.

Ist (H_{n})_{n} eine unendliche SLDNF–Berechnung zu P, so existiert kein ausgewachsener SLDNF–Baum zu P ∪{H_{0}}. Denn wäre B ein ausgewachsener SLDNF–Baum zu P ∪ {H_{0}}, so müßte B für jedes n∈N einen Zweig enthalten, der die Herleitung [H_{0}, ⋯, H_{n}] enthält. (Vergleiche Lemma (5.11)). Dann würde B aber beliebig lange Zweige besitzen. Das würde der Endlichkeit von B widersprechen.

Wie wir bereits früher angedeutet haben, ist für die Gültigkeit eines Vollständigkeitssatzes für die SLDNF–Resolution die Existenz von ausgewachsenen SLDNF–Bäumen unabdingbar. Es ist daher vernünftig, nach einer Klasse von normalen Programmen zu suchen, für die es keine unendlichen SLDNF–Berechnungen gibt. Zu diesem Zweck definieren wir auf der Menge aller Prädikatszeichen eine Abbildung level : Σ → N. Durch diese Abbildung werden die Prädikatszeichen in Schichten eingeteilt. Für den restlichen Abschnitt fixieren wir diese Abbildung. Wir erweitern die Funktion level auf Literale, indem wir

level(pt_{1} ⋯ t_{n}) := level(p) und level(¬Q) := level(Q)

definieren. Der klassische Ansatz, um die Existenz unendlicher SLDNF–Berechnungen zu vermeiden, besteht darin, nur “hierarchische” Programme zu betrachten.

Definition 6.8 (hierarchische Programme) Ein normales Programm heißt hierarchisch, falls für jede Klausel

[L_{1}, ⋯ L_{n}]:[Q]

aus P gilt:

∀i∈{1, ⋯, n}(level(L_{i}) < level(Q)).

Bedauerlicherweise erlauben hierarchische Programme keinerlei Form von Rekursion. Wir stellen daher ein neues Konzept vor, das den Begriff des hierarchischen Programmes wesentlich verallgemeinert. Vorab müssen wir allerdings noch definieren, was wir unter der Länge eines Terms verstehen. Ist A = (Λ, Σ) unser Alphabet, so ordnen wir zunächst einmal jedem Funktionszeichen f ∈Λ eine positive Zahl weight(f) zu, die wir als das Gewicht von f bezeichnen:

weight : Λ → N −{0}.

Nun können wir festlegen, was wir unter der Länge eines Terms t verstehen wollen:

Definition 6.9 (Länge eines Termes) Ist t ein Term, so definieren wir die Länge von t (geschrieben ln(t)) induktiv durch:

I.A.: t = x∈V. In diesem Fall setzen wir

ln(t) := 0.

I.S.: t = ft_{1} ⋯ t_{n}. Wir definieren:

ln(t) := weight(f) + ∑_{i=1}^{n} ln(t_{i}).

Bei Literalen müssen wir zwischen Termen, die als Eingabe oder Ausgabe gedacht sind, unterscheiden. Wir fixieren daher für das folgende eine I/O– Spezifikation σ. Ist Q = pt_{1} ⋯ t_{n} eine Primformel und ist

I := {i∈{1, ⋯, n} : (σ(p))_{i} = +},

so definieren wir

ln^{+}(Q) := ∑_{i∈I} ln(t_{i}).

Für negative Literale der Form L = ¬pt_{1} ⋯ t_{n} setzen wir

ln^{+}(L) := ∑_{i=1}^{n} ln(t_{i}) + 1.

(Daß wir hier noch eine 1 zuzählen geschieht aus Gründen, die erst im nächsten Kapitel klar werden.) Damit haben wir alles Material zusammen, um das Konzept des geordneten Programmes einführen zu können.

Definition 6.10 (geordnete Programme) Ist P ein normales Programm zur I/O–Spezifikation σ, so ist P durch die Funktion level bezüglich σ geordnet, falls für jede Klausel

[L_{1}, ⋯, L_{n}]:[Q]

aus P gilt:

1. ∀i∈{1, ⋯, n}(level(L_{i}) ≤ level(Q)).

2. Ist die Menge I := {i ∈ {1, ⋯, n} : level(L_{i}) = level(Q)} nicht leer, so gilt:

∑_{i∈I}(1 + ln^{+}(L_{i})) < 1 + ln^{+}(Q) und ⋃_{i∈I} FV^{+}(L_{i}) ⊆_{multi} FV^{+}(Q).

In der obigen Definition bedeutet die Schreibweise

⋃_{i∈I} FV^{+}(L_{i}) ⊆_{multi} FV^{+}(Q),

daß wir ⋃_{i∈I} FV^{+}(L_{i}) und FV^{+}(Q) als Multimengen auffassen. Bemerkung: Reden wir im folgenden von einem geordneten Programm, so meinen wir damit immer ein bezüglich einer I/O–Spezifikation σ geordnetes Programm. Die Angabe von σ unterdrücken wir, wenn aus dem Kontext klar hervorgeht, durch welche I/O–Spezifikation σ das betrachtete Programm geordnet wird.

Die Teilmengenbeziehung ⋃_{i∈I} FV^{+}(L_{i}) ⊆_{multi} FV^{+}(Q) in der Definition der geordneten Programme garantiert uns, daß die Eigenschaft

∑_{i∈I}(1 + ln^{+}(L_{i})) < 1 + ln^{+}(Q)

unter Substitutionen stabil ist. Daß dies so ist, zeigt das nächste Lemma:

Lemma 6.11 (Stabilitätseigenschaft von ln^{+})

Vor.: ∑_{i∈I}(1 + ln^{+}(L_{i})) < 1 + ln^{+}(Q) und ⋃_{i∈I} FV^{+}(L_{i}) ⊆_{multi} FV^{+}(Q).

Beh.: Für jede Substitution τ gilt:

∑_{i∈I}(1 + ln^{+}(L_{i}τ)) < 1 + ln^{+}(Qτ).

Beweis: Zunächst machen wir uns klar, daß wir ohne Einschränkung davon ausgehen können, daß die zugrundeliegende I/O–Spezifikation σ für alle unsere Prädikatszeichen nur aus “+”–Zeichen besteht, denn sowohl zu ln^{+}(pt_{1} ⋯ t_{n}) als auch zu FV^{+}(pt_{1} ⋯ t_{n}) würde ein Term t_{i} mit (σ(p))_{i} = − keinen Beitrag liefern. Nachdem wir diese zusätzliche Voraussetzung über die I/O–Spezifikation gemacht haben, brauchen wir im folgenden nicht mehr zwischen ln(L) und ln^{+}(L) und FV (L) bzw. FV^{+}(L) zu unterscheiden.

Weiter bemerken wir, daß wir Primformeln und Literale auch als Terme aus einem erweiterten Alphabet auffassen können. Ist das ursprüngliche Alphabet A = (Λ, Σ), so sind Literale, die aus diesem Alphabet gebildet worden sind, gleichzeitig auch Terme aus dem erweiterten Alphabet Â := (Λ ∪ Σ ∪ {¬}, ∅). Für die beiden Funktionen ln und FV ist es offenbar gleichgültig, ob wir ihre Argumente als Terme oder Literale interpretieren. Daher genügt es, die folgende Variante der Behauptung zu beweisen:

(1)  ln(s) < ln(t) & FV (s) ⊆_{multi} FV (t) ⇒ ln(sτ) < ln(tτ)

Um (1) einzusehen, bemerken wir zunächst, daß

(2)  ln(sτ) = ln(s) + ∑_{x∈FV (s)} ln(τ(x))

gilt, falls wir FV (s) wieder als Multimenge auffassen. Da wir für Variablen x die Definition der Länge durch ln(x) = 0 vorgenommen haben, kann (2) kann durch eine triviale Induktion nach dem Aufbau von s nachgewiesen werden. Weiter stellen wir fest, daß FV (s) ⊆_{multi} FV (t) die Gültigkeit von

(3)  ∑_{x∈FV (s)} ln(τ(x)) ≤ ∑_{x∈FV (t)} ln(τ(x))

impliziert. Aus (2) und (3) folgt nun (1). _{□}

Es ist unmittelbar klar, daß geordnete Programme eine Verallgemeinerung der hierarchischen Programme sind. Wir werden später sehen, daß sich zumindest alle primitiv–rekursiven Funktionen durch geordnete Programme berechnen lassen. Entscheidend ist aber, daß zu geordneten Programmen keine unendlichen SLDNF– Berechnungen existieren. Genauer gilt:

Lemma 6.12 (Endlichkeits–Lemma) Es gelte

1. P ∪ {G} ist σ–konsistent.

2. P ist geordnet bezüglich σ.

Dann gibt es keine unendliche SLDNF–Berechnung (H_{n})_{n} zu P, so daß H_{0} = G ist.

Beweis: Wir werden den Beweis indirekt führen und annehmen, daß es eine Folge (H_{n})_{n} gibt, so daß es für alle n ∈ N ein k ∈ N und eine Substitution ϑ gibt, so daß gilt:

(1)  [H_{0}, ⋯, H_{n}] zeigt P ∪ {H_{0}} ⊢_{k}^{ϑ} H_{n}.

Die Idee des Beweises besteht darin, jedem Goal H_{n} eine Ordinalzahl o(H_{n}) zuzuordnen, so daß für alle n∈N

(2)  o(H_{n+1}) < o(H_{n})

gilt. Dann wäre (o(H_{n}))_{n∈N} eine unendliche absteigende Folge von Ordinalzahlen, was der Wohlordnungseigenschaft von Ordinalzahlen widerspricht. Es bleibt also nur o(H_{n}) zu definieren, und mit dieser Definition (2) nachzuweisen.

Zu diesem Zweck definieren wir vorab eine Variante der Funktion ln^{+}:

\underline{ln}^{+}(L) := \{ \begin{matrix}ln^{+}(L) & falls FV^{+}(L) = ∅; \\ ω & sonst. \end{matrix}

Nun können wir jedem Goal G eine Ordinalzahl o(G) zuordnen. Wir definieren:

o([L_{1}, ⋯, L_{n}]:[]) := #_{i=1}^{n} ω^{2∗level(L_{i})} ∗ (1 + \underline{ln}^{+}(L_{i})).

Dabei steht # für die natürliche Summe von Ordinalzahlen. (Eine Darstellung der für unsere Zwecke benötigten Theorie der Ordinalzahlen findet sich beispielsweise in den Kapiteln 6—8 von Pohlers [Poh89].)

Mit der obigen Definition von o(G) läßt sich (2) zeigen. Hat H_{n} die Form Γ_{n} : [], so hängen unsere weiteren Überlegungen von der Gestalt des ersten Literals in Γ_{n} ab.

1. Fall: Γ_{n} = [Q_{2}|Δ_{2}] In diesem Fall gibt es eine Klausel

[K_{1}, ⋯, K_{m}]:[Q_{1}]

in P, so daß Q_{1} und Q_{2} mit μ als MGU unifizierbar sind. Hat Δ_{2} die Form Δ_{2} = [L_{1}, ⋯, L_{r}], so gilt:

Γ_{n+1} = [K_{1}μ, ⋯, K_{m}μ, L_{1}μ, ⋯, L_{r}μ].

Um die Schreibweise nicht zu unübersichtlich werden zu lassen, führen wir einige Abkürzungen ein:

k_{i} := level(K_{i}) für alle i∈{1, ⋯, m},
l_{i} := level(L_{i}) für alle i∈{1, ⋯, r}.

Weiter sei q = level(Q_{2}). Dann gilt:

o(H_{n}) = ω^{2q} ∗ (1 + \underline{ln}^{+}(Q_{2})) # #_{i=1}^{r} ω^{2l_{i}} ∗ (1 + \underline{ln}^{+}(L_{i})) und

o(H_{n+1}) = #_{i=1}^{m} ω^{2k_{i}} ∗ (1 + \underline{ln}^{+}(K_{i}μ)) # #_{i=1}^{r} ω^{2l_{i}} ∗ (1 + \underline{ln}^{+}(L_{i}μ)).

Zunächst ist klar, daß \underline{ln} + (L_{i}μ) ≤ \underline{ln}^{+}(L_{i}) ist, denn falls L_{i} positiv geschlossen ist (mit dieser Redeweise drücken wir FV^{+}(L_{i}) = ∅ aus), so verändert die Substitution μ nichts mehr an den Termen, die als Eingabe auftreten. Falls FV^{+}(L_{i}) ≠ ∅ ist, so ist \underline{ln}^{+}(L_{i}) = ω und das ist ohnehin der größte Wert, den die Funktion \underline{ln}^{+} annehmen kann. Daher gilt:

#_{i=1}^{r} ω^{2l_{i}} ∗ (1 + \underline{ln}^{+}(L_{i}μ)) ≤ #_{i=1}^{r} ω^{2l_{i}} ∗ (1 + \underline{ln}^{+}(L_{i})).

Aus dieser Ungleichung folgt (2), falls wir noch

(3)  #_{i=1}^{m} ω^{2k_{i}} ∗ (1 + \underline{ln}^{+}(K_{i}μ)) < ω^{2q} ∗ (1 + \underline{ln}^{+}(Q_{2}))

zeigen können. Wenn alle k_{i} < q sind, so ist (3) ohnehin klar, denn dann treten auf der linken Seite von (3) nur Potenzen von ω mit einem Exponenten ≤ 2q − 1 auf. Wir nehmen daher an, daß die Menge

I := {i∈{1, ⋯, r} : level(K_{i}) = level(Q_{1})}

nicht leer ist. In diesem Fall folgt aus der zweiten Voraussetzung, daß

(4) ∑_{i∈I}(1+ln^{+}(K_{i})) < 1+ln^{+}(Q_{1}) und ⋃_{i∈I} FV^{+}(K_{i}) ⊆_{multi} FV^{+}(Q_{1})

gilt. Nach Lemma (6.5) wissen wir, daß P ∪ {H_{n}} σ–konsistent ist. Also gilt FV^{+}(Q_{2}) = ∅, woran auch die Substitution μ nichts ändert, so daß FV^{+}(Q_{2}μ) = ∅ folgt. Wegen Q_{1}μ = Q_{2}μ folgt daraus auch FV^{+}(Q_{1}μ) = ∅. Zusammen mit (4) folgt, daß

FV^{+}(K_{i}μ) = ∅ für alle i∈I

gilt. Daher besteht für die i ∈ I zwischen ln^{+}(K_{i}μ) und \underline{ln}^{+}(K_{i}μ) kein Unterschied, und mit Lemma (6.11) folgt aus (4), daß

∑_{i∈I}(1 + \underline{ln}^{+}(K_{i}μ)) < 1 + \underline{ln}^{+}(Q_{1}μ) = 1 + \underline{ln}^{+}(Q_{2}μ)

ist. Wegen FV^{+}(Q_{2}) = ∅ ist \underline{ln}^{+}(Q_{2}) = \underline{ln}^{+}(Q_{2}μ), und zusammen mit der letzten Ungleichung impliziert das

∑_{i∈I}(1 + \underline{ln}^{+}(K_{i}μ)) < 1 + \underline{ln}^{+}(Q_{2}).

Auf der rechten Seite der Ungleichung (3) stehen mehr Terme der Form ω^{2q}, und zwar 1 + ln^{+}(Q_{2}), als auf der linken Seite, wo nur ∑_{i∈I}(1 + ln^{+}(K_{i}μ)) Terme von dieser Art zu finden sind. Da ω^{2q} eine Hauptzahl ist, folgt (3) und also auch (2).

2. Fall: Γ_{n} = [¬Q_{2}|Δ_{2}] In diesem Fall ist Γ_{n+1} = Δ_{2}. Definieren wir q := level(Q_{2}), so sehen wir sofort, daß

o(H_{n}) = o(H_{n+1}) # ω^{2q} ∗ (1 + \underline{ln}^{+}(¬Q_{2}))

gilt. Daraus folgt (2) und damit die Behauptung. _{□}

6.4 Adäquatheit konsistent geordneter Programme

In diesem Abschnitt zeigen wir, daß sich die primitiv–rekursiven Funktionen durch konsistent geordnete Programme berechnen lassen. Dabei nennen wir ein Programm P konsistent geordnet, falls gilt:

1. Es gibt eine I/O–Spezifikation σ, so daß alle Klauseln aus P σ–erlaubt sind.

2. P ist geordnet bezüglich σ.

Eigentlich sollten wir ein konsistent geordnetes Programm P besser als Tripel (P, σ, level) schreiben, da ja die Angabe von P alleine nicht ausreicht, um sagen zu können, daß P konsistent geordnet ist. Wenn wir im folgenden von einem konsistent geordneten Programm P sprechen, werden wir σ und level immer stillschweigend als gegeben annehmen.

Das formale Gegenstück zu den natürlichen Zahlen sind Ziffern. Wir definieren Ziffern als die geschlossenen Terme, die sich aus der Konstanten 0 und dem einstelligen Funktionszeichen S bilden lassen. Ist n∈N, so soll in Zukunft \underline{n} als Abkürzung für die Ziffer

\underbrace{S ⋯ S}_{n–mal} 0

dienen. Mit dieser Schreibweise lautet das Hauptergebnis dieses Abschnittes:

Theorem 6.13 (Adäquatheits–Theorem) Es sei f : N^{n} → N eine primitiv–rekursive Funktion. Dann gibt es ein konsistent geordnetes Programm P_{f} sowie ein n + 1–stelliges Prädikatszeichen p_{f} ∈ Σ aus dem Alphabet A = (Λ, Σ) von P_{f}, so daß gilt:

1. Für alle k_{1}, ⋯, k_{n} ∈ N ist [p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, x)]:[] σ–erlaubt.

2. Für alle k_{1}, ⋯, k_{n} ∈ N gilt:

P_{f} ∪ \{[p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, x)]:[]\} ⊢_{ω}^{ϑ} □ ⇒ ϑ(x) = \underline{f(k_{1}, ⋯, k_{n})}.

3. Für alle k_{1}, ⋯, k_{n} ∈ N gibt es eine Substitution ϑ mit

ϑ(x) = \underline{f(k_{1}, ⋯, k_{n})} & P_{f} ∪ \{[p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, x)]:[]\} ⊢_{ω}^{ϑ} □.

Bemerkung: Der zweite Punkt aus der Behauptung des Adäquatheits–Theorems stellt eine Korrektheitsaussage dar, der dritte Punkt beschreibt eine Art Vollständigkeit.

Beweis des Adäquatheits–Theorems: Wir beweisen das Theorem durch eine Induktion nach dem Aufbau von f. Da in [Llo87] eine ähnliche Aussage bewiesen wird, können wir uns darauf beschränken zu zeigen, daß es eine Abbildung level : Σ → N und eine I/O–Spezifikation σ gibt, so daß gilt:

1. P_{f} ist geordnet bezüglich σ.

2. P_{f} ∪ {G} ist σ–konsistent.

Der Rest der Behauptung folgt dann aus [Llo87], denn das dort konstruierte Programm P_{f}, ist mit dem P_{f}, das wir konstruieren werden, identisch. Außerdem unterscheidet sich die von uns bewiesene Version des Adäquatheitssatzes von dem in der Literatur zu findendem Ergebnis nur durch die zusätzliche Forderung, daß P_{f} konsistent geordnet ist.

Bevor wir mit dem Beweis beginnen, müssen wir noch die Funktion weight festlegen. Da S das einzige Funktionszeichen ist, was in dem Programmen, die wir gleich konstruieren werden, auftritt, reicht es aus,

weight(S) := 1

zu definieren. Wir konstruieren nun P_{f}:

1. Fall: f = Z.

(Dabei ist Z : N → N definiert durch Z(n) = 0 für alle n∈N.) In diesem Fall besteht P_{f} nur aus der Klausel

[]:[p_{f}(x, \underline{0})].

Wir definieren level(p_{f}) := 0 und setzen σ(p_{f}) := +−. Offenbar ist P_{f} damit konsistent geordnet. Außerdem ist klar, daß

[p_{f}(\underline{k}, x)]:[]

für alle k ∈N σ–erlaubt ist.

2. Fall: f = S.

(Dabei ist S : N → N definiert durch S(n) = n + 1 für alle n ∈ N.) In diesem Fall besteht P_{f} aus der Klausel

[]:[p_{f}(x, Sx)].

Wir definieren level(p_{f}) := 0 und setzen σ(p_{f}) := +−. Offenbar ist P_{f} damit konsistent geordnet. Außerdem ist klar, daß

[p_{f}(\underline{k}, x)]:[]

für alle k ∈N σ–erlaubt ist.

3. Fall: f = U_{i}^{n}.

(Dabei ist U_{i}^{n} : N → N definiert durch U(k_{1}, ⋯, k_{n}) = k_{i} für alle k_{1}, ⋯, k_{n} ∈N.) In diesem Fall besteht P_{f} aus der Klausel

[]:[p_{f}(x_{1}, ⋯, x_{n}, x_{i})].

Wir definieren level(p_{f}) := 0 und setzen σ(p_{f}) := + ⋯ + −. Offenbar ist P_{f} damit konsistent geordnet. Außerdem ist klar, daß

[p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, x)]:[]

für alle k_{1}, ⋯, k_{n} ∈ N σ–erlaubt ist.

4. Fall: f = h ∘ (g_{1}, ⋯, g_{r}). (Dabei ist h ∘ (g_{1}, ⋯, g_{r}) : N^{n} → N definiert durch

h ∘ (g_{1}, ⋯, g_{r})(k_{1}, ⋯, k_{n}) := h(g_{1}(k_{1}, ⋯, k_{n}), ⋯, g_{r}(k_{1}, ⋯, k_{n})),

falls h r–stellig ist und g_{1}, ⋯, g_{r} n–stellig sind.) Nach IV gibt es Programme P_{g_{1}}, ⋯, P_{g_{r}} und P_{h}, die σ–konsistent und geordnet sind und die die Funktionen g_{1}, ⋯, g_{r} und h im Sinne dieses Theorems berechnen. Wir definieren P_{f} als

P_{f} := P_{g_{1}} ∪ ⋯ ∪ P_{g_{r}} ∪ P_{h} ∪ {Γ:Δ},

wobei wir Γ und Δ durch

Γ := [p_{g_{1}}(x_{1}, ⋯, x_{n}, y_{1}), ⋯, p_{g_{r}}(x_{1}, ⋯, x_{n}, y_{r}), p_{h}(y_{1}, ⋯, y_{r}, y)]

und Δ := [p_{f}(x_{1}, ⋯, x_{n}, y)]

definieren. Ist d der höchste in P_{g_{1}}, ⋯ P_{g_{r}} oder P_{h} auftretende Funktionswert der Funktion level, so setzen wir level(p_{f}) := d + 1. Die I/0–Spezifikation definieren wir durch

σ(p_{f}) := \underbrace{+ ⋯ +}_{n} −.

Nun folgt unmittelbar aus den Definitionen, daß P_{f} konsistent geordnet ist und daß

[p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, x)]:[]

für alle k_{1}, ⋯, k_{n} ∈ N σ–erlaubt ist.

5. Fall: f = Rgh.

(Dabei ist Rgh : N^{n} + 1 → N unter der Voraussetzung, daß g n–stellig und h n + 2–stellig ist, durch die beiden Gleichungen

Rgh(k_{1}, ⋯ k_{n}, 0) = g(k_{1}, ⋯, k_{n}) und

Rgh(k_{1}, ⋯ k_{n}, k_{n+1} + 1) = h(k_{1}, ⋯, k_{n}, k_{n+1}, Rgh(k_{1}, ⋯, k_{n}, k_{n+1}))

definiert.) Nach IV gibt es geordnete σ–konsistente Programm P_{g} und P_{h}, die die Funktion g bzw. h berechnen. Es sei d der höchste in P_{g} oder P_{h} auftretende Funktionswert der Funktion level. Wir definieren P_{f} durch

P_{f} := P_{g} ∪ P_{h} ∪ {Γ_{1} :Δ_{1}, Γ_{2} :Δ_{2}}.

Dabei sind Γ_{1}, Γ_{2}, Δ_{1} und Δ_{2} durch

Γ_{1} := [p_{g}(x_{1}, ⋯, x_{n}, y)], Δ_{1} := [p_{f}(x_{1}, ⋯, x_{n}, 0, y)],
Γ_{2} := [p_{f}(x_{1}, ⋯, x_{n}, x_{n+1}, z), p_{h}(x_{1}, ⋯, x_{n}, x_{n+1}, z, y)] und

Δ_{2} := [p_{f}(x_{1}, ⋯, x_{n}, s(x_{n+1}), y)]

definiert. Weiter setzen wir

level(p_{f}) := d + 1 und σ(p_{f}) := \underbrace{+ ⋯ +}_{n+1} −.

Wie in den anderen Fällen ist es auch hier leicht zu sehen, daß P_{f} mit diesen Definitionen σ–konsistent und geordnet ist. Dazu ist lediglich nachzurechnen, daß

ln^{+}([p_{f}(x_{1}, ⋯, x_{n}, s(x_{n+1}), y)]) = 1,
ln^{+}([p_{f}(x_{1}, ⋯, x_{n}, x_{n+1}, z)]) = 0,
FV^{+}([p_{f}(x_{1}, ⋯, x_{n}, s(x_{n+1}), y)]) = {x_{1}, ⋯, x_{n+1}} und
FV^{+}([p_{f}(x_{1}, ⋯, x_{n}, x_{n+1}, z)]) = {x_{1}, ⋯, x_{n+1}}

gilt, wobei wir in den letzten beiden Gleichungen FV^{+}(⋯) auch als Multimenge auffassen können. Außerdem ist klar, daß

[p_{f}(\underline{k_{1}}, ⋯, \underline{k_{n}}, \underline{k_{n+1}}, x)]:[]

für alle k_{1}, ⋯, k_{n+1} ∈ N σ–erlaubt ist. _{□}

Vollständigkeit der SLDNF–Resolution

In diesem Kapitel beweisen wir verschiedene Vollständigkeitssätze für die SLDNF–Resolution. Wir setzen dabei immer voraus, daß die normalen Programme P, die wir betrachten, konsistent geordnet sind. Im ersten Abschnitt leiten wir ein rein syntaktisches Ergebnis her. Wir werden sehen, daß unter den eben genannten Bedingungen für P für jedes geschlossene atomare Goal der Form [Q]:[]

P ∪ {[Q]:[]} ⊢_{ω} □ oder P ∪ {[¬Q]:[]} ⊢_{ω} □

gilt. Dieses Ergebnis wird später der Grundstein für die Ableitung weiterer Vollständigkeitssätze sein.

Im zweiten Abschnitt führen wir den auf Clark [Cl78] zurückgehenden Begriff der Vervollständigung eines normales Programmes ein. Damit haben wir durch das Konzept der korrekten Antwort eine deklarative Semantik für die SLDNF– Resolution gefunden, die sich als ein adäquates Gegenstück zu der mit dem Begriff der berechneten Antwort eingeführten operativen Semantik herausstellen wird. In dieser Richtung zitieren wir im zweiten Abschnitt einen Korrektheitssatz für die SLDNF–Resolution, der uns zeigt, daß die mit der SLDNF–Resolution berechneten Antworten bezüglich der Vervollständigung des Programmes auch korrekt sind.

Im dritten Abschnitt wenden wir uns der Umkehrung der letzten Aussage zu und zeigen, daß sich bei der von uns untersuchten Klasse von normalen Programmen jede korrekte Antwort als Instanz einer berechneten Antwort wiederfinden läßt. Damit erhalten wir eine Vollständigkeitsaussage für eine Teilklasse der normalen Programme, die, wie wir im letzten Kapitel mit dem Adäquatheitssatz (Theorem 6.13) zeigen konnten, bereits in der Lage ist, die primitiv–rekursiven Funktionen zu berechnen. Damit ist sie erheblich leistungsfähiger, als die Klasse der erlaubten hierarchischen Programme, auf die sich bisher die Vollständigkeitssätze beschränkten.

Der im dritten Abschnitt bewiesene Vollständigkeitssatz enthält noch eine Lücke. Er setzt die Konsistenz der Vervollständigung von P voraus. Wir zeigen im vierten Abschnitt, daß die Konsistenz der Vervollständigung von P bereits aus den beiden ersten Voraussetzungen des Vollständigkeitssatzes für die SLDNF– Resolution folgt. Wir zeigen also, daß für ein konsistent geordnetes Programm P die Vervollständigung von P konsistent ist. Dieses Ergebnis ist auch für sich allein interessant, da es zeigt, daß konsistent geordnete Programme auch mit der NF–Regel widerspruchsfrei sind.

In diesem Kapitel steht P immer für ein normales Programm, G für ein normales Goal und K und L (evt. mit Indizes) stehen für Literale. Primformeln bezeichnen wir mit Q.

7.1 Syntaktische Vollständigkeit der SLDNF–Resolution

Ist P ein konsistent geordnetes Programm, so können wir zeigen, daß zu jedem Goal G, für das P ∪ {G} σ–konsistent ist, ein ausgewachsener SLDNF–Baum existiert. Daraus erhalten wir später einen Vollständigkeitssatz. Um ein solches Ergebnis zeigen zu können, müssen wir neue ausgewachsene Bäume aus schon konstruierten ausgewachsenen Bäumen zusammenbauen. Diese Konstruktion kann nicht entsprechend der induktiven Definition der SLDNF–Bäume geführt werden, denn an den Blättern kann ein ausgewachsener Baum nicht mehr erweitert werden. Das dies so ist, war ja gerade die Definition des Attributes “ausgewachsen”.

Es gibt aber einen anderen Weg, um aus ausgewachsenen Bäumen neue ausgewachsene Bäume zu konstruieren. Dieser Weg besteht darin, ausgewachsene Bäume auf die Blätter eines noch nicht ausgewachsenen Baumes aufzupfropfen. Im einfachsten Fall wählt man dafür einen Baum, der nur aus einer Wurzel besteht. Je nach dem Vorzeichen des aufgerufenen Literals in dieser Wurzel sind zwei Fälle zu unterscheiden:

1. Ist [Q|Δ] : [] ein normales Goal und gibt es für jede Klausel Γ_{i} : [Q_{i}] aus P, für die Q und Q_{i} durch den MGU μ_{i} unifizierbar sind, einen ausgewachsenen SLDNF–Baum B_{i} zu P ∪ {Γ_{i}μ_{i}, Δμ_{i}: []}, so können wir daraus einen ausgewachsenen SLDNF–Baum für P ∪{[Q|Δ]:[]} konstruieren, indem wir alle Bäume B_{i} auf die gemeinsame Wurzel [Q|Δ]:[] aufpfropfen. Die zu B_{i} führende Kante markieren wir mit μ_{i}. Sind die Bäume B_{i} mit i = 1 bis i = n indiziert, so ergibt sich folgendes Bild:

[figure: [Q|Δ]:[]; μ_{1}; μ_{i}; μ_{n}; B_{1}; ⋯; B_{i}; ⋯; B_{n}]

2. Es sei [¬Q|Δ]:[] ein normales Goal, so daß gilt:

(a) Zu P ∪ {[Q]:[]} gibt es einen erfolglosen SLDNF–Baum.

(b) Zu P ∪ {Δ:[]} gibt es einen ausgewachsenen SLDNF–Baum B.

Dann können wir einen ausgewachsenen SLDNF–Baum zu P ∪{[¬Q|Δ]:[]} konstruieren, indem wir von [¬Q|Δ] : [] eine mit id markierte Kante zur Wurzel von B ziehen:

[¬Q|Δ]:[] id B

Anschaulich sollte klar sein, daß bei der oben beschriebenen Konstruktion wieder ausgewachsene SLDNF–Bäume entstehen. Wollten wir einen exakten Beweis führen, so würden wir zunächst überall das Attribut “ausgewachsen” streichen und die dann erhaltene Aussage durch eine Induktion nach dem Aufbau der Bäume B_{i} bzw. B beweisen. Abschließend würden wir uns überlegen, daß die so konstruierten Bäume ausgewachsen sind, falls nur die Bäume B_{i} bzw. B diese Eigenschaft haben. Mit den oben ausgeführten Gedanken im Hinterkopf beweisen wir das nächste Lemma:

Lemma 7.1

Vor.: 1. P ∪ {G} ist σ–konsistent.

2. P ist geordnet bezüglich σ.

Beh.: Es existiert ein ausgewachsener SLDNF–Baum zu P ∪ {G} .

Beweis: Zunächst ordnen wir jedem Goal G eine Ordinalzahl o(G) zu:

(∗)  o([L_{1}, ⋯, L_{n}]:[]) := #_{i=1}^{n} ω^{2∗level(L_{i})} ∗ (1 + \underline{ln}^{+}(L_{i})).

Damit ist o(G) genauso definiert wie beim Beweis des Endlichkeits–Lemmas (6.12) im letzten Kapitel. Wie dort führen wir den Rest des Beweises durch transfinite Induktion nach o(G).

Im Induktionsanfang gilt o(G) = 0. Ein kurzer Blick auf die Definition (∗) von o(G) zeigt, daß dann G = [] : [] gilt. Der gesuchte ausgewachsene SLDNF– Baum zu P ∪ {G} besteht einfach aus der mit G markierten Wurzel.

Im Induktionsschritt führen wir eine Fallunterscheidung abhängig davon durch, ob das aufgerufene Literal in G positiv oder negativ ist.

1. Fall: G = [Q|Δ]:[].

Ist Γ_{i}: [Q_{i}] eine Klausel aus P, deren Kopf Q_{i} mit Q unifizierbar ist und ist μ_{i} = mgu(Q, Q_{i}), so zeigt die selbe Argumentation wie beim Beweis von (6.12), daß

o(Γ_{i}μ_{i}, Δμ_{i}:[]) < o(G)

gilt. Ähnlich wie beim Beweis von Lemma (6.5) überzeugen wir uns davon, daß aus der σ–Konsistenz von P ∪ {G} auch die σ–Konsistenz von P ∪ {Γ_{i}μ_{i}, Δμ_{i} : []} folgt. Dann existiert nach IV ein ausgewachsener SLDNF–Baum B_{i} zu P ∪ {Γ_{i}μ_{i}, Δμ_{i} : []}. Da dies für jede Klausel aus P gilt, deren Kopf mit Q unifizierbar ist, können wir mit dem vorab skizzierten Verfahren einen ausgewachsenen SLDNF–Baum B zu P ∪ {G} konstruieren, indem wir die Bäume B_{i} auf die gemeinsame Wurzel [Q|Δ]:[] aufpfropfen.

2. Fall: G = [¬Q|Δ]:[].

Wir betrachten das Goal [Q]:[]. Es gilt

o([¬Q|Δ]:[]) ≥ o([¬Q]:[]) > o([Q]:[]).

Die Gültigkeit der Ungleichung o([¬Q] : []) > o([Q] : []) folgt dabei aus unserer Definition der Funktion ln^{+} für negative Literale. Wir hatten

ln^{+}(¬pt_{1} ⋯ t_{n}) := ∑_{i=1}^{n} ln(t_{i}) + 1

gesetzt, und daraus folgt zusammen mit (∗) die benötigte Ungleichung, denn da Q geschlossen ist, gilt für Q = pt_{1} ⋯ t_{n}:

\underline{ln}^{+}(pt_{1} ⋯ t_{n}) ≤ ∑_{i=1}^{n} ln(t_{i}).

(Q ist geschlossen, weil P ∪ {G} σ–konsistent ist.) Außerdem folgt aus der Geschlossenheit von Q, daß auch P ∪ {[Q]:[]} σ–konsistent ist. Nach IV gibt es also einen ausgewachsenen SLDNF–Baum B zu P ∪ {[Q] : []}. Es können zwei Fälle auftreten:

a) B ist erfolglos.

Es ist klar, daß o(Δ : []) < o(G) ist. Da auch P ∪ {Δ : []} σ– konsistent ist, zeigt die IV, daß es einen ausgewachsenen SLDNF– Baum B̂ zu P ∪ {Δ : []} gibt. Mit der vor Beginn dieses Lemmas gemachten Bemerkung können wir daraus einen SLDNF–Baum für P ∪{[¬Q|Δ]:[]} konstruieren, indem wir den Baum B̂ auf die Wurzel [¬Q|Δ]:[] aufpfropfen.

b) B ist erfolgreich.

In diesem Fall ist bereits der Baum, der nur aus der mit dem Goal [¬Q|Δ] : [] markierten Wurzel besteht, ausgewachsen. Denn wenn B erfolgreich ist, so enthält B einen Zweig, den wir als SLDNF– Widerlegung von P ∪ {[Q] : []} interpretieren können. (Vergleiche hierzu Lemma (5.10).) Nach Definition ist dann der oben konstruierte Baum ausgewachsen.

Wir haben nun alle Resultate zusammen, um einen ersten Vollständigkeitssatz zeigen zu können.

Theorem 7.2 (Syntaktischer Vollständigkeitssatz) Es sei P ein normales Programm und Q ein geschlossenes Atom, so daß gilt:

1. P ist geordnet bezüglich σ.

2. P ∪ {[Q]:[]} ist σ–konsistent.

Dann gilt:

P ∪ {[Q]:[]} ⊢_{ω} □ oder P ∪ {[¬Q]:[]} ⊢_{ω} □.

Beweis: Nach dem soeben bewiesenen Lemma wissen wir, daß zu P ∪ {[Q] : []} ein ausgewachsener SLDNF–Baum B existiert. Falls dieser Baum erfolgreich ist, enthält B einen Zweig, dessen Blatt mit □ markiert ist. Nach Lemma (5.10) gibt es dann eine SLDNF–Widerlegung zu P ∪ {[Q]:[]} und folglich gilt

P ∪ {[Q]:[]} ⊢_{ω} □.

Ist B erfolglos, so folgt nach Definition der SLDNF–Herleitung

[[¬Q]:[], []:[]] zeigt P ∪ {[¬Q]:[]} ⊢_{ω} □

und das ist die Behauptung. _{□}

Bemerkung: Die in Kapitel 6 mit Theorem (5.12) bewiesene Widerspruchsfreiheit der SLDNF–Resolution garantiert uns, daß wir das “oder” in der Behauptung des syntaktischen Vollständigkeitssatzes exklusiv interpretieren können.

7.2 Die Vervollständigung eines normalen Programmes

In diesem Abschnitt entwickeln wir ein semantisches Gegenstück zur SLDNF– Resolution. Es handelt sich dabei um den von Clark [Cl78] eingeführten Begriff der Vervollständigung eines normalen Programmes. Mit diesem Begriff konstruieren wir eine Interpretation eines normalen Programmes, die der CWA gerecht wird. Während wir bisher eine Klausel [L_{1}, ⋯, L_{n}]:[Q] aus einem normalen Programm P als eine andere Schreibweise für die Formel

L_{1} ∧ ⋯ ∧ L_{n} → Q

aufgefaßt haben, werden wir den Klauseln aus P nun eine prädikatenlogische Formel zuordnen, die der CWA näher kommt. Die Grundidee bei der CWA besteht darin anzunehmen, daß nur das wahr ist, was aus P gefolgert werden kann. Um diesen Gedanken zu erläutern, betrachten wir zunächst ein einfaches, aussagenlogisches Beispiel. Das Programm P enthalte die beiden Klauseln

(∗)  [q_{1}]:[p] und [q_{2}]:[p]

(Dabei sind q_{1}, q_{2} und p 0–stelllige Prädikatszeichen.) Falls P keine weiteren Klauseln der Form Γ : [p] enthält, so ist die Interpretation der beiden Klauseln in (∗) in der Vervollständigung von P durch die Formel

p ↔ q_{1} ∨ q_{2}

gegeben. Diese Formel drückt aus, daß p nur dann gelten kann, wenn es aus einer der beiden Klauseln in (∗) folgt. Das heißt aber, daß q_{1} oder q_{2} gelten muß, falls p gilt.

Bevor wir die exakte Definition der Vervollständigung eines normalen Programmes angeben können, sind noch einige andere Begriffe festzulegen.

Definition 7.3 (Definition eines Prädikatszeichens) Die Definition eines Prädikatszeichens q in einem normalen Programm P ist die Menge aller derjenigen Klauseln aus P, in deren Kopf q auftritt. Für die Definition von q in P schreiben wir def_{P} (q).

Definition 7.4 (Transformierte einer Klausel) Ist P ein normales Programm, ist C = [L_{1}, ⋯, L_{m}] : [qt_{1} ⋯ t_{n}] eine Klausel aus def_{P} (q) und gilt FV (C) = {y_{1}, ⋯, y_{k}}, so definieren wir die Transformierte T (C) der Klausel C als die Formel

∃y_{1} ⋯ ∃y_{k}(x_{1} ≐ t_{1} ∧ ⋯ ∧ x_{n} ≐ t_{n} ∧ L_{1} ∧ ⋯ ∧ L_{m}) → qx_{1} ⋯ x_{n}.

Dabei setzen wir natürlich voraus, daß {x_{1}, ⋯, x_{n}} ∩ {y_{1}, ⋯, y_{k}} = ∅ ist.

In der letzten Definition ist ≐ ein neues 2–stelliges Prädikatszeichen, dessen mögliche Interpretationen wir später durch eine geeignete Theorie festlegen werden.

Definition 7.5 (Vervollständigte Definition eines Prädikatszeichens) Es sei P ein normales Programm und q sei ein Prädikatszeichen, für welches def_{P} (q) nicht leer ist. Dann konstruieren wir die vervollständigte Definition von q in P (geschrieben comp_{P} (q)), indem wir für jede Klausel C aus def_{P} (q) zunächst die Transformierte T (C) bilden. Ist def_{P} (q) = {C_{1}, ⋯, C_{m}}, so erhalten wir dabei n Formeln der Gestalt:

T (C_{1}) = (F_{1} → qx_{1} ⋯ x_{n}),
⋮
T (C_{m}) = (F_{m} → qx_{1} ⋯ x_{n}).

Dann definieren wir comp_{P} (q) als die Formel

∀x_{1} ⋯ ∀x_{n}(qx_{1} ⋯ x_{n} ↔ F_{1} ∨ ⋯ ∨ F_{m}).

Ist def_{P} (q) = ∅ und ist q n–stellig, so setzen wir

comp_{P} (q) := ∀x_{1} ⋯ ∀x_{n}¬qx_{1} ⋯ qx_{n}.

Um von den vervollständigten Definitionen der Prädikatszeichen zur Vervollständigung von P zu kommen, benötigen wir noch eine Theorie T h(≐), um die Interpretation des neuen Prädikatszeichens ≐ festlegt.

Definition 7.6 (T h(≐)) Ist A = (Λ, Σ) das unserer Sprache zugrundeliegende Alphabet, so besteht T h(≐) aus den folgenden Formeln:

1. Ist f ∈Λ n–stellig, g ∈Λ m–stellig und f ≠ g, so enthält T h(≐) die Formel

¬fx_{1} ⋯ x_{n} ≐ gy_{1} ⋯ y_{m}.

2. Für jeden Term t∈T , in dem die Variable x auftritt und der selber von x verschieden ist, enthält T h(≐) die Formel

¬t ≐ x.

3. T h(≐) enthält die Formeln

x ≐ x, x ≐ y → y ≐ x und x ≐ y ∧ y ≐ z → x ≐ z.

4. Für jedes n–stellige f ∈Λ enthält T h(≐) die Formel

x_{1} ≐ y_{1} ∧ ⋯ ∧ x_{n} ≐ y_{n} ↔ fx_{1} ⋯ x_{n} ≐ fy_{1} ⋯ y_{n}.

5. Für alle n–stelligen Prädikatszeichen p∈Σ enthält T h(≐) die Formel

x_{1} ≐ y_{1} ∧ ⋯ ∧ x_{n} ≐ y_{n} ∧ px_{1} ⋯ x_{n} → py_{1} ⋯ y_{n}.

Der Theorie T h(≐) ist weniger eine Theorie der Gleichheit, als eine Theorie der Unifizierbarkeit. Diese Anschauung wird durch die beiden folgenden Lemmata ausgedrückt, die wir hier allerdings ohne Beweis mitteilen, da wir diese Ergebnisse einerseits im folgenden nicht benötigen werden und andererseits für einen Beweis auch zu weit ausholen müßten. Ein eleganter Beweis findet sich beispielsweise in dem Artikel von Apt [Apt90] im Handbook of Theoretical Computer Science.

Lemma 7.7 Sind t und s zwei Terme, die nicht unifizierbar sind, so gilt:

T h(≐) ⊧ ∀(¬t ≐ s).

Lemma 7.8 Sind t und s zwei unifizierbare Terme, ist μ = mgu(t, s) und sind x_{1}, ⋯ x_{n} die in t oder s auftretenden Variablen, so gilt:

T h(≐) ⊧ ∀x_{1} ⋯ ∀x_{n}(t ≐ s ↔ x_{1} ≐ μ(x_{1}) ∧ ⋯ ∧ x_{n} ≐ μ(x_{n})).

Definition 7.9 (Vervollständigung eines normalen Programmes) Ist P ein normales Programm zu dem Alphabet A = (Λ, Σ), so definieren wir die Vervollständigung von P (geschrieben comp(P)) als

{comp_{P} (q) : q ∈Σ} ∪ T h(≐).

Definition 7.10 (Korrekte Antwort) Ist P ein normales Programm, G = [L_{1}, ⋯, L_{n}] : [] ein normales Goal und ϑ eine Substitution, so nennen wir ϑ eine korrekte Antwort für comp(P) ∪ {G}, falls gilt:

comp(P) ⊧ ∀((L_{1} ∧ ⋯ ∧ L_{n})ϑ).

Theorem 7.11 (Korrektheit der SLDNF–Resolution) Es sei P ein normales Programm und G ein normales Goal. Falls

P ∪ {G} ⊢_{ω}^{ϑ} □

gilt, so ist ϑ eine korrekte Antwort für comp(P) ∪ {G}.

Ein Beweis dieses Theorem findet sich auf Seite 93 in [Llo87] (Theorem 15.6). _{□}

Bemerkung: Bedauerlicherweise bringt der oben zitierte Korrektheitssatz keine Widerspruchsfreiheit der SLDNF–Resolution mit sich. Das liegt daran, daß unter Umständen

comp(P) ⊧ ⊥

gelten kann. Ein einfaches Beispiel dafür bildet das Programm P, das nur aus der Klausel

[¬q]:[q]

besteht. In diesem Fall enthält comp(P) die Formel

q ↔ ¬q,

und die ist offenbar widersprüchlich. Das ist auch der Grund, daß wir im Kapitel 6 mit Theorem (5.12) die Widerspruchsfreiheit der SLDNF–Resolution auf rein syntaktischem Weg nachgewiesen haben.

7.3 Semantische Vollständigkeit der SLDNF–Resolution

In diesem Abschnitt zeigen wir die Vollständigkeit der SLDNF–Resolution bezüglich der im letzten Abschnitt eingeführten Vervollständigung eines normalen Programmes. Unser Ziel ist es, den Korrektheitssatz (7.11) aus dem letzten Abschnitt umzukehren.

Mit P bezeichnen wir in diesem Abschnitt ein normales Programm, und σ bezeichne eine feste I/O–Spezifikation für P.

Bevor wir mit dem Beweis des Vollständigkeitssatzes beginnen können, sind noch einige Hilfssätze zu beweisen. Wir benötigen einerseits ein zu Lemma (4.6) analoges Lifting–Lemma für die SLDNF–Resolution, und andererseits müssen wir in der Lage sein, SLDNF–Widerlegungen aneinanderzuhängen. Dieser letzte Punkt bedarf einiger Vorbereitung. Wir beginnen mit einem Transitivitätslemma für die SLDNF–Resolution.

Lemma 7.12 (Transitivitätslemma für die SLDNF–Resolution)

Vor.: P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}} Δ:[] und P ∪ {Δ:[]} ⊢_{k}^{ϑ_{2}} Λ:[].

Beh.: P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}ϑ_{2}} Λ:[].

Beweis: Wir führen den Beweis durch eine Induktion nach dem Aufbau der Herleitung von

P ∪ {Δ:[]} ⊢_{k}^{ϑ_{2}} Λ:[].

Im Induktionsanfang ist Δ = Λ und ϑ_{2} = id, so daß die Behauptung trivial ist. Im Induktionsschritt führen wir eine Fallunterscheidung nach der Art des letzten Schlusses durch.

1. Fall: Es gilt

(1)  P ∪ {Δ:[]} ⊢_{k}^{ϑ_{0}} [Q_{0}|Δ_{0}]:[]

und der letzte Schluß hat die Form

P ∪ {[Q_{0}|Δ_{0}]:[]} ⊢_{k}^{μ} Λ:[].

Es gibt also eine Klausel C = [K_{1}, ⋯, K_{m}] : [Q] in P, so daß Q und Q_{0} unifizierbar sind und μ = mgu(Q, Q_{0}) ist, und es gilt

(2)  Λ = [K_{1}μ, ⋯, K_{m}μ], Δ_{0}μ.

Außerdem ist ϑ_{2} = ϑ_{0}μ. Nach IV folgt aus (1), daß

(3)  P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}ϑ_{0}} [Q_{0}|Δ_{0}]:[],

gilt. Ein Schnitt mit der Klausel C verwandelt (3) in

P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}ϑ_{0}μ} [K_{1}μ, ⋯, K_{m}μ], Δ_{0}μ:[]

und das ist wegen ϑ_{2} = ϑ_{0}μ und (2) die Behauptung.

2. Fall: Es gilt

(1)  P ∪ {Δ:[]} ⊢_{k}^{ϑ_{0}} [¬Q_{0}|Δ_{0}]:[]

und der letzte Schluß ist von der Gestalt

P ∪ {[¬Q_{0}|Δ_{0}]:[]} ⊢_{k}^{id} Δ_{0} :[].

In diesem Fall ist ϑ_{2} = ϑ_{0}id, Λ = Δ_{0}, und es gibt einen erfolglosen SLDNF–Baum (vom Rang kleiner als k) für P ∪ {[Q_{0}] : []}. Aus (1) folgt mit der IV, daß

(2)  P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}ϑ_{0}} [¬Q_{0}|Δ_{0}]:[]

gilt. Eine Anwendung der NF–Regel liefert

P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}ϑ_{0}} Δ_{0} :[]

und wegen ϑ_{0} = ϑ_{2} und Λ = Δ_{0} ist das die Behauptung. _{□}

Lemma 7.13 (Abschwächungslemma für die SLDNF–Resolution)

Vor.: P ∪ {Γ:[]} ⊢_{k}^{ϑ} Δ:[] und FV (Λ) = ∅.

Beh.: P ∪ {Γ, Λ:[]} ⊢_{k}^{ϑ} Δ, Λ:[].

Beweis: Wir führen den Beweis durch Herleitungsinduktion. Im Induktionsanfang ist Γ = Δ, und die Behauptung ist trivial. Im Induktionsschritt führen wir eine Fallunterscheidung nach der Art des letzten Schlusses in der Herleitung P ∪ {Γ:[]} ⊢_{k}^{ϑ} Δ:[] durch.

1. Fall: Es gilt

(1)  P ∪ {Γ:[]} ⊢_{k}^{ϑ_{0}} [Q_{0}|Δ_{0}]:[]

und der letzte Schluß hat die Form

P ∪ {[Q_{0}|Δ_{0}]:[]} ⊢_{k}^{μ} Δ:[].

Es gibt also eine Klausel C = [K_{1}, ⋯, K_{m}] : [Q] in P, so daß Q und Q_{0} unifizierbar sind und μ = mgu(Q, Q_{0}) ist, und es gilt

(2)  Δ = [K_{1}μ, ⋯, K_{m}μ], Δ_{0}μ.

Außerdem ist ϑ = ϑ_{0}μ. Nach IV folgt aus (1), daß

(3)  P ∪ {Γ, Λ:[]} ⊢_{k}^{ϑ_{0}} [Q_{0}|Δ_{0}], Λ:[],

gilt. Ein Schnitt mit der Klausel C verwandelt (3) in

(4)  P ∪ {Γ, Λ:[]} ⊢_{k}^{ϑ_{0}μ} [K_{1}μ, ⋯, K_{m}μ], Δ_{0}μ, Λ:[].

Eigentlich müßten wir in (4) Λμ statt Λ schreiben, aber da Λ geschlossen ist, ist Λ = Λμ. Wegen ϑ = ϑ_{0}μ und (2) stimmt (4) mit der Behauptung überein.

(1)  P ∪ {Γ:[]} ⊢_{k}^{ϑ} [¬Q_{0}|Δ]:[]

und der letzte Schluß ist von der Gestalt

P ∪ {[¬Q_{0}|Δ]:[]} ⊢_{k}^{id} Δ:[].

Dann gibt es einen erfolglosen SLDNF–Baum (vom Rang kleiner als k) für P ∪ {[Q_{0}]:[]}. Aus (1) folgt mit der IV, daß

(2)  P ∪ {Γ, Λ:[]} ⊢_{k}^{ϑ} [¬Q_{0}|Δ], Λ:[]

gilt. Eine Anwendung der NF–Regel liefert

P ∪ {Γ, Λ:[]} ⊢_{k}^{ϑ} Δ, Λ:[]

und das ist die Behauptung. _{□}

Lemma 7.14 (Verklebungslemma für die SLDNF–Resolution)

Vor.: P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}} □ und P ∪ {Δ:[]} ⊢_{k}^{ϑ_{2}} Λ:[] mit FV (Δ) = ∅.

Beh.: P ∪ {Γ, Δ:[]} ⊢_{k}^{ϑ_{1}ϑ_{2}} Λ:[].

Beweis: Zunächst folgt aus P ∪ {Γ:[]} ⊢_{k}^{ϑ_{1}} []:[] und FV (Δ) = ∅ mit dem soeben bewiesenen Abschwächungslemma, daß

(∗)  P ∪ {Γ, Δ:[]} ⊢_{k}^{ϑ_{1}} Δ:[]

gilt. Daraus folgt mit P ∪ {Δ : []} ⊢_{k}^{ϑ_{2}} Λ : [] und dem Transitivitätslemma die Behauptung. _{□}

Lemma 7.15 (Aneinanderhängen von SLDNF–Widerlegungen)

Vor.: Für alle i∈{1, ⋯, n} gilt

P ∪ {Γ_{i}:[]} ⊢_{k}^{ϑ_{i}} □ und FV (Γ_{i}) = ∅.

Beh.: Dann gibt es ein ϑ∈SUB, so daß gilt:

P ∪ {Γ_{1}, ⋯, Γ_{n}:[]} ⊢_{k}^{ϑ} □.

Beweis: Dieses Lemma läßt sich mit Hilfe des Verklebungslemmas durch eine triviale Induktion nach n beweisen.

Lemma 7.16 (Lifting–Lemma für die SLDNF–Resolution)

Vor.: 1. P ∪ {Γ:[]} ist σ–konsistent.

2. P ∪ {Γτ:[]} ⊢_{k}^{ϑ} Δ:[].

Beh.: Es gibt ein normales Goal Δ̂:[] und zwei Substitutionen ϑ̂ und φ, so daß

1. P ∪ {Γ:[]} ⊢ϑ̂ ; k Δ̂:[] und

2. τϑ = ϑ̂φ und Δ = Δ̂φ gilt.

Beweis: Wir führen den Beweis durch Herleitungsinduktion. Der Induktionsanfang ist trivial, da dort Δ = Γτ und ϑ = id ist. (Die Definitionen ϑ̂ := id, φ := τ und Δ̂ := Γ liefern dann die Behauptung.) Im Induktionsschritt führen wir eine Fallunterscheidung nach dem letzten Schluß durch:

1. Fall: Es gilt

(1)  P ∪ {Γτ:[]} ⊢_{k}^{ϑ_{0}} [Q_{0}|Δ_{0}]:[]

und der letzte Schluß hat die Form

P ∪ {[Q_{0}|Δ_{0}]:[]} ⊢_{k}^{μ_{0}} Δ:[].

Es gibt also eine Klausel C = [K_{1}, ⋯, K_{m}] : [Q] in P, so daß Q und Q_{0} unifizierbar sind, weiter ist μ_{0} = mgu(Q, Q_{0}) und es gilt

Δ = [K_{1}μ_{0}, ⋯, K_{m}μ_{0}], Δ_{0}μ_{0}.

Außerdem ist ϑ = ϑ_{0}μ_{0}. Nach IV folgt aus (1), daß es Substitutionen ϑ̂_{0} und φ_{0}, sowie ein Atom Q̂_{0} und eine Liste Δ̂_{0} gibt, so daß gilt:

(2)  P ∪ {Γ:[]} ⊢ϑ̂_{0} ; k [Q̂_{0}|Δ̂_{0}]:[],

(3)  τϑ_{0} = ϑ̂_{0}φ_{0}, Q_{0} = Q̂_{0}φ_{0} und Δ_{0} = Δ̂_{0}φ_{0}.

Wir können o.B.d.A. davon ausgehen, daß dom(φ_{0}) ∩ FV (C) = ∅ ist. Das impliziert Qφ_{0} = Q und dann zeigt die Gleichungskette

Q̂_{0}φ_{0}μ_{0} = Q_{0}μ_{0} = Qμ_{0} = Qφ_{0}μ_{0},

daß Q̂_{0} und Q unifizierbar sind. Ist μ = mgu(Q̂_{0}, Q), so gibt es eine Substitution φ, so daß

(4)  φ_{0}μ_{0} = μφ

gilt. Mit der Definition Δ̂ := [K_{1}μ, ⋯, K_{m}μ], Δ̂_{0}μ gilt jetzt

P ∪ {[Q̂_{0}|Δ̂_{0}]:[]} ⊢_{k}^{μ} Δ̂:[]

und daraus folgt mit (2)

(5)  P ∪ {Γ:[]} ⊢ϑ̂ ; k Δ̂:[] mit ϑ̂:= ϑ̂_{0}μ.

Außerdem gilt

τϑ = τϑ_{0}μ_{0} =^{(3)} ϑ̂_{0}φ_{0}μ_{0} =^{(4)} ϑ̂_{0}μφ =^{(5)} ϑ̂φ

und es ist

\begin{aligned}Δ̂φ & = & [K_{1}μφ, ⋯, K_{m}μφ], Δ̂_{0}μφ \\ & = & [K_{1}φ_{0}μ_{0}, ⋯, K_{m}φ_{0}μ_{0}], Δ̂_{0}φ_{0}μ_{0} & = & Δ. \end{aligned}

Damit ist für diesen Fall alles gezeigt.

2. Fall: Es gilt

(1)  P ∪ {Γτ:[]} ⊢_{k}^{ϑ} [¬Q_{0}|Δ]:[]

und der letzte Schluß ist von der Gestalt

(2)  P ∪ {[¬Q_{0}|Δ]:[]} ⊢_{k}^{id} Δ:[].

Nach IV folgt aus (1), daß es zwei Substitutionen ϑ̂ und φ, ein Atom Q̂_{0} und eine Liste Δ̂ gibt, so daß

(3)  P ∪ {Γ:[]} ⊢ϑ̂ ; k [¬Q̂_{0}|Δ̂]:[],

(4)  τϑ = ϑ̂φ, Q_{0} = Q̂_{0}φ und Δ = Δ̂φ

gilt. Nach Lemma (6.5) ist P ∪ {[¬Q̂_{0}|Δ] : []} σ–konsistent. Also ist Q̂_{0} geschlossen und daher gilt Q̂_{0}φ = Q̂_{0}. Dies zeigt, daß Q_{0} = Q̂_{0} ist. Aus (2) folgt, daß es einen erfolglosen SLDNF–Baum für P ∪{[Q_{0}]:[]} gibt und dieser Baum ist natürlich auch ein erfolgloser SLDNF–Baum für P ∪{[Q̂_{0}]: []}. Also gilt

P ∪ {[¬Q̂_{0}|Δ̂]:[]} ⊢_{k}^{id} Δ̂:[]

und daraus folgt mit (3)

P ∪ {Γ:[]} ⊢ϑ̂ ; k Δ̂:[].

Der Rest der Behauptung folgt jetzt aus (4). _{□}

Wir kommen nun zum Höhepunkt dieses Kapitels. Wir zeigen, daß für konsistent geordnete Programme P, für die die Theorie comp(P) widerspruchsfrei ist, jede korrekte Antwort Instanz einer berechneten Antwort ist. Genauer gilt:

Theorem 7.17 (Vollständigkeitssatz) Es sei P ein normales Programm, G ein normales Goal und σ eine I/O– Spezifikation für P ∪ {G}. Ferner gelte:

1. P ∪ {G} ist σ–konsistent.

2. P ist geordnet bezüglich σ.

3. Die Substitution ϑ ist eine korrekte Antwort für P ∪ {G}.

Dann gibt es Substitutionen ϑ̂ und φ, so daß gilt:

1. P ∪ {G} ⊢_{ω}^{φ} □.

2. φ ≤ ϑ̂ und ϑ(x) = ϑ̂(x) für alle x∈FV (G).

Beweis: Ist G = [L_{1}, ⋯, L_{n}]:[], so folgt aus der Korrektheit von ϑ, daß

(1)  comp(P) ⊧ ∀((L_{1} ∧ ⋯ ∧ L_{n})ϑ)

gilt. Sind x_{1}, ⋯, x_{m} die in Gϑ auftretenden Variablen, so wählen wir neue Konstanten c_{1}, ⋯, c_{m} und definieren eine Substitution τ durch:

τ := [x_{1}/c_{1}, ⋯, x_{m}/c_{m}].

Aus (1) folgt dann

(2)  comp(P) ⊧ L_{1}ϑτ ∧ ⋯ ∧ L_{n}ϑτ.

An dieser Stelle müssen wir die zugrunde liegende Sprache um die neu hinzu kommenden Konstanten c_{1}, ⋯, c_{m} erweitern. Wir müssen dann ebenfalls die Definition der Funktion weight auf diese Zeichen ausdehnen. Wir erreichen das durch die Festlegung

weight(c_{i}) := 1 für alle i∈{1, ⋯, m}.

Da die Konstanten c_{i} in dem Programm P nicht auftreten, ist klar, daß P auch als Programm aus dem neuen Alphabet weiterhin bezüglich σ geordnet ist.

Die Theorie comp(P) hängt nicht nur von dem Programm P ab, sondern ebenfalls von der zugrunde liegenden Sprache. Da diese Sprache bis jetzt immer durch ein festes Alphabet gegeben war, haben wir diese Abhängigkeit bis jetzt in der Notation unterdrückt. In (2) steht comp(P) noch für die Vervollständigung von P in der alten Sprache. Bei der Vervollständigung von P in der neuen Sprache kommen zu der alten Theorie comp(P) noch Gleichungen der Gestalt c_{i} ≐ c_{i} und Ungleichungen der Form ¬c_{i} ≐ ft_{1} ⋯ t_{k} für alle k–stelligen Funktionszeichen f der neuen Sprache hinzu. Wir wollen diese neue Theorie mit comp(P)^{+} bezeichen. Da comp(P)^{+} eine Erweiterung von comp(P) ist, folgt aus (2)

comp(P)^{+} ⊧ L_{1}ϑτ ∧ ⋯ ∧ L_{n}ϑτ.

Daraus folgt insbesondere

(3)  comp(P)^{+} ⊧ L_{i}ϑτ für alle i∈{1, ⋯, n}.

Da die L_{i}ϑτ alle geschlossen sind, zeigt der syntaktische Vollständigkeitssatz (7.2), daß für alle i∈{1, ⋯, n}

P ∪ {[L_{i}ϑτ]:[]} ⊢_{ω} □ oder P ∪ {[¬L_{i}ϑτ]:[]} ⊢_{ω} □

gilt. Träte für ein i∈{1, ⋯, n} der zweite Fall ein, gälte also

P ∪ {[¬L_{i}ϑτ]:[]} ⊢_{ω} □,

so würde daraus aufgrund des Korrektheitssatzes (7.11)

comp(P)^{+} ⊧ ¬L_{i}ϑτ

folgen. Dann wäre die Theorie comp(P)^{+} inkonsistent. Dies widerspricht dem im nächsten Abschnitt hergeleiteten Satz (7.22). Daher können wir davon ausgehen, daß

P ∪ {[L_{i}ϑτ]:[]} ⊢_{ω} □

für alle i∈{1, ⋯, n} gilt. Nun zeigt uns das Lemma (7.15), daß es ein γ̂ ∈SUB gibt, so daß

(4)  P ∪ {Gϑτ} ⊢γ̂ ; ω □

gilt. Wir können o.B.d.A. voraussetzen, daß alle in der Herleitung (4) verwendeten Variablen von x_{1}, ⋯, x_{m} verschieden sind. Daher können wir in dieser Herleitung die Konstanten c_{i} wieder durch die Variablen x_{i} ersetzen. Etwas ungenau könnten wir sagen, daß wir die Herleitung mit der “Substitution” τ^{−1} multiplizieren. Dann erhalten wir

(5)  P ∪ {Gϑ} ⊢_{ω}^{γ} □ mit γ = γ̂τ^{−1}.

Da FV (Gϑτ) = ∅ ist, gilt offenbar γ̂|FV (Gϑτ) = id. Da die Variablen x_{1}, ⋯, x_{n} in der Herleitung (4) nicht auftreten, kann γ̂ auch keine Bindungen für diese Variablen enthalten. Wegen γ̂τ^{−1} = γ gilt dies auch für γ und wir haben

(6)  dom(γ) ∩ FV (Gϑ) = ∅.

Aus (5) folgt mit dem Lifting–Lemma für die SLDNF–Resolution, daß es zwei Substitutionen φ und ϱ gibt, so daß

P ∪ {G} ⊢_{ω}^{φ} □ und ϑγ = φϱ

gilt. Definieren wir ϑ̂ := ϑγ, so stimmen ϑ und ϑ̂ wegen (6) auf x_{1}, ⋯, x_{n} überein und darüber hinaus gilt:

φ ≤ ϑ̂. _{□}

7.4 Die Konsistenz von comp(P)

In diesem Abschnitt geht es uns darum, den Beweis der Konsistenz von comp(P) für ein konsistent geordnetes Programm P nachzutragen, die wir im letzten Abschnitt bei der Herleitung des Vollständigkeitssatzes (7.17) benutzt haben. Wir werden zeigen, daß wir die Voraussetzung

“Die Theorie comp(P) ist konsistent.”

bereits aus den Voraussetzungen des Vollständigkeitssatzes folgern können. Dies ist auch deshalb ein wichtiges Ergebnis, weil die Konsistenz von comp(P) im allgemeinen unentscheidbar ist. Wir werden die Konsistenz von comp(P) dadurch nachweisen, daß wir zu jedem konsistent geordneten Programm P ein Herbrand– Modell für comp(P) konstruieren.

Definition 7.18 (Herbrand–Basis) Ist A := (Λ, Σ) das unserer Sprache zugrundeliegende Alphabet, so definieren wir die Herbrand–Basis B als die Menge

B := {pt_{1} ⋯ t_{n} : p∈Σ ist n–stellig, t_{1}, ⋯, t_{n} ∈U}

(Zur Erinnerung: Mit U bezeichnen wir das Herbrand–Universum, das in diesem Fall aus allen geschlossenen Termen der Sprache besteht.)

Ist H eine Herbrand–Struktur, so ist H durch die folgende Teilmenge I der Herbrand–Basis B

(∗)  I := {pt_{1}..t_{n} ∈ B : W ert_{H}(pt_{1} ⋯ t_{n}) = W }

bereits eindeutig bestimmt. Wir werden daher bei unseren weiteren Überlegungen Herbrand–Strukturen mit der durch (∗) gegebenen Teilmenge der Herbrand– Basis identifizieren. Als nächstes ordnen wir jedem normalen Programm P einen auf der Potenzmenge der Herbrand–Basis definierten Operator T_{P} zu. Vorab vereinbaren wir, daß wir mit grund(P) die Menge aller geschlossenen Instanzen von Klauseln aus P bezeichnen.

Definition 7.19 (T_{P}) Es sei P ein normales Programm. Dann definieren wir eine Abbildung T_{P} : P(B) → P(B) durch

T_{P} (I) := {Q : ∃([L_{1}, ⋯, L_{n}]:[Q]) ∈ grund(P) & L_{1} ˜∈I & ⋯ & L_{n} ˜∈I}.

Dabei soll L˜∈I für ein positives Literal L wahr sein, wenn L∈I ist. Für ein negatives Literal L = ¬Q ist L˜∈I genau dann wahr, wenn Q∉I ist.

Wollen wir ein Modell für comp(P) konstruieren, so benötigen wir noch eine Interpretation für das neu hinzugefügte Prädikatszeichen ≐, das ja nicht aus unserem Alphabet A stammt. Wir vereinbaren, daß wir ≐ in einer Herbrand– Struktur immer durch die Identität interpretieren werden. (Solche Herbrand– Strukturen heißen auch normale Herbrand–Strukturen.)

Der folgende Satz stellt ein wichtiges Hilfsmittel dar, um Herbrand–Modelle eines normalen Programmes konstruieren zu können.

Satz 7.20 Es sei P ein normales Programm und I ⊆ B sei eine Herbrand– Struktur für P. Falls T_{P} (I) = I ist, so ist I ein Modell von comp(P).

Beweis: Dieser Satz ist eine direkte Konsequenz von Satz 14.3 in [Llo87]. Wir müssen uns nur klar machen, daß unsere Vereinbarung, ≐ in einem Herbrand– Modell immer durch die Identität zu interpretieren, I zu einem Modell von T h(≐) macht, denn für zwei geschlossene Terme s und t gilt (vgl. [Llo87] Seite 79):

T h(≐) ⊧ s ≐ t ⇔ s ≡ t. _{□}

Das folgende Lemma zeigt, unter welchen Umständen eine Widerlegung mit einer Substitution “multipliziert” werden darf.

Lemma 7.21 (Multiplikationslemma für die SLDNF–Resolution)

Vor.: Es gelte

H zeigt P ∪ {Γ:[]} ⊢_{k}^{ϑ} □

und σ sei eine Substitution, für die var(σ) = ∅ und FV (H) ⊆ dom(σ) gilt.

Beh.: Dann gibt es eine Substitution ϑ̂, so daß gilt:

P ∪ {Γϑσ:[]} ⊢ϑ̂ ; k □.

Beweis: Wir führen den Beweis durch Herleitungsinduktion. Der Induktionsanfang ist trivial. Im Induktionsschritt führen wir eine Fallunterscheidung nach der Art des \underline{ersten} Schlußes durch.

1. Fall: Γ = [Q_{0}|Γ_{0}] In diesem Fall gibt es eine Klausel C = [K_{1}, ⋯, K_{m}] : [Q] in P, so daß Q und Q_{0} unifizierbar sind. Ist μ = mgu(Q, Q_{0}), so hat der erste Schluß die Form

(1)  P ∪ {[Q_{0}|Γ_{0}]} ⊢_{k}^{μ} [K_{1}μ, ⋯, K_{m}μ], Γ_{0}μ:[],

es gilt

(2)  P ∪ {[K_{1}μ, ⋯, K_{m}μ], Γ_{0}μ:[]} ⊢_{k}^{ϑ_{0}} □

und ϑ = μϑ_{0}. Nach IV folgt aus (2), daß es eine Substitution ϑ̂_{0} gibt, so daß

(3)  P ∪ {[K_{1}μϑ_{0}σ, ⋯, K_{m}μϑ_{0}σ], Γ_{0}μϑ_{0}σ:[]} ⊢ϑ̂_{0} ; k □

gilt. Nach den Voraussetzungen, die wir für die Substitution σ gemacht haben, ist Q_{0}ϑσ geschlossen. Also gilt

(4)  Q_{0}ϑσ = (Q_{0}ϑσ)ϑσ.

Damit können wir zeigen, daß Q_{0}ϑσ und Q durch die Substitution ϑσ unifizierbar sind. Es gilt

(Q_{0}ϑσ)ϑσ = Q_{0}ϑσ = Q_{0}μϑ_{0}σ = Qμϑ_{0}σ = Qϑσ.

Definieren wir μ̂ := mgu(Q, Q_{0}ϑσ), so gilt offenbar

(5)  P ∪ {[Q_{0}ϑσ|Γ_{0}ϑσ]} ⊢μ̂ ; k [K_{1}μ̂, ⋯, K_{m}μ̂], Γ_{0}ϑσμ̂:[].

Außerdem gibt es eine Substitution γ, so daß μ̂γ = ϑσ ist, denn ϑσ ist ja ein Unifikator von Q und Q_{0}ϑσ. Darüber hinaus gilt aus den selben Gründen wie (4)

([K_{1}μ̂, ⋯, K_{m}μ̂], Γ_{0}ϑσμ̂:[])γ = [K_{1}ϑσ, ⋯, K_{m}ϑσ], Γ_{0}ϑσ:[].

Da die rechte Seite dieser Gleichung nach (3) eine SLDNF–Widerlegung besitzt, zeigt daß Lifting–Lemma, daß auch die Sequenz in der Klammer auf der linken Seite eine SLDNF–Widerlegung besitzt. Es gibt also eine Substitution ϑ̂_{0}, so daß

(6)  P ∪ {[K_{1}μ̂, ⋯, K_{m}μ̂], Γ_{0}ϑσ:[]} ⊢ϑ̂ ; k □

gilt. (Dabei haben wir Γ_{0}ϑσ = Γ_{0}ϑσμ̂ ausgenutzt, was aus FV (Γ_{0}ϑσ) = ∅ folgt.) Die Behauptung folgt nun aus (5) und (6) mit dem Transitivitätslemma.

2. Fall: Γ = [¬Q_{0}|Γ_{0}] In diesem Fall gibt es zu P ∪ {[Q_{0}] : []} einen erfolglosen SLDNF–Baum (vom Rang kleiner als k), der erste Schluß hat die Gestalt

(1)  P ∪ {[¬Q_{0}|Γ_{0}]:[]} ⊢_{k}^{id} Γ_{0} :[]

und es gilt

(2)  P ∪ {Γ_{0} :[]} ⊢_{k}^{ϑ} □.

Nach IV folgt aus (2), daß es eine Substitution ϑ̂ gibt, für die

(3)  P ∪ {Γ_{0}ϑσ:[]} ⊢ϑ̂ ; k □

gilt. Da Q_{0} geschlossen ist, ist Q_{0}ϑσ = Q_{0}, und (1) zeigt

(4)  P ∪ {[¬Q_{0}ϑσ|Γ_{0}ϑσ]:[]} ⊢_{k}^{id} Γ_{0}ϑσ:[].

Aus (4) und (3) folgt die Behauptung mit dem Transitivitätslemma. _{□}

Nun haben wir alles Material zusammen, um für konsistent geordnete Programme P ein Herbrand–Modell für comp(P) konstruieren zu können.

Satz 7.22 (Konsistenzsatz für konsistent geordnete Programme) Ist P ein normales, konsistent geordnetes Programm, so existiert für die Theorie comp(P) ein (normales) Herbrand–Modell I.

Beweis: Wir definieren I durch

(1)  I := {Q∈B : P ∪ {[Q]:[]} ⊢_{ω} □}.

Wir zeigen, daß I mit dieser Definition ein Fixpunkt des Operators T_{P} wird. Die Behauptung folgt dann aus Satz (7.20).

Zunächst zeigen wir, daß T_{P} (I) ⊆ I ist. Ist Q∈T_{P} (I), so gibt es eine Klausel C = [L_{1}, ⋯, L_{n}]:[Q_{0}] aus P und eine Substitution φ, so daß

FV (Cφ) = ∅, Q_{0}φ = Q und L_{1}φ˜∈I, ⋯, L_{n}φ˜∈I

gilt. Als erstes zeigen wir, daß für alle i∈{1, ⋯, n}

(2)  P ∪ {[L_{i}φ]:[]} ⊢_{ω} □

gilt. Ist das Literal L_{i} positiv, so folgt dies sofort aus der Definition (1) von I. Ist L_{i}φ = ¬Q̃ für ein Atom Q̃∈B, so folgt aus L_{i}φ˜∈I, daß Q̃ ∉ I ist. In diesem Fall zeigt die Definition von I, daß

P ∪ {[Q̃]:[]} ⊬_{ω} □

gilt. Aus dem syntaktischen Vollständigkeitssatz (7.2) folgt dann

P ∪ {[¬Q̃]:[]} ⊢_{ω} □

und damit ist (2) gezeigt. Aus (2) folgt mit dem Lemma (7.15), daß

P ∪ {[L_{1}φ, ⋯, L_{n}φ]:[]} ⊢_{ω} □

gilt, und das zeigt

P ∪ {[Q]:[]} ⊢_{ω} □.

Nach (1) gilt dann Q∈I und insgesamt haben wir

(3)  Q∈T_{P} (I) ⇒ Q∈I

nachgewiesen.

Wir zeigen nun I ⊆ T_{P} (I). Ist Q∈I, so gilt nach Definition von I

P ∪ {[Q]:[]} ⊢_{ω} □.

Also gibt es eine Klausel C = [L_{1}, ⋯, L_{n}]:[Q_{0}] und eine Substitution μ, so daß

(4) Q_{0}μ = Qμ = Q, μ = mgu(Q, Q_{0}) und P ∪ {[L_{1}μ, ⋯, L_{n}μ]:[]} ⊢_{ω} □

gilt. (Die Gleichung Qμ = Q folgt aus FV (Q) = ∅.) Wir erweitern μ zu einer Substitution φ ≥ μ, für die

FV (L_{1}φ), ⋯, FV (L_{n}φ) = ∅ und var(φ) = ∅

ist und die Bindungen für alle in der Widerlegung von [L_{1}μ, ⋯, L_{n}μ]:[] auftretenden Variablen enthält. Mit dem Multiplikationslemma 7.21 folgt aus (4), daß

P ∪ {[L_{1}φ, ⋯, L_{n}φ]:[]} ⊢_{ω} □

gilt und daraus folgt

(5)  P ∪ {[L_{i}φ]:[]} ⊢_{ω} □

für alle i ∈ {1, ⋯, n}. Ist L_{i} ein positives Literal, so zeigt die Definition von I, daß L_{i} ˜∈I ist. Für ein negatives Literal L_{i} = ¬Q̃ folgt aus (5) zunächst

P ∪ {[¬Q̃]:[]} ⊢_{ω} □.

Mit der Widerspruchsfreiheit der SLDNF–Resolution (Theorem 5.12) folgt

P ∪ {[Q̃]:[]} ⊬_{ω} □.

Nun zeigt die Definition von I, daß L_{i}φ˜∈I ist. Nach Definition von T_{P} gilt

(6)  Q∈I ⇒ Q∈T_{P} (I).

Aus (3) und (6) folgt mit dem letzten Satz die Behauptung. _{□}

Anwendungen von konsistent geordneten Programmen

In diesem Kapitel zeigen wir, wie sich einige typische Programmieraufgaben durch konsistent geordnete Programme lösen lassen. Durch den Adäquatheitssatz (Theorem 6.13) ist zwar sichergestellt, daß sich jede Funktion, die wir mit vertretbarem Aufwand berechnen können, durch ein konsistent geordnetes Programm berechnen läßt. Es bleibt aber die Frage offen, ob die Lösung, die durch ein konsistent geordnetes Programm geliefert wird, evt. wesentlich umständlicher ist als eine Lösung, die ein “gewöhnliches” Prolog–Programm verwendet. Wir werden in diesem Kapitel untersuchen, unter welchen Umständen sich die üblicherweise bei der Lösung bestimmter Probleme verwendeten Prolog–Programme konsistent ordnen lassen.

Im ersten Abschnitt stellen wir ein Programm zur symbolischen Differentiation von Termen vor. Dieses Programm erkennen wir leicht als konsistent geordnet. Daß bei der symbolischen Differentiation keine Probleme auftreten, war ohnehein zu erwarten, denn dieses Problem läßt sich auch sehr einfach unter Verwendung primitiv–rekusiver Wortfunktionen lösen.

Im zweiten Abschnitt untersuchen wir ein Programm, mit dessen Hilfe es möglich ist, (nichtdeterministische) Pushdown–Automaten zu simulieren. Das von uns vorgestellte Programm wird sich als nicht konsistent geordnet erweisen. Wir stellen daher eine Programmtransformationstechnik vor, mit deren Hilfe es uns möglich ist, das ursprünglich angegebene Programm in ein konsistent geordnetes zu transformieren.

Im letzten Abschnitt betrachten wir zwei Probleme, die sich nicht durch konsistent geordnete Programme lösen lassen. Es wird sich dabei um Probleme handeln, zu deren Lösung eine Suche durchgeführt werden muß, die sich a priori nicht in “einfacher” Weise beschränken läßt.

Es ist zweckmäßig, unsere Schreibweise für Hornformeln den üblicherweise in der Prolog–Gemeinde verwendeten Bräuchen anzupassen. Ist

[L_{1}, ⋯, L_{n}]:[Q]

eine positive Hornformel, so schreiben wir dafür in diesem Kapitel

                        “Q :- L1,· · · ,Ln.'',

für einen Fakt []:[Q] schreiben wir “Q.” und eine negative Hornformel

[L_{1}, ⋯, L_{n}]:[]

schreiben wir als “:- L1, ⋯,Ln.”. Darüberhinaus vereinbaren wir, daß wir Variablen in diesem Kapitel immer durch Großbuchstaben oder durch Wörter, die mit Großbuchstaben beginnen, mitteilen werden.

Um von einem Prolog–Programm P sagen zu können, daß es konsistent geordnet ist, sind zunächst drei Funktionen festzulegen:

1. Die I/O–Spezifikation σ : Σ → {+, −}^{∗}.

2. Die Funktion weight : Λ → N−{0}, die das Gewicht der Funktionszeichen festlegt.

3. Die Abbildung level : Σ → N, die die Prädikatszeichen in Schichten einteilt.

(Dabei bezeichnet Σ die in P auftretenden Prädikatszeichen und Λ ist die Menge der in P auftretenden Funktionszeichen.) Da diese drei Funktionen gewissermaßen Bestandteile des konsistent geordneten Programmes sind, teilen wir sie in Form von Kommentaren am Anfang des Programmes mit. Ist p ∈ Σ ein n–stelliges Prädikatszeichen aus P, so stellen wir einen Fakt der Form

                     ``sigma(p,c1, · · · ,cn).''

an den Anfang des Programmes, um auszudrücken, daß σ(p) = c_{1} ⋯ c_{n} ist. Durch einen Fakt der Form

                          “level(p,k).''

teilen wir mit, daß level(p) = k ist. Ist f ∈ Λ ein m–stelliges Funktionszeichen aus P, so drücken wir durch einen Fakt

                         “weight(f,k).''

aus, daß weight(f) = k ist. (Damit dabei keine Verwirrung entsteht, setzen wir stillschweigend voraus, daß weder das Zeichen “sigma” noch das Zeichen “level” oder das Zeichen “weight” in P als Prädikatszeichen auftritt.) Durch die Beispiele in den folgenden Abschnitten wird klar werden, wie die neue Schreibweise zu verstehen ist.

8.1 Symbolische Differentiation

Eines der Probleme, die durch Prolog mit beeindruckender Eleganz gelöst werden können, ist das Problem, einen gegebenen Term t symbolisch zu differenzieren. Wir nehmen an, daß der zu differenzierende Term t mit Hilfe der Funktionszeichen

(∗)  {sin, cos, exp, log, +, -, *, /, x, 0, 1, -1 }

gebildet wird. Die Stellenzahl der meisten in (∗) erwähnten Funktionszeichen ist intuitiv klar. Wir vereinbaren zusätzlich, daß das Zeichen x 0–stellig ist und das die Zeichen “+” und “−” nur 2–stellig verwendet werden. Dann ist das folgende konsistent geordnete Programm geeignet, jeden aus (∗) gebildeten Term t symbolisch nach x zu differenzieren.

%       sigma( derive, +, - ).          level( derive, 1 ).
%       weight( +, 2 ).                 weight( exp, 1 ).
%       weight( -, 2 ).                 weight( log, 1 ).
%       weight( *, 2 ).                 weight( 0, 1 ).
%       weight( /, 2 ).                 weight( 1, 1 ).
%       weight( sin, 1 ).               weight( -1, 1 ).
%       weight( cos, 1 ).
        derive( U + V, US + VS ) :-
                derive( U, US ),
                derive( V, VS ).
        derive( U - V, US - VS ) :-
                derive( U, US ),
                derive( V, VS ).
        derive( U * V, US * V + U * VS ) :-
                derive( U, US ),
                derive( V, VS ).
        derive( U / V, (US * V - U * VS) / (V * V) ) :-
                derive( U, US ),
                derive( V, VS ).
        derive( sin(U), cos(U) * US ) :-
                derive( U, US ).
        derive( cos(U), -1 * sin(U) * US ) :-
                derive( U, US ).

        derive( exp(U), exp(U) * US ) :-
                derive( U, US ).
        derive( log(U), US / U ) :-
                derive( U, US ).
        derive( 0, 0 ).                 derive( -1, 0 ).
        derive( 1, 0 ).                 derive( x, 1 ).

Die Verifikation, daß es sich bei dem obigen Programm wirklich um ein konsistent geordnetes Programm handelt, ist im Prinzip trivial, in der praktischen Durchführung aber viel zu langwierig, als daß wir sie hier im Detail durchführen könnten. Ist t ein aus den Funktionszeichen in (∗) gebildeter Term, so erkennt der mit Prolog vertraute Leser, daß die zu dem Goal

                       ``:- derive(t,D).''

einzige existierende berechnete Antwort ϑ durch

ϑ(X) = \{ \begin{matrix}\frac{dt}{dx} & falls X = D \\ X & sonst \end{matrix}

gegeben ist. (Ein ähnliches Programm mit einer Diskussion seines Verhaltens findet sich in [StSh86] auf Seite 63.)

Bemerkung: Beim obigen Programm P werden die berechneten Ableitungen selbstverständlich \underline{nicht} vereinfacht, so daß die mit diesem Programm berechneten Ergebnisse von einer skurrilen Komplexität sind. So ergibt sich als Ableitung von exp(1) ∗ sin(x) beispielweise:

        (exp(1) * 0) * sin(x) + exp(1) * (cos(x) * 1).

8.2 Simulation von Pushdown–Automaten

In diesem Abschnitt beschreiben wir ein Prolog–Programm, mit dessen Hilfe es möglich ist, einen (nichtdeterministischen) Pushdown–Automaten zu simulieren. Das Programm P, das wir angeben werden, ist nicht konsistent geordnet und läßt sich in der von uns angegebenen Form auch nicht konsistent ordnen. Wir stellen daher eine Technik zur Programmtransformation vor, mit deren Hilfe es uns möglich ist, das Programm P in ein konsistent geordnetes Programm P̂ zu transformieren. Die zur Transformation verwendete Technik ist nicht neu. Sie ist als “Entfaltung” bekannt, vgl. z.B. [StSh86]. Bevor wir mit der eigentlichen Arbeit beginnen können, müsssen wir definieren, was wir unter einem Pushdown– Automaten verstehen. Wir halten uns an die von Hopcroft und Ullman [HoUl79] gegebene Definition:

Definition 8.1 (Pushdown–Automat) Ein Pushdown–Automat ist ein 6–Tupel (Q, Σ, Γ, δ, q_{0}, Z_{0}). Dabei haben die einzelnen Komponenten die folgende Bedeutung:

1. Q ist die endliche Menge der möglichen Zustände des Automaten.

2. Σ ist das Eingabe–Alphabet.

3. Γ ist das Stack–Alphabet.

4. δ ist eine partielle Abbildung von Q × (Σ ∪ {ε}) × Γ in die Menge aller endlichen Teilmengen von Q × Γ^{∗}.

5. q_{0} ∈Q ist der Anfangszustand.

6. Z_{0} ∈Γ ist das Startsymbol.

Für eine Darstellung der Arbeitsweise eines Pushdown–Automaten verweisen wir auf [HoUl79]. Dort ist auf Seite 112 ein Pushdown–Automat M angegeben, der in der Lage ist, Palindrome gerader Länge aus dem Alphabet {0, 1} zu erkennen. M hat die Gestalt

M = ({q_{1}, q_{2}}, {0, 1}, {R, G, B}, δ, q_{1}, R) mit

\begin{aligned}δ(q_{1}, 0, R) & = & \{(q_{1}, BR)\} & δ(q_{1}, 1, R) & = & \{(q_{1}, GR)\} \\ δ(q_{1}, 0, B) & = & \{(q_{1}, BB), (q_{2}, ε)\} & δ(q_{1}, 1, B) & = & \{(q_{1}, GB)\} \\ δ(q_{1}, 0, G) & = & \{(q_{1}, BG)\} & δ(q_{1}, 1, G) & = & \{(q_{1}, GG), (q_{2}ε)\} \\ δ(q_{2}, 0, B) & = & \{(q_{2}, ε)\} & δ(q_{2}, 1, G) & = & \{(q_{2}, ε)\} \\ δ(q_{1}, ε, R) & = & \{(q_{2}, ε)\} & δ(q_{2}, ε, R) & = & \{(q_{2}, ε)\} \end{aligned}

Liest M ein Wort aus dem Alphabet {0, 1}, so kann der Stack von M danach genau dann leer sein, wenn w ein Palindrom gerader Länge ist. Wir geben nun ein normales Prolog–Programm an, mit dessen Hilfe es möglich ist, diesen Pushdown–Automaten zu simulieren.

accept( Xs ) :- initial( Q ), start( Z ),
                transform( Q, Xs, [ Z ], [] ).
transform( Q, [], Stack, Stack ).
transform( Q, [ X | Xs ], [ S | Ss ], New_Stack ) :-
        delta( Q, X, S, New_Q, New_Ss ),
        append( New_Ss, Ss, Intermediate_Stack ),
        transform( New_Q, Xs, Intermediate_Stack, New_Stack ).
transform( Q, Xs, [ S | Ss ], New_Stack ) :-

        delta( Q, epsilon, S, New_Q, New_Ss ),
        append( New_Ss, Ss, Intermediate_Stack ),
        transform( New_Q, Xs, Intermediate_Stack, New_Stack ).
append( [], List, List ).
append( [ X | Xs ], List, [ X | Xs_List ] ) :-
        append( Xs, List, Xs_List ).
initial( q_1 ).                      start( r ).
delta( q_1, 0, r, q_1, [b,r] ).      delta( q_1, 0, b, q_2, [] ).
delta( q_1, 1, r, q_1, [g,r] ).      delta( q_1, 1, g, q_2, [] ).
delta( q_1, 0, b, q_1, [b,b] ).      delta( q_2, 0, b, q_2, [] ).
delta( q_1, 0, g, q_1, [b,g] ).      delta( q_2, 1, g, q_2, [] ).
delta( q_1, 1, b, q_1, [g,b] ).
delta( q_1, 1, g, q_1, [g,g] ).
delta( q_1, epsilon, r, q_2, [] ).
delta( q_2, epsilon, r, q_2, [] ).

Das obige Programm bezeichnen wir mit P_{M}. Ist Xs eine Liste, die ein Wort aus dem Alphabet {0, 1}^{∗} repräsentiert, so gilt

P_{M} ∪ {[accept(Xs)]:[]} ⊢_{ω} □

genau dann, wenn Xs als Wort aufgefaßt von dem oben angegebenen Pushdown– Automaten M akzeptiert wird. Um P_{M} in ein geordnetes Programm zu überführen, ist eine I/O–Spezifikation und eine Abbildung level festzulegen. Darüberhinaus müssen wir den Funktionszeichen Gewichte zuordnen. An dieser Stelle erinnern wir kurz daran, daß Prolog–Listen in Wahrheit Terme sind, die mit dem Funktionszeichen “dot” aufgebaut sind. Die Prolog–Schreibweise [X|Xs] steht eigentlich für den Term dot(X,Xs) und [] steht für die Konstante nil. Ein naheliegender Ansatz, die Funktionen “level”, σ und “weight” festzulegen, ist:

%       sigma( accept, + ).
%       sigma( transform, +, +, +, - ).
%       sigma( append, +, +, - ).
%       sigma( initial, - ).
%       sigma( start, - ).
%       sigma( delta, +, +, +, -, - ).
%       level( accept, 3 ).                     weight( dot, 1 ).
%       level( transform, 2 ).                  weight( nil, 1 ).
%       level( append, 1 ).                     weight( q_1, 1 ).
%       level( initial, 1 ).                    weight( q_2, 1 ).

%       level( start, 1 ).                      weight( r, 1 ).
%       level( delta, 1 ).                      weight( b, 1 ).
%       level( delta, 1 ).                      weight( g, 1 ).

Mit dieser Definition ist P_{M} allerdings nicht konsistent geordnet. Der Grund dafür ist in den Klauseln für das Prädikat transform zu suchen. In der Klausel

transform( Q, [ X | Xs ], [ S | Ss ], New_Stack ) :-
        delta( Q, X, S, New_Q, New_Ss ),
        append( New_Ss, Ss, Intermediate_Stack ),
        transform( New_Q, Xs, Intermediate_Stack, New_Stack ).

tritt die Variable Intermediate_Stack positiv in dem Literal

(*)        transform( New_Q, Xs, Intermediate_Stack, New_Stack )

auf, die Variable tritt aber nicht im Kopf der Klausel auf. Eine genauere Analyse zeigt, daß sich dieses Problem auch nicht dadurch ändern läßt, daß wir unsere I/O–Spezifikation σ anders definieren. Wir könnten zwar versuchen, die I/O– Spezifikation für transform in

        sigma( transform, -, +, -, -, - ).

abzuändern. Dann wären für die Klausel (∗) zwar alle Bedingungen erfüllt, aber bei der Klausel

transform( Q, Xs, [ S | Ss ], New_Stack ) :-
        delta( Q, epsilon, S, New_Q, New_Ss ),
        append( New_Ss, Ss, Intermediate_Stack ),
        transform( New_Q, Xs, Intermediate_Stack, New_Stack ).

gibt es ein Problem, denn die Länge der positiv auftretenden Terme ist dann sowohl im Kopf der Klausel, als auch in dem Literal

        transform( New_Q, Xs, Intermediate_Stack, New_Stack )

gleich 0, was der Definition der konsistent geordeneten Programme widerspricht.

Wir stellen nun eine Technik zur Programmtransformation vor, mit deren Hilfe es in diesem Falle möglich ist, P_{M} in ein konsistent geordnetes Programm zu transformieren. Diese Technik ist in der Literatur als “Entfaltung” bekannt. Ist

(1)  Q : − L_{1}, ⋯, L_{i−1}, Q_{0}, L_{i+1}, ⋯, L_{n}.

eine Programm–Klausel aus einem Prolog–Programm P, sind

R_{1} : − K_{1}^{(1)}, ⋯, K_{m_{1}}^{(1)}

⋮

R_{k} : − K_{1}^{(k)}, ⋯, K_{m_{k}}^{(k)}

alle Klauseln aus P, deren Kopf mit Q_{0} unifizierbar ist, gilt weiter

μ_{1} = mgu(Q_{0}, R_{1}), ⋯, μ_{k} = mgu(Q_{0}, R_{k}),

so ist die Entfaltung der Klausel (1) bezüglich des Literals Q_{0} durch die k Klauseln

Qμ_{1} : − L_{1}μ_{1}, ⋯, L_{i−1}μ_{1}, K_{1}^{(1)}μ_{1}, ⋯, K_{m_{1}}^{(1)}μ_{1}, L_{i+1}μ_{1}, ⋯, L_{n}μ_{1}.
⋮
Qμ_{k} : − L_{1}μ_{k}, ⋯, L_{i−1}μ_{k}, K_{1}^{(k)}μ_{k}, ⋯, K_{m_{k}}^{(k)}μ_{k}, L_{i+1}μ_{k}, ⋯, L_{n}μ_{k}.

gegeben, durch die dann die Klausel (1) in dem ursprünglichen Programm ersetzt wird. Ist q ein Prädikatszeichen aus dem Programm P, so wird die vollständige Entfaltung von P bezüglich q dadurch erreicht, daß jede Klausel aus P, in deren Rumpf ein Literal Q̂ auftritt, welches das Prädikatszeichen q enthält, bezüglich Q̂ entfaltet wird. Anschließend werden alle Klauseln aus der Definition von q gestrichen. Dazu muß natürlich vorausgesetzt werden, daß die Definition von q nicht rekursiv ist. Das Prädikatszeichen q darf also nicht im Rumpf einer Klausel aus der Definition von q auftreten. Darüber hinaus darf q auch in keinem negativen Literal auftreten. Sind diese Bedingungen erfüllt, so ist die Beweiskraft des alten Programmes bezüglich der in dem “entfalteten” Programm noch auftretenden Prädikatszeichen die gleiche wie die Beweiskraft des entfalteten Programmes.

Entfalten wir unsere Programm P_{M} bezüglich der beiden Prädikatszeichen delta und append, so ergibt sich das folgende Programm:

accept( Xs ) :- initial( Q ), start( Z ),
                transform( Q, Xs, [ Z ], [] ).
transform( Q, [], Stack, Stack ).
transform( q_1, [ 0 | Xs ], [ r | Ss ], New_Stack ) :-
        transform( q_1, Xs, [ b, r | Ss ], New_Stack ).
transform( q_1, [ 1 | Xs ], [ r | Ss ], New_Stack ) :-
        transform( q_1, Xs, [ g, r | Ss], New_Stack ).
transform( q_1, [ 0 | Xs ], [ b | Ss ], New_Stack ) :-
        transform( q_1, Xs, [ b, b | Ss ], New_Stack ).
transform( q_1, [ 0 | Xs ], [ b | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
transform( q_1, [ 0 | Xs ], [ g | Ss ], New_Stack ) :-

        transform( q_1, Xs, [ b, g | Ss ], New_Stack ).
transform( q_1, [ 1 | Xs ], [ b | Ss ], New_Stack ) :-
        transform( q_1, Xs, [ g, b | Ss ], New_Stack ).
transform( q_1, [ 1 | Xs ], [ g | Ss ], New_Stack ) :-
        transform( q_1, Xs, [ g, g | Ss ], New_Stack ).
transform( q_1, [ 1 | Xs ], [ g | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
transform( q_2, [ 0 | Xs ], [ b | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
transform( q_2, [ 1 | Xs ], [ g | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
transform( q_1, Xs, [ r | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
transform( q_2, Xs, [ r | Ss ], New_Stack ) :-
        transform( q_2, Xs, Ss, New_Stack ).
initial( q_1 ).                         start( r ).

Dieses Programm ist mit den oben angegebenen Definitionen der Funktionen “level”, σ und “weight” konsistent geordnet.

8.3 Negative Beispiele

In diesem Abschnitt stellen wir einige Prolog–Programme vor, die sich nicht konsistent ordnen lassen und die sich auch nicht durch “Entfaltung” in konsistent geordnete Programme überführen lassen. Wir argumentieren, daß diese Programme sich nicht konsistent ordnen lassen, weil sie in irgendeiner Weise eine Suche enthalten, die sich a priori nicht in “einfacher” Weise beschränken läßt. Da dies keine mathematische Aussage ist, können wir auch keinen exakten Beweis für diese Behauptung liefern. Wir werden stattdessen versuchen, den Inhalt dieser Behauptung durch zwei charakteristische Beispiele klar zu machen. Wir beginnen mit einem Programm P_{A}, was dazu geeignet ist, die Ackermann– Funktion zu berechnen. Die 2-stellige Ackermann–Funktion f ist durch die Gleichungen

f(0, y) = y + 1, f(x + 1, 0) = f(x, 1) und f(x + 1, y + 1) = f(x, f(x + 1, y)) definiert. Diese Funktion wird von dem folgenden Programm berechnet:

ackermann( 0, Y, s(Y) ).
ackermann( s(X), 0, Z ) :- ackermann( X, s(0), Z ).
ackermann( s(X), s(Y), Z ) :- ackermann( s(X), Y, Z1 ),
                              ackermann( X, Z1, Z ).

Hier läßt sich weder die zweite noch die dritte Klausel konsistent ordnen. Bei der zweiten Klausel liegt der Grund dafür nicht sehr tief und ließe sich mit einer geringfügigen Änderung der Definitionen beseitigen. Wir könnten beispielsweise zulassen, daß die Gewichte von Funktionszeichen abhängig davon sind, an welcher Stelle im Prädikat das Funktionszeichen auftritt. Würden wir dann dem Funktionszeichen s an der ersten Stelle in dem Prädikat ackermann ein höheres Gewicht zuorden als an der zweiten Stelle, so wäre die zweite Klausel konsistent geordnet. Bei der dritten Klausel findet sich allerdings keine einfache Möglichkeit mehr, um die Definitionen so abzuändern, daß diese Klausel doch noch konsistent geordnet wird. Der Grund dafür ist in dem Auftreten der Variable Z1 zu suchen, die im Kopf der Klausel nicht auftritt. Deren Wert hängt in sehr komplizierter (nämlich nicht primitiv–rekursiver) Weise von dem Wert der Variablen X und Y im Kopf der Klausel ab.

Als weiteres Beispiel betrachten wir ein Programm, das in der Lage ist zu entscheiden, ob zwischen zwei Knoten in einem endlichen gerichteten Graphen eine Verbindung besteht. Es handelt sich dabei um das Programm 14.10 aus [StSh86]:

connected( X, Y ) :- connected( X, Y, [X] ).
connected( A, A, Visited ).
connected( A, B, Visited ) :- edge( A, N ),
                              not member(N, Visited),
                              connected( N, B, [ N | Visited ] ).
member( X, [ X | Xs ] ).
member( X, [ Y | Ys ] ) :- member( X, Ys ).

Zusätzlich enthält das Programm Fakten der Form edge(a,b), die die Struktur des zugrundeliegenden Graphen beschreiben. Zwar ist bei diesem Programm durch die Forderung, daß der Graph endlich ist, sichergestellt, daß es keine unendlichen Berechnungen gibt. Dies ist aber in einfacher Weise erst auf einer Metaebene einsehbar, denn in der letzten Klausel zu dem 3–stelligen Prädikat connected tritt das Prädikat connected selbst wieder im Rumpf auf, und zwar mit einer Termstruktur, die komplizierter ist als die Termstruktur des Kopfes.

Literaturverzeichnis

[Apt90] K.R. Apt, Logic Programming, Handbook of Theoretical Computer Science Volume B, Jan van Leeuwen (Editor), Elsevier, 1990, S. 493– 574

[Cl78] K.L. Clark, Negation as failure, H. Gallaire und J. Minker (eds), Plenum Press, New York, 1978, S. 293–322

[Cl79] K.L. Clark, Predicate Logic as a Computational Formalism, Research Report DOC 79/59, Department of Computing, Imperial Colledge, 1979

[CB83] J. Corbin und M. Bidoit, A rehabilitation of Robinsons unification algorithm, Information Processing 83, 1983, S. 909–914

[FH86] F. Fages und G. Huet, Complete set of unifiers and matchers in equational theories, Theoretical Computer Science 43, 1986, s: 189– 200

[HK89] D. Hofbauer, R.–D. Kutsche, Grundlagen des maschinellen Beweisens, Vieweg 1989

[HoUl79] J.E. Hopcroft und J.D. Ullman, Introduction to Automata Theory, Languages and Computation, Addison–Wesley, Reading, Massachussets, 1979

[Knight89] K. Knight, Unification: A multidisciplinary survey, ACM Comp. Surveys 21(1), 1989, S. 93–124

[Llo87] J.W. Lloyd, Foundations of Logic Programming, Springer 1987

[LT86] J.W. Lloyd und R.W. Topor, A Basis for Deductive Database Systems II, Journal of Logic Programming 3, 1 (1986), S. 55–67

[Pad88] P. Padawitz, Computing in Horn Clause Theories Springer, 1988

[Poh89] W. Pohlers, Proof Theory, LNM 1407, Springer, 1989 [Reit78] R. Reiter, On Closed World Data Bases, H. Gallaire und J. Minker

(eds), Plenum Press, New York, 1978, S. 55–76

[Rob65] J.A. Robinson, A Machine–oriented Logic Based on the Resolution Principle, Journal of the ACM 12, 1, S. 23–41

[Shep85] J.C. Shepherdson, Negation as failure II, Journal of Logic Programming 2, 3 (1985), S. 185–202

[Siek89] J. Siekmann, Unification theory, Journal of Symbolic Computation 7, 1989, S.207–274

[StSh86] L. Sterling und E. Shapiro, The Art of Prolog, MIT Press 1986

[Str90] K. Stroetmann, Ein Vollständigkeitssatz für normale Prolog–Programme mit I/O–Spezifikationen, Interner Bericht des Instituts für mathematische Logik und Grundlagenforschung, Münster (1990)

Lebenslauf und Bildungsgang

Name  Karl Stroetmann
geboren  am 7. 4. 1961 in Ascheberg in Westfalen
Eltern  Josef Stroetmann und

Johanna–Maria Stroetmann geb. Söding

1967 – 1971  Besuch der Grundschule in Ascheberg
1971 – 1980  Besuch des Gymnasium Canisianum in Lüdinghausen
9. 5. 1980  Abitur
1. 7. 1980 – 30. 6. 1982 Zeitsoldat bei der Bundeswehr
WS 1980 – SS 1982  Studium der Mathematik mit dem Nebenfach

Elektrotechnik an der Fernuniversität Hagen

WS 1982  Aufnahme des Studiums der Physik an der

Westfälischen Wilhelms–Universität Münster

1. 11. 1983 – 30. 4. 1987 Studentische Hilfskraft am

Institut für Theoretische Physik II

1. 10. 1983 – 31. 3. 1986 Studentische Hilfskraft am Fachbereich Mathematik
2. 4. 1984  Diplom–Vorprüfung im Fach Physik
2. 4. 1984  Diplom–Vorprüfung im Fach Mathematik
WS 1985  Beginn der Diplomarbeit
29. 4. 1987  Diplom im Fach Physik

Thema der Diplomarbeit:

Das Pseudopotential im Lithium–Kristall

1. 5. 1987 – 30. 11. 1988 Wissenschaftlicher Mitarbeiter am Institut

für Numerische und Instrumentelle Mathematik an der WWU Münster

1. 12. 1988 – 31. 5. 1989 Wissenschaftliche Hilfskraft am Institut

für mathematische Logik und Grundlagenforschung an der WWU Münster

1. 12. 1988  Beginn mit den Arbeiten zur Dissertation
seit dem 1. 6. 1989  Wissenschaftlicher Mitarbeiter am Institut für

mathematische Logik und Grundlagenforschung an der WWU Münster