Logikprogrammierung

Prof. Dr. M. Hanus

Lehr- und Forschungsgebiet Informatik II Rheinisch-Westfälische Technische Hochschule Aachen Ahornstraße 55, 52072 Aachen WWW:

http://www-users.informatik.rwth-aachen.de/~leucker/lp/index.html

SS 1995

Skript: \begin{matrix}c \\ ◯ \end{matrix}1996–1999 Hans-Georg Eßer, Roermonder Str. 42, 52072 Aachen

                        h.g.esser@gmx.de
               WWW: http://home.pages.de/~hge/

Inhaltsverzeichnis

1 Elementare Einführung in Prolog 3

2 Objekte in Prolog 7 2.1 Zahlen, Atome und Strukturen . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Listen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Operatoren . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.4 Variablen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.5 Gleichheit von Termen . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Beweisen mit dem Resolutionsprinzip 10 3.1 Einfaches Resolutionsprinzip . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Unifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.3 Allgemeines Resolutionsprinzip . . . . . . . . . . . . . . . . . . . . . 14 3.4 Gleichheit in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

4 Elementare Programmiertechniken 15 4.1 Aufzählung des Suchbaums . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Musterorientierte Wissensrepräsentation . . . . . . . . . . . . . . . . 17 4.3 Verwendung von Relationen . . . . . . . . . . . . . . . . . . . . . . . 19 4.4 Datenstrukturen als Fakten . . . . . . . . . . . . . . . . . . . . . . . 20

5 Theoretische Grundlagen der Logikprogrammierung 22 5.1 Aufbau logischer Programme . . . . . . . . . . . . . . . . . . . . . . . 22 5.2 Interpretationen und Modelle für Formeln . . . . . . . . . . . . . . . 25 5.3 Fixpunkte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.4 Deklarative Semantik logischer Programme . . . . . . . . . . . . . . . 33 5.5 Beweisen mit logischen Programmen . . . . . . . . . . . . . . . . . . 35

5.6 Beweisen in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

6 Nichtdeklarative Bestandteile von Prolog 44 6.1 Beweisstrategie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6.2 Der ”Cut“-Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 6.3 Negation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 6.4 Zyklische Strukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 6.5 Arithmetik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.6 Ein-/Ausgabe von Daten . . . . . . . . . . . . . . . . . . . . . . . . . 53 6.7 Zerlegung und Konstruktion von Termen . . . . . . . . . . . . . . . . 55 6.8 Daten als Programme . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 6.9 Programme als Daten . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

7 Fortgeschrittene Programmiertechniken 57 7.1 Differenzlisten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 7.2 Meta-Interpretierer . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 7.3 Debugging von Prolog-Programmen . . . . . . . . . . . . . . . . . . . 60

8 Erweiterungen der reinen Logikprogrammierung 61 8.1 Flexible Berechnungsregeln . . . . . . . . . . . . . . . . . . . . . . . . 61 8.2 Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

9 Implementierungen von Prolog 65 9.1 Grundideen der Warren Abstract Machine . . . . . . . . . . . . . . . 66 9.2 Die Warren Abstract Machine (WAM) . . . . . . . . . . . . . . . . . 70

9.2.1 Speicherbereiche und Register der WAM . . . . . . . . . . . . 70 9.2.2 Instruktionssatz . . . . . . . . . . . . . . . . . . . . . . . . . . 72

9.3 Globale Analyse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

Zu diesem Skript

Das vorliegende Skript wurde von mir auf der Grundlage einer Vorlesungsmitschrift aus dem Sommersemester 1995 erstellt. Dies ist kein offizielles Skript des Lehrstuhls. Zwar habe ich mich bei der Erstellung bemüht, Fehler meiner handschriftlichen Mitschrift zu korrigieren, kann aber natürlich keine Garantie für die Korrektheit übernehmen.

Dieses Skript darf nicht kommerziell, wohl aber privat und unentgeltlich weiterverbreitet werden (sofern nicht das Urheberrecht von Prof. Hanus dies verbietet), für Anregungen und Fehlerhinweise an meine Email-Adresse h.g.esser@gmx.de wäre ich dankbar.

Außer dem Skript zur Vorlesung Logikprogrammierung habe ich auch Skripte zur Funktionalen Programmierung aus dem Wintersemester 1995/96 von Prof. Indermark und zur Vorlesung Approximationstheorie I aus dem Wintersemester 1995/96 von Prof. Stens erstellt.

Zu dieser Vorlesung

Die in der Vorlesung Logikprogrammierung verwendete Sprache ist Prolog. Gründe dafür sind, daß Prolog weit verbreitet und ein de facto-Standard für Logiksprachen ist und es viele Implementierungen gibt (siehe dazu das FAQ in der Newsgroup

comp.lang.prolog).

Nachteil: es gibt wenig Konzepte für große Systeme.

Entstehung

1965: Robinsons Resolutionsprinzip (Grundlage zum Arbeiten) 1972-73: Colmeraner, Roussel (Marseille): Effiziente Implementierung der

Resolution ⇝ Prolog

1974: Kowalski: Predicate Logic as Programming Language

⇝ Rechnen = Beweisen

1977: Pereira/Warren: DEC-10-Prolog (Übersetzer in MC-Code)

Anwendungen: Expertensysteme, Verarbeitung natürlicher Sprache, Datenbank, Übersetzerbau, Symbolische Mathematik

1981: Prolog als Implementierungssprache von Japans fünfter Computergeneration (5th generation project)

Eigenschaften:

+ Einfache Syntax

+ Klares Grundkonzept

+ Einfache Semantik (mathematische Strukturen)

+ Prototyping, Symbolverarbeitung einfach

– Programmausführung häufig nicht so effizient

– Speicherintensiv

– Noch kein Standard für Module und Typen

1 Elementare Einführung in Prolog

Prinzip der Logikprogrammierung

• Formulierung der logischen Zusammenhänge des Problems,

• Lösungsfindung ist Aufgabe des Rechners.

Programmierer der Logikprogrammierung beschreiben nicht, wie das Problem gelöst wird, sondern was das Problem ist.

Eingabe:

– Wissen über das Problem.

– Anfrage: ”Ist die Aussage richtig?“ bzw. ”Für welche Werte ist eine Aussage richtig?“ Ausgabe: yes/no bzw. Werte für Variablen Wissen:

1. Eigenschaften und Beziehungen:

”Rot ist eine Farbe“, ”16 ist größer als 5“

2. Regeln zur Ableitung neuer Tatsachen: ”Wenn 16 größer als 5 ist und 5 größer als 2, dann ist auch 16 größer als 2.“

Beispiel: Verwandtschaftsbeziehungen Ziel: ”Wer ist die Mutter von Monika?“, ”Welche Großväter hat Andreas?“

Lösung 1: Speicherung sämtlicher Beziehungen. Nachteil: Aufwendig, unflexibel bei Änderungen, fehleranfällig.

Lösung 2: Speichere nur elementare Beziehungen, die übrigen werden durch Regeln definiert.

Elementare Beziehungen:

1. männlich / weiblich

2. Wer ist mit wem verheiratet?

3. Wer ist die Mutter?

[figure: christine ◯◯ heinz; maria ◯◯ fritz; monika ◯◯ herbert; angelika ◯◯ hubert; susanne; norbert; andreas]

Ableitbar: angelika ist Tante von susanne.

Berechnungsprinzip von Prolog: Eingabe: Tatsachen und Regeln. Prolog-System sucht Antworten durch Anwendung von Tatsachen und Regeln.

Prolog-Syntax Aussagen:

• ”3 ist ungerade“ (Objekt: 3, Art der Aussage/Name: ”ist ungerade“)

• ”monika ist mit herbert verheiratet“ (Objekte: monika, herbert, Art der Aussage/Name: verheiratet)

In Prolog: name(objekt_{1}, ..., objekt_{n})

ungerade (3)
verheiratet (monika, herbert)

Anmerkungen:

1. Alle Namen werden klein geschrieben.

2. Die Reihenfolge der Objekte ist relevant.

3. Andere Schreibweisen: → Operatoren (später)

Solche Aussagen heißen Fakten.

weiblich (christine).
weiblich (maria).
weiblich (monika).
weiblich (angelika).
weiblich (susanne).
maennlich (heinz).
maennlich (fritz).
maennlich (herbert).
maennlich (hubert).
maennlich (norbert).
maennlich (andreas).
verheiratet (christine,heinz).
...
istMutterVon (christine,herbert).
...

Regeln in Prolog

                   Aussage3 :- Aussage1, Aussage2.

Beispiel:

istVaterVon (herbert,susanne) :-
     verheiratet (monika,herbert),
     istMutterVon (monika,susanne).

Weitere Regel: dieselbe Regel mit maria statt monika.

Ausweg: statt unendlich vieler Regeln: Variablen (unbekannte Objekte) → beginnen mit Großbuchstaben

⇒ istVaterVon(V,K) :- verheiratet(M,V), istMutterVon(M,K).

entspricht unendlich vielen konkreten Regeln.

istGrossvater(G,E) :- istVaterVon(G,V), istVaterVon(V,E).

Anfragen:

   • ?- verheiratet (maria,fritz).
     ⇝ yes
   • ?- verheiratet (monika,M).
     ⇝ M = herbert
   • ?- istGrossvater(heinz,E).
     ⇝ E = susanne ;
     E = norbert ;
     no

Klauseln: Fakten/Regeln für Eigenschaften/Beziehungen (Prädikate und Relationen) → relationale Programmierung

Anfrage: Frage, ob Aussagen wahr/falsch sind bezüglich des vorhandenen Wissens (!)

Soweit: Prolog ⊆ \underbrace{Prädikatenlogik erster Stufe}_{unentscheidbar}

⇒ Auch Prolog-Programme terminieren nicht in jedem Fall. Beispiel: Interpreter für Pascal: möglich in Prolog (Endlosschleife ausführen)

Vergleich Prolog / imperative Sprachen:

Prolog  imperative Sprachen

Problemwissen angeben

Operationen (Algorithmus) angeben

Rechner sucht Lösung

Rechner arbeitet Operationen ab

Logisches Schließen sollte bekannt sein Aufbau des von-Neumann-Rechners sollte bekannt sein, ebenso Semantik der Sprache

Variablen in Prolog = unbekannte Objekte

Variablen = Speicherzellen

Rechnen = Beweisen Rechnen = Manipulation von Speicherzellen

Aber: beide Sprachtypen haben gleiche Mächtigkeit.

2 Objekte in Prolog

”Wissen“ entspricht Aussagen über abstrakte Objekte: Aus der realen Person ”Susanne“ wird durch Abstraktion das Objekt susanne oder (susanne,schmidt,geb.3.4.60).

2.1 Zahlen, Atome und Strukturen

Wir unterscheiden vier Kategorien von Zeichen:

• GBs := { A, B, ..., Z },

• KBs := { a, b, ..., z },

• Zif := { 0, 1, ..., 9 },

• SZ := { +, −, ∗, /, <, =, >, ‘, \,:, .,?, @, #, $, &, ^, ~ }. Zahlen: Folgen von Ziffern (auch Gleitkommazahlen) Atome:

• Folge von KBs, GBs, Zif und ’_’, die mit KBs beginnt (z.B. susanne_schmidt)

• Folge von SZ (z.B. :-, ==>)

• beliebige Zeichenfolge in einfachen Anführungszeichen (z.B. 'haLL?o')

• Atome mit besonderer Bedeutung: , ; ! [] Konstanten: Zahlen oder Atome Beispiel: Relation geboren: Fakten der Form geboren (fritz,1,6,27). Beobachtung: 1,6,27 sind drei einzelne Objekte, sie sollten aber besser ein Objekt bilden. Strukturen: Zusammenfassung von mehreren Objekten zu einem. Darstellung: datum(1,6,27) mit Funktor datum und Komponenten 1,6,27.

→ geboren (fritz, datum(1,6,27)) (zweistellige Relation)

Der Funktor ist dabei relevant: datum(9,6,35) ≠ zeit(9,6,35). Auch geschachtel-

te Strukturen sind möglich, z.B. person(susanne,schmidt,datum(3,4,60)).

2.2 Listen

Definition (Listen) Listen werden induktiv über die folgenden beiden Fälle definiert:

• Die leere Liste [] ist eine Liste.

8 2 OBJEKTE IN PROLOG

• Wenn L eine Liste ist und E beliebig, dann ist .(E,L) eine Liste. Beispiel: Liste mit Elementen a,b,c: .(a,.(b,.(c,[]))) Notationen:

• [E1,E2,...,En] = Liste mit den Elementen E_{1}, ..., E_{n}

• [E|L] = Liste mit Anfang E und Rest L (=.(E,L))

Beispiel: [a,b,c] = [a|[b,c]] = [a|[b|[c|[]]]]

Texte: Liste von ASCII-Werten. Notation: “Prolog“ → [80,114,111,108,111,103]

2.3 Operatoren

”Summe der Zahl 1 und Produkt aus 3 und 4“: +(1,*(3,4)). Natürliche Schreibweise: 1 + 3 ∗ 4 (mit Infixoperatoren +, ∗) Operatorschreibweise:

1. Strukturen mit einer Komponente:

(a) Präfixoperator: -2 steht für −(2),

(b) Postfixoperator: 2 fak fak steht für fak(fak(2))

2. Strukturen mit zwei Komponenten:

Infixoperator: 2+3 ist +(2, 3) Problem: Eindeutigkeit

(a) 1-2-3 steht für −(−(1, 2), 3) (linksassoziativ) oder −(1, −(2, 3)) (rechtsassoziativ),

(b) 12/6+1 steht für +(/(12, 6), 1) (/ hat kleinere Präzedenz als +) oder /(12, +(6, 1)) (andersrum). Behebung:

1. Der Prolog-Benutzer kann Operatoren mit Assoziativität und Präzedenz definieren,

2. Übliche mathematische Operatoren (+, −, ∗, /) sind vordefiniert,

3. Das Setzen von Klammern ist immer möglich, z.B. 12/(6+1).

2.4 Variablen

Variablen sind unbekannte Objekte, die durch Variablennamen repräsentiert werden: Folgen von GBs, KBs, ’ ’, beginnend mit GBs. Beispiel:

• datum(1,4,Jahr): alle ersten Apriltage

• [A,B|L]: alle Listen mit mindestens zwei Elementen Gleiche Variablennamen sind gleiche Objekte:

• [E,E|L]: Liste mit zwei identischen Anfangselementen und beliebigem Rest Anonyme Variable: _für Objekte, deren Werte nicht interessieren, z.B.

?- istGrossvaterVon(G,_) ⇝ G = ...,
istEhemann(P) :- verheiratet(_,P).

Term: Terme sind Konstanten, Variablen und Strukturen (= Prolog-Objekte), Terme ohne Variablen heißen Grundterm. Beispiel: Listenstrukturen: Prädikat member(E,L) wahr, falls E in L vorkommt: Intuitive Lösung:

• E ist erstes Element von L → wahr

• E ist zweites Element von L → wahr

• ... Bessere Lösung:

• E ist erstes Element von L → wahr

• E im Rest von L → wahr Implementierung:

  member(E,[E|_]).
  member(E,[_|R]) :- member(E,R).

2.5 Gleichheit von Termen

Relevant: Suche von passenden Fakten und Regeln. Der Begriff der Gleichheit von Termen ist nicht trivial – gilt z.B. 5 = 2 + 3? Definition (Termgleichheit)

1. Zahlen und Atome sind nur zu sich selbst gleich.

10 3 BEWEISEN MIT DEM RESOLUTIONSPRINZIP 2. Variablen sind gleich, wenn sie den gleichen Namen haben.

3. Strukturen sind gleich, wenn • der Funktor gleich ist,

• sie die gleiche Anzahl von Komponenten haben,

• die Komponenten paarweise gleich sind ⇒ 5 und 2+3 sind nicht gleich. Andererseits sind 2∗2 und ∗(2, 2) gleich. (Vergleiche Indermark: ”abstrakte Syntax“). verheiratet(M, fritz) und verheiratet(maria, fritz) sind gleich, wenn M durch maria ersetzt wird ⇒ Unifikation. Zwei Gleichheitsbegriffe:

1. Termgleichheit (s.o.), in Prolog: s==t

2. Unifizierbarkeit, in Prolog: s=t

3 Beweisen mit dem Resolutionsprinzip

3.1 Einfaches Resolutionsprinzip

Literal: Aussage über Objekte: p(O_{1}, ..., O_{n}) (p: Art der Aussage, O_{i}: Terme) Fakten sind Literale, die immer richtig sind, z.B. maennlich(herbert). Vorsicht:

maennlich(maria). (??)

→ Jedes Faktum ist eine beweisbare Aussage. Regeln: L : −L_{1}, ..., L_{n}. (L, L_{i} Literale, keine Negation). Logisch: (L_{1} ∧ ... ∧ L_{n} ⇒ L) ≡ ¬L_{1} ∨ ¬L_{2} ∨ ...¬L_{n} ∨ L. Semantik: Wenn L : −L_{1}, ..., L_{n} eine Regel ist und L_{1}, ..., L_{n} beweisbar sind, dann ist auch L beweisbar. (Modus ponens, Abtrennungsregel) Anfrage: Aussagen, die überprüft werden sollen: ? − L_{1}, ..., L_{n} Semantik: Sind L_{1}, ...L_{n} beweisbar bezüglich der Fakten und Regeln? Beweisen durch Umkehrung des modus ponens: Definition (Resolutionsprinzip, einfach) Eine Aussage L ist beweisbar, falls

• L : −L_{1}, ..., L_{n} eine Regel ist und

• jedes L_{i} beweisbar ist.

Spezialfall: Fakten (n = 0).

Anwendung:

(1) verheiratet (monika,herbert).

(2) istMutterVon (monika,susanne).

(3) istVaterVon (herbert,susanne) :– verheiratet (monika,herbert), istMutterVon (monika,susanne). ?- istVaterVon(herbert,susanne). ⊢_{(3)} ?- verheiratet(monika,herbert), istMutterVon(monika,susanne). ⊢_{(1)} ?- istMutterVon(monika,susanne). ⊢_{(2)} ?- .

Kann eine Anfrage mit dem Resolutionsprinzip auf eine leere Anfrage reduziert werden, dann ist sie beweisbar.

Aspekte:

1. Nichtdeterminismus (mehrere Literale, mehrere Klauseln)

2. Nichtterminierung:

Beispiel: p(a) :- p(a).

?- p(a). ⊢ ?- p(a). ⊢ ?- p(a). ⊢ ...

Negation: p(a) : −¬p(a). ⟺ (¬p(a) ⇒ p(a)) ⟺ (¬¬p(a) ∨ p(a)) ⟺ p(a) ?- p(a). ⊢ ?- ¬p(a). ⊢ ?- p(a). ⊢ ...

3.2 Unifikation

Problem: istGrossvaterVon(X,Z) :– istVaterVon(X,Y), istVaterVon(Y,Z). ?– istGrossvaterVon(heinz,E).

Semantik von Variablen: Ersetze X durch heinz, Z durch E.

Definition (Substitution) Eine Abbildung σ, die auf den Termen definiert ist, Variablen durch Terme ersetzt und die folgenden Eigenschaften erfüllt, heißt Substitution:

1. Für alle f(t_{1}, ..., t_{n}) gilt σ(f(t_{1}, ..., t_{n})) := f(σ(t_{1}), ..., σ(t_{n})) (strukturerhaltend, Homomorphismus) (analog für Literale),

2. Die Menge {X|X Variable mit σ(X) ≠ X} ist endlich.

Daraus ergibt sich eine eindeutige Darstellung von Substitutionen durch

{X/σ(X) | X Variable und σ(X) ≠ X}

Beispiel: σ = {X/heinz, Z/E} σ(istGrossvaterV on(X, Z) = istGrossvaterV on(heinz, E).

Problem: verheiratet (maria,fritz). ?– verheiratet (maria,M). (M ⇝ fritz) Das führt zur Unifikation: Anpassung von Termen durch Variablenersetzung.

Beispiel: Unifikation ist nicht eindeutig: datum(T ag, Monat, 83) und datum(3, M, J)

• σ_{1} = {T ag/3, Monat/4, M/4, J/83}

• σ_{2} = {T ag/3, Monat/M, J/83}

σ_{1} und σ_{2} machen die Terme gleich, aber σ_{1} ist zu speziell.

Definition (Unifikator)

• Eine Substitution σ heißt Unifikator für t_{1} und t_{2}, falls σ(t_{1}) = σ(t_{2}). Dann heißen t_{1} und t_{2} unifizierbar.

• Ein Unifikator σ heißt allgemeinster Unifikator (mgu, most general unifier), falls für jeden Unifikator σ′ eine Substitution φ mit σ′ = φ ∘ σ existiert.

Mgu’s sind effektiv berechenbar (Robinson 1965).

Definition (Unstimmigkeitsmenge) Seien t, t′ Terme. Die Unstimmigkeitsmenge (disagreement set) ds(t, t′) wird definiert durch:

1. t = t′ ⇒ ds(t, t′) = ∅

2. t Variable, t ≠ t′ ⇒ ds(t, t′) = {t, t′}

3. t′ Variable, t ≠ t′ ⇒ ds(t, t′) = {t, t′}

4. t = f(t_{1}, ..., t_{n}), t′ = g(s_{1}, ..., s_{m}), n, m ≥ 0

• Falls f ≠ g oder m ≠ n ⇒ ds(t, t′) = {t, t′}

• Falls f = g, m = n und t_{i} = s_{i} für i = 1, ..., k −1 und t_{k} ≠ s_{k} ⇒ ds(t, t′) = ds(t_{k}, s_{k})

Unifikationsalgorithmus Eingabe: Terme t_{0}, t_{1} Ausgabe: mgu σ für t_{0}, t_{1}, falls diese unifizierbar sind, ansonsten ”fail“.

1. k := 0, σ_{0} := {} 2. Falls σ_{k}(t_{0}) = σ_{k}(t_{1}), dann ”σ_{k} ist mgu“

3. Falls ds(σ_{k}(t_{0}), σ_{k}(t_{1})) = {x, t} (mit x Variable, die nicht in t vorkommt), dann σ_{k+1} := {x/t} ∘ σ_{k}; k := k + 1; goto 2 sonst ”fail“

Beispiel

1. t_{0} = verheiratet(monika, M), t_{1} = verheiratet(F, herbert)

ds(t_{0}, t_{1}) = {F, monika} ⇒ σ_{1} = {F/monika} ds(σ_{1}t_{0}, σ_{1}t_{1}) = {M, herbert} ⇒ σ_{2} = {M/herbert}∘σ_{1} = {M/herbert, F/monika} σ_{2}t_{0} = σ_{2}t_{1} = verheiratet(monika, herbert) ⇒ σ_{2} ist mgu.

2. t_{0} = equ(f(1), g(X)), t_{1} = equ(Y, Y)

ds(t_{0}, t_{1}) = {Y, f(1)} ⇒ σ_{1} = {Y/f(1)} ds(σ_{1}t_{0}, σ_{1}t_{1}) = {g(X), f(1)} ⇒ ”fail“

3. t_{0} = X, t_{1} = f(X)

ds(t_{0}, t_{1}) = {X, f(X)} ⇒ ”fail“ (da X in f(X) vorkommt)

Die Abfrage ”x in t?“ im Algorithmus heißt occur check (Vorkommenstest); sie kostet Zeit, ist aber in der Praxis selten erfolgreich. Daher gibt es in vielen Prolog-Systemen keinen occur check. Dies führt eventuell zu fehlerhafter Unifikation: Erzeugung zyklischer Terme: X = f(X) ⇒ {X/f(f(f(f(... } (Korrektheit)

Satz (Unifikationssatz von Robinson) Seien t_{0}, t_{1} Terme. Falls t_{0} und t_{1} unifizierbar sind, dann gibt der obige Algorithmus einen mgu aus, ansonsten ”fail“.

Konsequenz: Unifizierbare Terme haben immer einen mgu.

Beweis:

• Terminierung:

1. Schleifendurchlauf nur, falls ds(σ_{k}t_{0}, σ_{k}t_{1}) mindestens eine Variable enthält.

2. In jedem Durchlauf wird eine Variable eliminiert (d.h. in σ_{k+1}t_{i} (i = 0, 1) kommt x nicht vor)

3. t_{0}, t_{1} enthalten nur endlich viele Variablen

Aus 1-3 folgt, daß es nur endlich viele Schleifendurchläufe geben kann, also ist der Algorithmus terminierend.

• Korrektheit:

1. t_{0}, t_{1} nicht unifizierbar: Falls der Algorithmus in Schritt 2 hielte, wären t_{0}, t_{1} doch unifizierbar. Also muß der Algorithmus wegen der Terminierungseigenschaft in Schritt 3 halten. ⇒ er gibt ”fail“ aus.

2. t_{0}, t_{1} unifizierbar: Sie θ ein beliebiger Unifikator für t_{0}, t_{1}. Zu zeigen ist: Für alle k ≥ 0 gibt es eine Substitution γ_{k} mit θ = γ_{k} ∘ σ_{k}, und im k-ten Durchlauf wird nicht ”fail“ ausgegeben (dann folgt wegen der Terminierung, daß die Ausgabe tatsächlich ein mgu ist). Beweis durch Induktion über k: k = 0: Sei γ_{k} := θ. Dann: γ_{0} ∘ σ_{0} = θ ∘ {} = θ. k → k + 1: Induktionsvoraussetzung: θ = γ_{k} ∘ σ_{k}, d.h. γ_{k} ist ein Unifikator für σ_{k}t_{0} und σ_{k}t_{1}. Entweder: σ_{k}t_{0} = σ_{k}t_{1}: Dann gibt es keinen (k+1)-ten Schleifendurchlauf. Oder: σ_{k}t_{0} ≠ σ_{k}t_{1}. Also: ∅ ≠ ds(σ_{k}t_{0}, σ_{k}t_{1}) = {x, t}, und x nicht in t (anderenfalls σ_{k}t_{0}, σ_{k}t_{1} nicht unifizierbar) ⇒ im (k+1)-ten Schleifendurchlauf keine Ausgabe von ”fail“ und σ_{k+1} = {x/t} ∘ σ_{k}. Sei γ_{k+1} := γ_{k} \ {x/γ_{k}(x)} (d.h. nehme Ersetzung für x aus γ_{k}). Dann: γ_{k+1} ∘ σ_{k+1} = γ_{k+1} ∘ {x/t} ∘ σ_{k} = {x/γ_{k+1}(t)} ∘ γ_{k+1} ∘ σ_{k} (da x von γ_{k+1} nicht ersetzt wird) = {x/γ_{k}(t)} ∘ γ_{k+1} ∘ σ_{k} (da x nicht in t) = γ_{k} ∘ σ_{k} (Definition von γ_{k+1}) = θ (nach Induktionsvoraussetzung) Also ist die Induktionsbehauptung wahr.

Komplexität: Im schlechtesten Fall exponentielle Laufzeit bezüglich der Größe der Eingabeterme (das liegt an exponentiell wachsenden Termen).

Anmerkungen:

1. Auch ohne Vorkommenstest ist die Laufzeit exponentiell, da die exponentiell wachsenden Terme aufgebaut werden müssen.

2. Ausweg: keine explizite Darstellung der Terme, sondern Graphen zur Darstellung ⇒ Laufzeitverbesserung bis zu linearen (!) Algorithmen [Martelli, Montenari], [Paterson, Wegman]

3. In der Praxis sind exponentiell wachsende Terme äußerst selten ⇒ klassische Algorithmen mit ”sharing“ von Variablen sind ausreichend (→ Implementierung)

3.3 Allgemeines Resolutionsprinzip

Definition (allgemeines Resolutionsprinzip) Der Beweis der Anfrage ? − A_{1}, ..., A_{m} kann reduziert werden auf den Beweis der Anfrage

? − σ(A_{1}, ..., A_{i−1}, L_{1}, ..., L_{n}, A_{i+1}, ..., A_{m})

wenn L : −L_{1}, ..., L_{n} eine Regel (mit neuen Variablen) und σ ein mgu für A_{i} und L sind.

Freiheiten:

1. Welches Literal A_{i} wird im nächsten Schritt ausgewählt?

2. Welche Regel wird ausprobiert?

Genaueres dazu später (Resolution mit Auswahlregeln; Kapitel 5)

Beweisen mit Resolutionsprinzip

Programm: istVaterVon(hans,peter).
  istVaterVon(peter,frank).
  istOpaVon(X,Z) :- istVaterVon(X,Y), istVaterVon(Y,Z).

Beweis:

?- istOpaVon (hans,E).

⊢ (Resolutionsschritt mit mgu σ_{1} = {X/hans, Z/E})

?- istVaterVon (hans,Y), istVaterVon (Y,E).

⊢ (σ_{2} = {Y/peter} ∘ σ_{1})

?- istVaterVon (peter,E).

⊢ (σ_{3} = {E/frank} ∘ σ_{2})

?- .

(Ausgabe: E=frank)

3.4 Gleichheit in Prolog

In Prolog ist für das Prädikat ”=“ die Klausel =(X,X). vordefiniert; es gibt keine weiteren Klauseln für =. Außerdem kann = als Infixoperator verwendet werden (X=X). Als Konsequenz ist die Anfrage ? − t_{1} = t_{2} genau dann beweisbar, wenn t_{1} und t_{2} unifizierbar sind. Beispiel:

   • ?- 3+2=5. → no
   • [X|Y]=[1]. → X = 1, Y = []

4 Elementare Programmiertechniken

4.1 Aufzählung des Suchbaums

Beispiel: Färben einer Landkarte

1  23  4

Zur Verfügung stehen vier Farben: rot, gelb, grün, blau. Problem: Die Landkarte ist so einzufärben, daß aneinandergrenzende Länder unterschiedlich gefärbt sind.

Wissen:

1. Vier Farben:

farbe(rot).
farbe(gelb).
farbe(gruen).
farbe(blau).

2. Jedes Land hat eine Farbe:

faerbung(L1,L2,L3,L4) :- farbe(L1),farbe(L2),farbe(L3),farbe(L4).

3. Ungleiche Farben:

verschieden(rot,gelb).
verschieden(rot,gruen).
...

4. Korrekte Lösungen:

korrekteFaerbung(L1,L2,L3,L4) :-
verschieden(L1,L2), verschieden(L1,L3), verschieden(L2,L3),
verschieden(L2,L4), verschieden(L3,L4).

5. Gesamtlösung:

?- faerbung(L1,L2,L3,L4), korrekteFaerbung(L1,L2,L3,L4).

liefert:

L1=rot, L2=gelb, L3=gruen, L4=rot

Analyse:

• Typisches Beispiel, ohne Algorithmus zur Lösung.

• Wissen entspricht Angabe über Lösungen.

• Aber: es gibt unendlich viele Prolog-Objekte.

• Daher: Einschränkung der Menge der potentiellen Lösungen (Suchraum); hier: faerbung(L1,..,L4)

• Schema:

loesung(L) :- moeglicheLoesung(L), korrekteLoesung(L) Der Suchraum sollte möglichst klein sein.

• Komplexität: hier: 4^{4} = 256 mögliche Lösungen

Beispiel: Sortieren von Zahlen: sortiere(UL,SL) mit einer beliebigen Liste UL von Zahlen (SL sortierte Liste)

1. Wann ist eine Liste sortiert?

sortiert([]).
sortiert([_]).
sortiert([E1,E2|L]) :- E1=<E2, sortiert([E2|L]).

2. Mögliche Lösungen: SL ist eine Permutation von UL

perm([],[]).
perm(L1,[E2|R2]) :- streiche(E2,L1,R1), perm(R1,R2).
3. streiche(E,L,R): E ∈ L, R = L \ {E}
streiche(E,[E|R],R).
streiche(E,[A|R],[A|RohneE]) :- streiche(E,R,RohneE).

(perm kann nicht symmetrisch definiert werden; unzureichende Auswertungsstrategie von Prolog)

4. Gesamtlösung:

sortiere(UL,SL) :- perm(UL,SL), sortiert(SL).

5. Anfrage:

?- sortiere([3,1,4,2],SL).

SL = [1, 2, 3, 4]

6. Komplexität: Suchraum = Menge aller Permutationen |UL| = n ⇒ |Suchraum| = n! Praktisch unbrauchbar ⇒ Nutze Wissen über bessere Sortieralgorithmen.

4.2 Musterorientierte Wissensrepräsentation

Typisch für Listenverarbeitung: kleiner Suchraum, weil nur eine Klausel ”paßt“. Jeder Klauselkopf hat eine spezifische Struktur.

Beispiel: addlast(L,E,LE) (L = [E_{1}, ..., E_{n}], LE = [E_{1}, ..., E_{n}, E])

1. L ist leer: addlast( \underline{[]},E,[E] )
2. L nichtleer: addlast( \underline{[F|R]},E,[F|RE]) :- addlast(R,E,RE).

Die unterstrichenen Teilausdrücke sind Muster (Pattern), es paßt immer höchstens eines.

Beweisbeispiel:

?- addlast([a,b],c,[a,b,c]).
⊢ ?- addlast([b],c,[b,c]).

⊢ ?- addlast([],c,[c]).
⊢ ?- .

Anmerkungen:

1. Der Suchraum ist ein-elementig.

2. Beweise sind deterministisch.

3. Der Verarbeitungsdauer ist linear abhängig von der Größe der Eingabeliste.

Beispiel: Symbolisches Differenzieren f(x) = 2x^{2} + ln x ⇒ \frac{df}{dx} = 4x + 1/x

Gesucht ist ein Prädikat dx(F,DF), welches wahr ist, falls DF = \frac{d}{dx}F, wobei F aus Zahlen, x, arithmetischen Operatoren, F^{c}, ln F besteht.

1. Repräsentation von Funktionen in Prolog:

Mathematische Funktion

Prolog-Term

c (Konstante)

                         k(c)

x  x

f + g (−, ∗, /)  F+G (−, ∗, /)

f^{c}  exp(F,k(c))
ln f  ln(F)
2x^{2} + ln x  k(2)*exp(x,k(2))+ln(x)

2. Wissen über dx: Formelsammlung

Mathematische Formel

Prolog-Klausel

(d/dx)c = 0  dx(k(C),k(0)).
(d/dx)x = 1  dx(x,k(1)).
(d/dx)(f + g) = f′ + g′  dx(F+G,DF+DG) :- dx(F,DF), dx(G,DG).
(d/dx)(cf) = c(d/dx)f  dx(k(C)*F,k(C)*DF) :- dx(F,DF).
(d/dx)(fg) = f′g + fg′  dx(F*G,DF*G+F*DG) :- dx(F,DF),dx(G,DG).
(d/dx)(f^{c}) = cf^{c−1}f′  dx(exp(F,k(C)),k(C)*exp(F,k(C-1))*DF)

                          :- dx(F,DF).

(d/dx)(ln f) = (1/f)f′  dx(ln(F),(1/F)*DF) :- dx(F,DF).

• In linken Seiten: Muster möglichst genau spezifizieren ⇒ kleiner Suchraum Alternativ für dx(F+G,...):

dx(U,DU) :- U=F+G, DU=DF+DG, dx(F,DF), dx(G,DG).

(prinzipiell immer anwendbar)

• Größe der Terme unbekannt ⇒ endlich viele Fakten nicht ausreichend ⇒ Regeln der Form p(...) : −...q_{i}(...) (als Argument von p: teilspezifizierter Term, z.B. (F + G); als Argumente der q_{i} Unterterme, z.B. F) ⇒ Beweis durch Zerlegen des Problems und Konstruktion einer Gesamtlösung.

Beispiel: Es gibt keine Klausel für dx(x*ln(x),...). Allerdings gibt es eine Klausel für F ∗ G; Anwendung mit Beweis für dx(x,...) und dx(ln(x),...).

• Symbolisches Differenzieren entspricht der Übersetzung von Funktionstermen in neue Funktionsterme und ist recht einfach spezifizierbar. ⇒ Prolog ist sehr gut geeignet für Übersetzer-Implementierungen. Spezielle Methode fest eingebaut: Definite Clause Grammars for Language Analysis (Pereira/Warren) in: Artificial Intelligence, Vol. 13 (1980) 231-278; oder: Hanus, Kap. 9

• Beachte: Prolog definiert Prädikate und keine Funktionen:

dx(x*ln(x),F) ⇝ erste Ableitung

dx(F,k(1)...) ⇝ Integral

4.3 Verwendung von Relationen

Häufig: Probleme sind funktionaler Natur: n Eingaben, berechne

f : M_{1} × ... × M_{n} → M : (x_{1}, ..., x_{n}) ↦ y

Implementierung als Relation: f(X1,...,Xn,Y) genau dann erfüllt, wenn Y das Ergebnis bezüglich Eingabe X_{1}, ..., X_{n} ist.

Verwendung:

1. als Funktion: f(t_{1}, ..., t_{n}, Y) ⇝ Y = ...

2. als Relation: f(X_{1}, ..., X_{n}, t) ⇝ X_{1} = ..., X_{n} = ... Umkehrfunktion/ Umkehrrelation

Beispiel: Konkatenation von Listen append(L_{1}, L_{2}, L_{3}) ⟺ L_{1} = [a_{1}, ..., a_{n}], L_{2} = [b_{1}, ..., b_{m}], L_{3} = [a_{1}, ..., a_{n}, b_{1}, ..., b_{m}] Definition über Struktur des ersten Arguments:

append([],L,L).
append([E|R],L,[E|RL]) :- append(R,L,RL).

Funktionaler Gebrauch:

?- append([a,f],[f,e],X).
X = [a,f,f,e]

Relationaler Gebrauch:

?- append([1],[2,3],[1,2,3]).
yes.

Umkehrrelation:

?- append(X,[3,4],[1,2,3,4]).
X = [1,2].

?- append([1,2],Y,[1,2,3,4]).
Y = [3,4].
?- append(X,Y,[a,b,c]).
X = [], Y = [a,b,c]  ;
X = [a], Y = [b,c]  ;
X = [a,b], Y = [c]  ;
X = [a,b,c], Y = []  ;
no.

Verwendung zur Definition neuer Prädikate:

• Anhängen eines Elements an eine Liste:

     anhang(L,E,LE) :- append(L,[E],LE).

• Letztes Element einer Liste:

     last(L,E) :- append(_,[E],L).

• Element enthalten?

     member(E,L) :- append(_,[E|_],L).

• Streichen eines Elementes:

     streiche(L,E,LohneE)
       :- append(L1,[E|L2],L), append(L1,L2,LohneE).

• Teilliste:

     teilliste(T,L) :- append(L1,R,L), append(T,L2,R).

(L = L_{1}; \underbrace{T; L_{2}}_{R})

1. Denke in Relationen (Beziehungen) und nicht in Zuordnungen.

2. Alle Parameter sind gleichberechtigt (keine Ein- oder Ausgabeparameter).

3. Nutze vorhandene Prädikate. Achte auf Allgemeinheit bei der Definition neuer Prädikate.

4.4 Datenstrukturen als Fakten

Beispiel: Wegesuche im Labyrinth

\overline{}a  b  c d  e  f

Frage: Gibt es einen Weg von a nach f? Allgemein: Weg von X nach Y. Lösung:

1. X = Y?

2. X hat Tür zu Z, und es gibt einen Weg von Z nach Y

⇒ Labyrinth muß als Objekt bekannt sein. Darstellung?

1. Erste Möglichkeit: Labyrinth = Liste aller Türen:

[tuer(a,b), tuer(b,c), ..., tuer(e,f)]

Lösungsfindung mittels Durchsuchen der Liste

2. Einfache Lösung: Labyrinth = Wissen über Türen:

tuer(a,b).
tuer(b,c).
...
tuer(e,f).

”Einseitige“ Formulierung. Eine Klausel der Form tuer(X,Y) :- tuer(Y,X). würde zur Gefahr von Endlosbeweisen führen. Vermeidung:

• zusätzliche Fakten oder

• hier: Berücksichtigung der Asymmetrie in Klauseln

gehe(X,Y); Weg von X nach Y Klauseln:

gehe(X,X).
gehe(X,Y) :- tuer(X,Z), gehe(Z,Y).
gehe(X,Y) :- tuer(Z,X), gehe(Z,Y). (Asymmetrie)

Dies ist logisch korrekt, allerdings besteht die Gefahr von Endlosbeweisen durch endlose Wege, z.B. a-b-c-e-d-b-c-e-d-b-c-e-... Zusätzlich: Information über besuchte Räume:

gehe(X,X,Besucht).
gehe(X,Y,Besucht) :- tuer(X,Z), nichtEnthalten(Z,Besucht),
                     gehe(Z,Y,[Z|Besucht]).
gehe(X,Y,Besucht) :- tuer(Z,X), nichtEnthalten(Z,Besucht),
                     gehe(Z,Y,[Z|Besucht]). (Asymmetrie)
nichtEnthalten(E,[]).
nichtEnthalten(E,[K|R]) :- ungleich(E,K), nichtEnhtalten(E,R).
ungleich(a,b).
ungleich(b,a).
...

Fragen:

• Weg von a nach f?

?- gehe(a,f,[a]).
⇝ yes.

22 5 THEORETISCHE GRUNDLAGEN DER LOGIKPROGRAMMIERUNG

• Weg von a nach f, der nicht durch c oder e führt?

       ?- gehe(a,f,[a,c,e]).
     ⇝ no.

Merke:

1. Es kann günstiger sein, Daten als Wissen darzustellen.

2. Problematisch ist die Änderung der Daten zur Laufzeit.

3. Typisch: Datenbankimplementierung (vergleiche Verwandtschaft)

5 Theoretische Grundlagen der Logikprogrammie-

rung

Semantik von Prolog ≈ Beweisen von Aussagen.

1. Was heißt ”konkreter“ Beweis?

2. Endlosbeweise: Kann Prolog alles beweisen?

3. Negation: Warum ist dies ein Problem? Weitere Struktur:

• Syntax und Semantik logischer Programme (≠ Prolog-Programme)

• Vergleich mit Prolog

5.1 Aufbau logischer Programme

Hier: Formeln der Prädikatenlogik erster Stufe. Definition (Prädikat, Term, Stelligkeit) Ein Prädikat hat die Form

p(t_{1}, ..., t_{n}), n ≥ 0

(p Prädikatname, t_{1}, ..., t_{n} Terme) Ein Term ist

• eine Variable (Großbuchstaben)

• eine Konstante (z.B. a, b, c, ...)

• eine Struktur f(t_{1}, ..., t_{n}), n ≥ 1, t_{i} Terme 5.1 Aufbau logischer Programme 23

Die Stelligkeit von Prädikaten/Funktoren ist die Anzahl ihrer Argumente. Beispiel: p(f(a, b), X, Y) ist ein dreistelliges Prädikat, dessen erstes Argument eine zweistellige Struktur und dessen zweites und drittes Argument Variablen sind. Definition (Formel)

1. Ein Prädikat ist eine Formel.

2. Wenn F und G Formeln sind, dann auch • (¬F): Negation ”nicht“

• (F ∧ G): Konjunktion ”und“ • (F ∨ G): Disjunktion ”oder“ • (F ⇒ G): Implikation ”folgt“

3. Wenn F eine Formel und X eine Variable sind, dann sind auch • (∃X : F) (Existenzquantor)

• (∀X : F) (Allquantor) Formeln.

(Dies beschreibt die Sprache der Prädikatenlogik erster Stufe: ”Erste Stufe“: Quantifizierung über Objekte, ”Zweite Stufe“: Quantifizierung über Prädikate. Beispiel:

• (∀X : (∃Y : (p(f(X, Y)) ⇒ q(X, Y))))

• (∀X : ((p(X, a) ∧ (¬p(X, a))) ⇒ q(X, a))) Vereinbarung: Klammern können weggelassen werden, solange die Eindeutigkeit klar ist:

• ∀X : ∃Y : p(f(X, Y)) ⇒ q(X, Y)

• ∀X : p(X, a) ∧ ¬p(X, a) ⇒ q(X, a) Definition (gebunden, frei, geschlossen) Eine Variable X heißt quantifiziert oder gebunden in F genau dann, wenn F eine Teilformel ∃X : G oder ∀X : G enthält und X außerhalb dieser Teilformel nicht vorkommt. Anderenfalls heißt X frei in F. Eine geschlossene Formel ist eine Formel ohne freie Variablen.

24 5 THEORETISCHE GRUNDLAGEN DER LOGIKPROGRAMMIERUNG

Definition (Literal, Klausel) Ein Literal ist ein Prädikat (positiv) oder ein negiertes Prädikat (negativ). Eine Klausel ist eine geschlossene Formel der Form

∀X_{1} : ...∀X_{k} : (L_{1} ∨ L_{2} ∨ ... ∨ L_{n})

(mit Literalen L_{i}).

Beispiel: ∀X : ∀Y : ¬p(f(X, Y)) ∨ q(X, Y)

Notation: Der Ausdruck

A_{1}, A_{2}, ..., A_{m} ⇒ B_{1}, ..., B_{n} (n, m ≥ 0)

mit Prädikaten A_{i}, B_{j} steht für

∀X_{1} : ...∀X_{k} : ¬A_{1} ∨ ... ∨ ¬A_{m} ∨ B_{1} ∨ ... ∨ B_{n}

(wobei X_{1}, ..., X_{k} alle Variablen in A_{i}, B_{j} sind).

Mathematische Gesetze:

• ¬A ∨ ¬B ≡ ¬(A ∧ B) (de Morgan)

• ¬A ∨ B ≡ A ⇒ B

Beachte: In A_{1}, ..., A_{m} ⇒ B_{1}, ..., B_{n} stehen die vorderen Kommata für ”und“, die hinteren Kommata für ”oder“.

Definition (Programmklausel, logisches Programm) Eine Programmklausel hat die Form

\underbrace{A_{1}, ..., A_{m}}_{Rumpf} ⇒ B (m ≥ 0),

mit Kopf B, für m = 0 heißt ⇒ B ein Faktum. Ein logisches Programm ist eine Menge von Programmklauseln, eine Anfrage hat die Form

A_{1}, ..., A_{m} ⇒

Die leere Klausel schreiben wir ⇒, und unter einer Hornklausel verstehen wir eine Programmklausel oder eine Anfrage. → Logikprogrammierung basiert auf Hornklausellogik.

Beispiel: ⇒ append([], L, L) append(R, L, RL) ⇒ append(·(E, R), L, ·(E, RL)) ”bedeutungslose Zeichenkette“.

5.2 Interpretationen und Modelle für Formeln

∀X : p(f(X, a), X) Fragen: 1) Über welche Menge wird quantifiziert? 2) Welche Bedeutung haben p, f, a?

Definition (Interpretation) Eine Interpretation I = (U, δ) von Formeln besteht aus

1. Dem Universum, einer nichtleeren Menge U von Objekten,

2. Einer Zuordnung von Konstanten c zu Objekten δ_{c} ∈ U,

3. Einer Zuordnung von n-stelligen Funktionen f zu Abbildungen δ_{f} : U^{n} → U,

4. Einer Zuordnung von n-stelligen Prädikaten p zu Abbildungen δ_{p} : U^{n} → {w, f}.

Beispiel: Verschiedene Interpretation der obigen Formel:

1. U = IN, δ_{a} = 1, δ_{f} = ∗, δ_{p} = ′ =′ p(f(X, a), X) ⇝_{δ} X ∗ 1 = X

2. U = ZZ, δ_{a} = 2, δ_{f} = +, δ_{p} = ′ >′ p(f(X, a), X) ⇝_{δ} X + 2 > X

Definition (Variablenbelegung) Sei I = (U, δ) eine Interpretation. Eine Variablenbelegung φ bezüglich I ist eine Abbildung von Variablen nach U. Notation: φ = {X_{1}/e_{1}, ..., X_{n}/e_{n}}, e_{i} ∈ U.

Ausrechnen von Termen:

Definition Sei I = (U, δ) eine Interpretation, φ eine Variablenbelegung bezüglich I. Dann wird die Fortsetzung φ̄ von φ auf Terme induktiv definiert über

• φ̄(X) := φ(X) für alle Variablen X,

• φ̄(c) := δ_{c} für alle Konstanten c,

• φ̄(f(t_{1}, ..., t_{n})) := δ_{f}(φ̄(t_{1}), ..., φ̄(t_{n})) für alle Strukturen.

Beispiel: Sei δ_{f} = +. φ_{1} = {X/0, Y/1} ⇒ φ̄_{1}(+(X, Y)) = 1, φ_{2} = {X/3, Y/5} ⇒ φ̄_{2}(+(X, Y)) = 8.

Definition (Wahrheit von Formeln) Seien I = (U, δ) eine Interpretation und φ eine Variablenbelegung.

1. p(t_{1}, ..., t_{n}) ist wahr : ⟺ δ_{p}(φ̄(t_{1}), ..., φ̄(t_{n})) = w.

2. Für zusammengesetzte Formeln ergibt sich die Wahrheit aus der Wahrheitstafel:

F G ¬F F ∧ G F ∨ G F ⇒ G
w w f  w  w  w
w f f  f  w  f
f w w  f  w  w
f f w  f  f  w

3. ∃X : F ist wahr, falls ein e ∈ U existiert, so daß F bezüglich I und φ[X/e] wahr ist, wobei

φ[X/e](Y) := \{ \begin{matrix}φ(Y), falls X ≠ Y \\ e, falls X = Y \end{matrix}

4. ∀X : F ist wahr, falls für jedes e ∈ U F bezüglich I und φ[X/e] wahr ist.

Im folgenden betrachten wir geschlossene Formeln.

Definition (Modell) Ein Modell für eine Formel ist eine Interpretation, unter der die Formel wahr wird. Eine Formel heißt erfüllbar, falls sie ein Modell besitzt, ansonsten heißt sie unerfüllbar. Eine Formel heißt allgemeingültig, falls jede Interpretation ein Modell ist.

Beispiel:

• ∀X : p(f(X, a), X) ist erfüllbar,

• p(a) ∧ ¬p(a) ist unerfüllbar,

• p(a) ∨ ¬p(a) ist allgemeingültig.

Definition Ein Modell für eine endliche Menge von Formeln {F_{1}, ..., F_{n}} ist eine Interpretation, unter der die Formel (F_{1} ∧ ... ∧ F_{n}) wahr ist (d.h. jede der Formeln F_{i} ist wahr).

(logische Programme: Mengen von Formeln)

Vereinbarung: F, F_{1}, ..., F_{n} immer Formeln, S endliche Formelmenge.

Definition (logische Konsequenz) F heißt logische Konsequenz aus S, wenn jedes Modell für S auch Modell für F ist.

Folgerung 5.1 F ist logische Konsequenz aus {F_{1}, ..., F_{n}} genau dann, wenn (F_{1} ∧ ... ∧ F_{n} ⇒ F) allgemeingültig ist.

Beweis: Übung.

Satz 5.2 F ist logische Konsequenz aus S genau dann, wenn S ∪ {¬F } unerfüllbar ist.

Beweis: ”⇒“: Sei I eine Interpretation für S ∪ {¬F }. Annahme: I ist Modell für S (sonst trivial). Dann folgt (da F logische Konsequenz aus S): I ist Modell für F. ⇒ ¬F falsch bezüglich I. ⇒ I ist kein Modell für S ∪ {¬F }. Da I beliebige Interpretation war, gibt es kein Modell. ”⇒“: Sei I ein Modell für S. Dann folgt (da S ∪ {¬F } unerfüllbar): I ist kein Modell für ¬F. Also ist F wahr bezüglich I und somit I ein Modell für F.

Falls S unerfüllbar ist, ist jedes F logische Konsequenz aus S.

Konsequenz für Logikprogrammierung: P Programm, A Anfrage. Sei P ∪ {A} unerfüllbar. ⇒ (Satz 5.2) ¬A ist logische Konsequenz aus P. A hat die Form ”A_{1}, ..., A_{n} ⇒“, d.h. Formel ∀X_{1}...∀X_{k} : ¬A_{1} ∨ ... ∨ ¬A_{n} d.h. ¬A: \underbrace{∃X_{1}...∃X_{k} : A_{1} ∧ ... ∧ A_{n}}_{wahr}

d.h. es existieren Werte für X_{1}, ..., X_{k}, so daß jedes A_{i} wahr ist.

Daher: zeige Unerfüllbarkeit von Formelmengen.

Lösung (unpraktikabel): Zeige, daß alle Interpretationen keine Modelle sind.

Im Fall von Klauselmengen ist es ausreichend, nur (syntaktische) Herbrand-Interpretationen zu untersuchen:

Definition (Herbrand-Basis) Sei S eine Formelmenge. Dann bezeichnen

• U_{S} := Menge aller Grundterme mit Konstanten und Faktoren aus S das Herbrand-Universum und

• B_{S} := {p(t_{1}, ..., t_{n}) | t_{1}, ..., t_{n} ∈ U_{S}, p kommt in S vor } die Herbrand-Basis von S.

Beispiel: S = {p(X, Y) ⇒ p(f(X), g(Y)), ⇒ p(f(a), X)}. Dann ist U_{S} = {a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), ...}.

Definition (Herbrand-Interpretation) Eine Interpretation I = (U, δ) eine Formelmenge S heißt Herbrand-Interpretation, falls

1. U = U_{S} (Herbrand-Universum),

2. δ_{c} = c für alle Konstanten c, 3. δ_{f}(t_{1}, ..., t_{n}) = f(t_{1}, ..., t_{n}) ∈ U_{S} für alle n-stelligen Funktoren f und t_{1}, ..., t_{n} ∈

U_{S} (Term-Interpretation)

Intuitiv: Herbrand-Interpretationen sind syntaktische Terminterpretationen. Prädikate sind in Herbrand-Interpretationen nicht festgelegt.

Definition (Herbrand-Modell) Herbrand-Interpretationen, die Modelle sind, heißen Herbrand-Modell.

Herbrand-Interpretationen lassen sich durch Angabe einer Teilmenge M ⊂ B_{S} der Herbrand-Basis spezifizieren. Intuitiv: L ∈ M bedeutet L ist wahr bezüglich M.

Beispiel: M = {p(a), p(f(f(a))}. Das Universum ist U = {a, f(a), f(f(a)), f(f(f(a))), ...}. Wahr sind: p(a) und p(f(f(a))). Falsch sind: p(f(a)), p(f^{3}(a)), p(f^{4}(a)), ... .

Satz 5.3 Sei S eine Klauselmenge, die ein Modell hat. Dann hat S auch ein Herbrand-Modell.

Beweis: Sei I ein Modell für S. Dann definieren wir die Herbrand-Interpretation I′ durch

I′ := {p(t_{1}, ..., t_{n}) ∈ B_{S} | p(t_{1}, ..., t_{n}) wahr bezüglich I}

Man kann nun recht einfach zeigen (Übung): I′ ist Modell für S.

Satz 5.4 Sei S eine Klauselmenge. Dann gilt: S unerfüllbar ⟺ S hat kein Herbrandmodell.

Beweis: ”⇒“: trivial. ”⇐ “: Wäre S erfüllbar, dann gäbe es nach Satz 5.3 ein Herbrandmodell, Widerspruch.

Also: In der Logikprogrammierung: Untersuche alle Herbrand-Interpretationen (aufzählbar). ⇒ Rein syntaktische Methoden sind ausreichend.

Anmerkung: Bei Nicht-Klauselmengen gilt Satz 5.4 nicht! (vergleiche Übung)

Konflikt:

• Zum automatischen Beweisen: Klauseln,

• Manchmal natürlicher: Problemspezifikation in Prädikatenlogik (also mit ∃- Quantoren)

Exkurs: Transformation von Formeln in Klauseln

Definition (logisch äquivalent) Zwei Formeln F, G heißen logisch äquivalent, wenn für jede Interpretation I und jede Variablenbelegung φ gilt:

F wahr bezüglich I, φ ⟺ G wahr bezüglich I, φ

Notation: F ≡ G.

Beispiel: (F ⇒ G) ≡ (¬F ∨ G)

Im folgenden versuchen wir Formeln mit ∀, ∃, ¬, ∧ und ∨ auf Klauselform

∀X_{1}...∀X_{k} : ¬A_{1} ∨ ...¬A_{m} ∨ B_{1} ∨ ... ∨ B_{n}

zu transformieren.

Erster Transformationsschritt: Quantoren nach außen schieben

Definition (Pränex-Form) Eine Formel ist in Pränex-Form, falls sie die Form Q_{1}X_{1}...Q_{n}X_{n}F hat, wobei die Q_{i} ∈ {∀, ∃} sind, n ≥ 0, X_{i} Variablen und F eine Formel ohne Quantoren sind.

Zur Transformation einer Formel in Pränex-Form:

Algorithmus (Transformation in Pränex-Form)

1. ¬(∀XF) ≡ ∃X(¬F)

¬(∃XF) ≡ ∀X(¬F)

2. Falls X in G nicht frei vorkommt (sonst benenne X um durch Äquivalenz ∀XF = ∀Y F [X/Y]; Ersetzung aller freien Variablen X durch Y in F) (∀XF) ∧ G ≡ ∀X(F ∧ G) (∀XF) ∨ G ≡ ∀X(F ∨ G) (∃XF) ∧ G ≡ ∃X(F ∧ G) (∃XF) ∨ G ≡ ∃X(F ∨ G)

Im folgenden: Jeder Quantor bindet eine andere Variable.

Satz 5.5 Zu jeder Formel existiert eine logische äquivalente Formel in Pränexform.

Beweis: Sukzessives Anwenden der obigen Äquivalenzen (genauer: Literatur: Schöning)

Zweiter Schritt: Elimination von Existenzquantoren (Skolemisierung)

Algorithmus (Skolemisierung) Eingabe: Formel F in Pränexform Ausgabe: Skolemform von F while ( F enthält Existenzquantoren ) do

Sei F = ∀X_{1}...∀X_{n}∃Y G

(∃Y ”linkester“ Existenzquantor)

Sei f ein neues n-stelliges Funktionssymbol. F := ∀X_{1}∀X_{n}G[Y/f(X_{1}, ..., X_{n})]

od Ausgabe F

Im allgemeinen ist dies keine Äquivalenzumformung. Es gilt aber:

Satz 5.6 Sei F in Pränexform. Dann gilt: F ist genau dann erfüllbar, wenn die Skolemform von F erfüllbar ist.

Beweis: Schöning

Erfüllbarkeitsäquivalenz ist für viele Anwendungen ausreichend, insbesondere für Unerfüllbarkeitstests.

Dritter Schritt: Konjunktive Normalform

Konjunktive Normalform (KNF): ⋀_{i} ⋁_{j} L_{ij}

Algorithmus (KNF) Eingabe: quantorenfreie Formel F Ausgabe: KNF von F

1. Führe folgende Ersetzungen durch: ¬¬G → G ¬(G ∧ H) → ¬G ∨ ¬H (de Morgan) ¬(G ∨ H) → ¬G ∧ ¬H

2. Führe folgende Ersetzungen durch: G ∨ (H ∧ K) → (G ∨ H) ∧ (G ∨ K) (F ∧ H) ∨ K → (G ∨ K) ∧ (H ∨ K)

Schritte 1, 2 und 3 führen zu Formel

∀X_{1}...∀X_{n} : ⋀_{i=1}^{n} ⋁_{j=1}^{m} L_{ij} ≈ {∀X_{1}...∀X_{n} : ⋁_{j=1}^{m} L_{ij} | i = 1, ..., n}

(L_{ij} Literale)

Beispiel:

F = (¬∃X(p(X, Z) ∨ ∀Y q(X, f(Y))) ∨ ∀Y p(q(Y, Y), Z))

1. Eliminiere mehrfache Vorkommen quantifizierter Variablen: F_{1} = (¬∃X(p(X, Z) ∨ ∀Y q(X, f(Y))) ∨ ∀W p(q(W, W), Z))

2. Freie Variablen mit ∃ binden:

F_{2} = ∃ZF_{1}

3. Pränexform:

∃Z∀X∃Y ∀W (¬(p(X, Z) ∨ q(X, f(Y))) ∨ p(q(W, W), Z))

4. Skolemform: Z/a, Y/h(X):

∀X∀W (¬p(X, a) ∨ q(X, f(h(X))))) ∨ p(q(W, W), a))

5. Rumpf in KNF:

∀X∀W (¬p(X, a) ∨ p(q(W, W), a)) ∧ (¬q(X, f(h(X))) ∨ p(q(W, W), a))

6. Klauselnotation:

{p(X, a) ⇒ p(q(W, W), a), q(X, f(h(X))) ⇒ p(q(W, W), a)} (sogar zufällig Hornklauseln ⇒ Ergebnis ist logisches Programm)

Theorembeweiser basieren meist auf Klauseln (allgemeinen – nicht nur Hornklauseln). Allerdings: Effiziente Beweisverfahren sind nur für Hornklauseln bekannt.

5.3 Fixpunkte

Motivation: Wir wollen eine Beziehung zwischen Modellen und Resolutionsverfahren hestellen. Definition (partielle Ordnung) Eine partielle Ordnung ist eine binäre Relation ”≤“ auf einer Menge M mit

1. x ≤ x∀x ∈ M (Transitivität)

2. x ≤ y und y ≤ x ⇒ x = y ∀x, y ∈ M (Antisymmetrie)

3. x ≤ y und y ≤ z ⇒ x ≤ z ∀x, y, z ∈ M (Reflexivität) Beispiel: A Menge, 2^{A} = P ot(A) Potenzmenge von A. Dann ist ⊆ eine partielle Ordnung auf 2^{A}. Definition (Schranken) Sei M eine Menge mit partieller Ordnung ≤.

• a ∈ M heißt obere Schranke für A ⊆ M, falls x ≤ a für alle x ∈ A.

• a ∈ M heißt untere Schranke für A ⊆ M, falls a ≤ x für alle x ∈ A.

• a ∈ M heißt kleinste obere Schranke (least upper bound, lub(A)), falls a obere Schranke ist und für jede obere Schranke b gilt: a ≤ b.

• a ∈ M heißt größte untere Schranke (greatest lower bound, glb(A)), falls a untere Schranke ist und für jede untere Schranke b gilt: b ≤ a.

Anmerkung: lub und glb sind eindeutig, falls sie existieren.

Definition (Verband) Eine partiell geordnete Menge M heißt vollständiger Verband, wenn lub(A) und glb(A) für alle A ⊆ M existieren. In diesem Fall heißen

• ⊥ =glb(M) kleinstes Element (bottom),

• ⊤ =lub(M) größtes Element (top).

Beispiel: 2^{A} ist vollständiger Verband, wobei

lub(B) = ⋃_{C∈B} C, glb(B) = ⋂_{C∈B} C, ⊥ = ∅, ⊤ = A

(für B ⊆ 2^{A})

Definition Sei M ein vollständiger Verband, f : M → M eine Abbildung.

• f heißt monoton, falls f(x) ≤ f(y) für alle x, y ∈ M.

• Eine Teilmenge X ⊆ M heißt gerichtet, falls jede endliche Teilmenge von X eine obere Schranke in X hat.

• f heißt stetig, falls f(lub(X)) = lub(f(X)) für alle gerichteten Teilmengen X ⊆ M.

Interessant für die Logikprogrammierung ist die Herbrandbasis B_{P}. Die Menge 2^{B_{P}} aller Herbrand-Interpretationen ist ein vollständiger Verband.

Definition (kleinster Fixpunkt) Sei M ein vollständiger Verband, f : M → M. a ∈ M heißt kleinster Fixpunkt von f, falls

• a Fixpunkt von f, d.h. f(a) = a und

• a ≤ b für alle übrigen Fixpunkte b von f.

Analog: größter Fixpunkt.

Satz 5.7 (Tarski) Sei M ein vollständiger Verband, f : M → M monoton. Dann existieren ein kleinster Fixpunkt lfp(f) und ein größter Fixpunkt gfp(f). Außerdem:

lfp(f) = glb{x | f(x) = x} = glb{x | f(x) ≤ x}

gfp(f) = lub{x | f(x) = x} = lub{x | x ≤ f(x)}

Beweis: Lloyd-Buch

Definition Sei M ein vollständiger Verband, f : M → M monoton. Dann definiere

• f ↑ 0 := ⊥

• f ↑ k := f(f ↑ (k − 1))∀k > 0

• f ↑ ω := lub{f ↑ k | k ≥ 0} (ω ≈ unendlich, → Ordinalzahlen)

Konstruktive Berechnung des kleinsten Fixpunktes lfp:

Satz 5.8 (Kleene) Sei M ein vollständiger Verband, f : M → M stetig. Dann gilt:

lfp(f) = f ↑ ω

Konsequenz: Berechne lfp durch Iteration, ausgehend von ⊥.

5.4 Deklarative Semantik logischer Programme

Im folgenden sei P immer ein logisches Programm.

Satz 5.9 ⋂{M|M Herbrand-Modell für P }

ist auch ein Herbrand-Modell, genannt kleinstes Herbrand-Modell M_{P}.

Beweis: Die Herbrand-Basis B_{P} ist ein Modell für P. Es ist einfach zu zeigen (→ Übung), daß der Durchschnitt einer nichtleeren Menge von Herbrand-Modellen ein Herbrand-Modell ist.

Häufig sagt man: die deklarative Semantik von P entspricht M_{P}. Dies wird durch den folgenden Satz gerechtfertigt:

Satz (van Emden, Kowalski)

M_{P} = {A ∈ B_{P} |A logische Konsequenz von P }

Beweis: A logische Konsequenz von P ⟺ P ∪ {¬A} unerfüllbar (Satz 5.2) ⟺ P ∪ {¬A} hat kein Herbrand-Modell (Satz 5.4) ⟺ ¬A ist falsch in allen Herbrand-Modellen für P ⟺ A ist wahr in allen Herbrand-Modellen für P ⟺ A ∈ M_{P}.

Charakterisierung von M_{P} als kleinster Fixpunkt (Beachte: 2^{B_{P}} ist vollständiger Verband.)

Definition (Operator T_{P}) Die Abbildung T_{P} : 2^{B_{P}} → 2^{B_{P}} auf Herbrand-Interpretationen sei definiert durch T_{P} (I) := {A ∈ B_{P} | A_{1}, ..., A_{n} ⇒ A Grundinstanz einer Klausel in

B_{P} mit {A_{1}, ..., A_{n}} ⊆ I}

Hierbei: t_{1} heißt Grundinstanz von t_{2}, falls es eine Substitution σ mit σ(t_{2}) = t_{1} gibt und t_{1} variablenfrei ist.

Beispiel: ⇒ p(A) p(X) ⇒ p(f(X)) Sei I_{0} := ∅. I_{1} = T_{P} (I_{0}) = {p(a)}. I_{2} = T_{P} (I_{1}) = {p(a), p(f(a))}. I_{3} = T_{P} (I_{2}) = {p(a), p(f(a)), p(f(f(a)))}. T_{P} beschreibt Ein-Schritt-Ableitungen mit Regeln.

Klar: T_{P} ist monoton: I_{1} ⊆ I_{2} ⇒ T_{P} (I_{1}) ⊆ T_{P} (I_{2}).

Satz 5.11: T_{P} ist stetig.

Beweis: Sei X eine gerichtete Teilmenge von 2^{B_{P}}. Zu zeigen ist: T_{P} (lub(X)) = lub(T_{P} (X)). Wir stellen zunächst fest: {A_{1}, ..., A_{n}} ⊆ lub(X) ⟺ {A_{1}, ..., A_{n}} ⊆ I für ein I ∈ X (→ Übung). A ∈ T_{P} (lub(X)) ⟺ A_{1}, ..., A_{n} ⇒ A Grundinstanz einer Klausel aus P und {A_{1}, ..., A_{n}} ⊆ lub(X) (Definition T_{P}) ⟺ A_{1}, ..., A_{n} ⇒ A Grundinstanz einer Klausel aus P und {A_{1}, ..., A_{n}} ⊆ I für ein I ∈ X ⟺ A ∈ T_{P} (I) für ein I ∈ X (Definition T_{P}) ⟺ A ∈ lub(T_{P} (X)) = ⋃_{I∈X} T_{P} (I).

Satz 5.12 Sei I eine Herbrand-Interpretation von P. Dann gilt: I ist Modell für P ⟺ T_{P} (I) ⊆ I.

Beweis: I Modell ⟺ Für alle Grundinstanzen A_{1}, ..., A_{n} ⇒ A von Klauseln aus P gilt: {A_{1}, ..., A_{n}} ⊆ I ⇒ A ∈ I ⟺ T_{P} (I) ⊆ I.

Satz 5.13 (Fixpunktcharakterisierung des kleinsten Herbrand-Modelles)

M_{P} = lfp(T_{P}) = T_{P} ↑ ω

Beweis: M_{P} = ⋂{I|I Herbrand-Modell für P } = glb{I|I Herbrand-Modell für P } = glb{I|T_{P} (I) ⊆ I} (Satz 5.12) = lfp(T_{P}) (Satz 5.7, Tarski) = T_{P} ↑ ω (Satz 5.8, Kleene).

⇒ Das kleinste Herbrand-Modell M_{P} ist effektiv berechenbar (im Unendlichen).

Wichtiger Aspekt: Variablen in Anfragen.

Definition (Antwort) Sei A eine Anfrage der Form A_{1}, ..., A_{n} ⇒. Eine Antwort für A bezüglich P ist eine Substitution σ der in A vorkommenden Variablen. Eine Antwort σ heißt korrekt, falls ∀(σ(A_{1} ∧ ... ∧ A_{n})) logische Konsequenz aus P ist. Hierbei ist der Allabschluß ∀(F) von F definiert durch ∀(F) := ∀X_{1}...∀X_{n} : F, falls X_{1}, ..., X_{n} alle Variablen aus F sind.

Korrekte Antworten ≈ intuitive Vorstellung von Prolog-Systemen.

Beispiel: P := {⇒ anhang([], E, ·(E, [])), anhang(R, E, RE) ⇒ anhang(·(K, R), E, ·(K, RE))} Anfrage: anhang(·(K, []), b, X) ⇒ Antwort: σ = {K/E, X/ · (E, ·(b, []))} Diese Antwort ist korrekt, falls ∀E : anhang(·(E, []), b, ·(E, ·(b, []))) logische Konsequenz aus P ist.

deklarative Semantik, statische Semantik: korrekte Antworten

Aber: Prolog ist ein Beweissystem und hat eine prozedurale (operationelle, dynamische) Semantik: → Resolutionsprinzip

5.5 Beweisen mit logischen Programmen

P: logisches Programm

Präzisierung der Resolution: SLD-Resolution

(SLD: \underline{L}inear Resolution for \underline{D}efinite Clauses with \underline{S}election Function)

36 5 THEORETISCHE GRUNDLAGEN DER LOGIKPROGRAMMIERUNG

Auswahlregel S: Wählt ein Literal aus einer Anfrage aus. Beispiel:

• FIRST: Wähle das erste Literal

• LAST: Wähle das letzte Literal Im folgenden sei S immer eine feste, aber beliebig gewählte Auswahlregel. Definition (SLD-Resolutionsschritt) Gegeben:

1. Anfrage A_{1}, ..., A_{k−1}, A_{k}, A_{k+1}, ..., A_{n} ⇒

2. Klausel B_{1}, ..., B_{l} ⇒ B

3. Auswahlregel S wählt A_{k} aus Ist σ mgu für A_{k} und B, dann heißt

σ(A_{1}), ..., σ(A_{k−1}), σ(B_{1}), ..., σ(B_{l}), σ(A_{k+1}), ..., σ(A_{n}) ⇒

ableitbar aus der Anfrage und Klausel bezüglich S bzw. Resolvente aus der Anfrage und Klausel bezüglich S. Definition (SLD-Ableitung) Sei A eine Anfrage. Eine SLD-Ableitung von P ∪ {A} bezüglich S ist eine endliche Folge

G_{1} ⊢_{σ_{1}} G_{2} ⊢_{σ_{2}} G_{3}...

von Anfragen (goals) mit 1. G_{1} = A

2. G_{i+1} ist Resolvente aus G_{i} und C_{i} mit mgu σ_{i} bezüglich S, wobei C_{i} eine Klausel aus P ist, in der eventuell einige Variablen umbenannt worden sind (vermeide Namenskonflikte für Variablen in G_{i} und C_{i}).

Beispiel: P:

1. ⇒ p(a)

2. ⇒ p(b)

3. q(a) ⇒ p(a)

4. p(X) ⇒ q(X)

SLD-Ableitung (S = LAST): p(b), \underline{q(a)} ⇒ ⊢_{\{X/a\},(4)} p(b), \underline{q(a)} ⇒ ⊢_{\{\},(1)} \underline{p(b)} ⇒ ⊢_{{},(2)}⇒ (bzw. □).

Definition (SLD-Widerlegung) Eine SLD-Widerlegung ist eine SLD-Ableitung, die in □ endet. Eine uneingeschränkte SLD-Widerlegung ist eine SLD-Widerlegung, bei der beliebige Unifikatoren (statt mgu’s) erlaubt sind. Drei Möglichkeiten:

• erfolgreiche SLD-Ableitungen enden in □,

• fehlgeschlagene SLD-Ableitungen sind endlich, enden aber nicht in □ (z.B. q(c) ⇒⊢_{{X/c}} p(c) ⇒ ),

• unendliche SLD-Ableitungen.

Eine erfolgreiche SLD-Widerlegung endet also in der leeren Klausel □, d.h. leere Disjunktion ≡ false. Am Ende: Widerspruch abgeleitet Bedeutung: P ∪ {A} ⇒ Widerspruch, damit ist P ∪ {A} unerfüllbar, d.h. ¬A ist logische Konsequenz aus P (vergleiche Anmerkungen zu Satz 5.2). Konstruktion von Widerspruchsbeweisen (typisch für Resolutionsbeweise)

Operationelle Semantik von Logikprogramm: SLD-Resolution

Definition (S-berechnete Antwort) Eine S-berechnete Antwort σ für P ∪ {A} ist eine Substitution der Variablen in A, für die eine SLD-Widerlegung A ⊢_{σ_{1}} A_{1} ⊢ σ_{2}A_{2} ⊢ ... ⊢_{σ_{n}} □ existiert, so daß σ(x) = σ_{n}(...(σ_{2}(σ_{1}(x))...) für alle Variablen x in A.

Beispiel: Anfrage: q(Z) ⇒⊢_{σ_{1}={X/Z}} p(Z) ⇒⊢_{σ_{2}={Z/a}} □. σ_{2} ∘ σ_{1} = {X/a, Z/a}. Eine S-berechnete Antwort ist σ = {Z/a}; σ ist auch eine korrekte Antwort.

Satz 5.14 (Korrektheit der S-berechneten Antwort) Jede S-berechnete Antwort σ für P ∪ {A} ist eine korrekte Antwort.

Beweis: Seien A : A_{1}, ..., A_{k} ⇒ und σ_{1}, ..., σ_{n} mgu’s in der SLD-Widerlegung von P ∪ {A}. Zu zeigen ist: Der Allabschluß ∀(σ_{n} ∘ ... ∘ σ_{1}(A_{1} ∧ ... ∧ A_{k})) ist logische Konsequenz aus P. Induktion über n:

• n = 1: Dann: A : A_{1} ⇒, und es gibt ein Faktum ⇒ B mit σ_{1}(A_{1}) = σ_{1}(B). Somit ist ∀σ_{1}(B) logische Konsequenz aus P, und damit auch ∀σ_{1}(A_{1}).

• n > 1: Betrachte ersten Ableitungsschritt von A: Sei A_{m} das ausgewählte Literal und B_{1}, ..., B_{l} ⇒ B die angewendete Klausel, d.h. σ_{1}(A_{m}) = σ_{1}(B). ⇒ Erste Resolvente: G = σ_{1}(A_{1}, ..., A_{m−1}, B_{1}, ..., B_{l}, A_{m+1}, ..., A_{k}) ⇒ Dann ist nach Induktionsvoraussetzung

∀(σ_{n} ∘ ... ∘ σ_{2} ∘ σ_{1}(A_{1} ∧ ... ∧ A_{m−1} ∧ B_{1} ∧ ... ∧ B_{l} ∧ A_{m+1} ∧ ... ∧ A_{k}))

logische Konsequenz aus P. Daraus folgt, daß ∀(σ_{n} ∘ ... ∘ \underbrace{σ_{1}(B)}_{σ_{1}(A_{m})}) logische Konsequenz aus P.

Insgesamt ist also ∀(σ_{n} ∘ ... ∘ σ_{1}(A_{1} ∧ ... ∧ A_{m} ∧ ... ∧ A_{k})) logische Konsequenz aus P.

Vollständigkeit der SLD-Resolution:

Ist jede korrekt Antwort auch eine berechnete?

• Im allgemeinen nicht: Berechnung mit allgemeinsten Unifikatoren liefert allgemeinste Antworten Beispiel: ⇒ p(X). Anfrage: p(Z) ⇒. korrekt: σ = {Z/a}; berechnet: σ′ = {Z/X}.

• Wir werden zeigen, daß jede korrekte Antwort eine Instanz einer berechneten Antwort ist.

Lemma 5.15 (mgu-Lemma) Sei

A ⊢_{σ_{1}} A_{1} ⊢_{σ_{2}} A_{2} ⊢ ... ⊢_{σ_{n}} □

eine uneingeschränkte SLD-Ableitung (d.h. σ_{1}, ..., σ_{n} nicht notwendig mgu’s sondern nur Unifikatoren). Dann existiert auch eine SLD-Widerlegung

A ⊢_{σ′_{1}} A′_{1} ⊢_{σ′_{2}} A′_{2} ⊢ ... ⊢_{σ′_{n}} □

und eine Substitution φ mit φ ∘ σ′_{n} ∘ ... ∘ σ′_{1} = σ_{n} ∘ ... ∘ σ_{1}.

Beweis: Induktion über n:

• n = 1: Dann: A ⊢_{σ_{1}} □. Also: A : L ⇒, und es gibt ein Faktum ⇒ B mit σ_{1}(L) = σ_{1}(B). Dann folgt mit dem Unifikationssatz aus Kapitel 3.2, daß es einen mgu σ′_{1} für L und B und eine Substitution φ mit φ ∘ σ′_{1} = σ_{1} gibt. Damit ist A ⊢_{σ′_{1}} □ eine SLD-Widerlegung.

• n > 1: Betrachte den ersten Schritt: Sei L ausgewähltes Literal und B_{1}, ..., B_{m} ⇒ B die verwendete Klausel, d.h. σ_{1}(L) = σ_{1}(B). Dann folgt aus dem Unifikationssatz, daß es einen mgu σ′_{1} und eine Substitution φ mit φ ∘ σ′_{1} = σ_{1} gibt. Also ist A ⊢_{σ′_{1}} A′_{1} ein SLD-Schritt mit φ(A′_{1}) = A_{1}. Weiterhin: A′_{1} ⊢_{σ_{2}∘φ} A_{2} ⊢_{σ_{3}} A_{3} ⊢ ... ⊢_{σ_{n}} □ ist uneingeschränkte SLD-Ableitung der Länge n − 1. Aus der Induktionsvoraussetzung folgt die Existenz einer SLD-Widerlegung A′_{1} ⊢_{σ′_{2}} A′_{2} ⊢_{σ′_{3}} ... ⊢_{σ′_{n}} □ und einer Substitution γ mit γ ∘ σ′_{n} ∘ ... ∘ σ′_{2} =

σ_{n} ∘ ... ∘ σ_{2} ∘ φ. Also γ ∘ σ′_{n} ∘ ... ∘ σ′_{2} ∘ σ′_{1} = σ_{n} ∘ ... ∘ σ_{2} ∘ \underbrace{φ ∘ σ′_{1}}_{σ_{1}}.

Zunächst: Variablenfreie Anfragen.

Satz 5.16 Sei L ein positives Literal ohne Variablen und logische Konsequenz aus P. Dann gibt es eine SLD-Widerlegung für P ∪ {L ⇒}.

Beweis: Da L ∈ B_{P} und L logische Konsequenz ist, gilt L ∈ M_{P} (Satz 5.10). Daraus folgt mit Satz 5.13: L ∈ T_{P} ↑ ω, und somit: ∃n : L ∈ T_{P} ↑ n. Induktion über n: Es gibt eine SLD-Widerlegung für P ∪ {L ⇒}.

• n = 1: L ∈ T_{P} ↑ 1. Dann folgt aus der Definition von T_{P}, daß es ein Faktum ⇒ A und eine Substitution σ mit σ(A) = L gibt, d.h. L ⊢_{σ} □ ist uneingeschränkte SLD-Ableitung. Nun kann das mgu-Lemma 5.15 angewendet werden.

• n > 1: L ∈ T_{P} ↑ n: Nach Definition von T_{P} gibt es eine Grundinstanz σ(B_{1}, ..., B_{k} ⇒ B) mit σ(B) = L und {σ(B_{1}), ..., σ(B_{k})} ⊆ T_{P} ↑ (n − 1). Dann existiert nach Induktionsvoraussetzung eine SLD-Widerlegung für P ∪ {σ(B_{i}) ⇒}. Da σ(B_{i}) variablenfrei ist, gibt es eine SLD-Widerlegung für P ∪ {σ(B_{1}), ..., σ(B_{k}) ⇒}. Damit existiert eine uneingeschränkte SLD-Widerlegung für P ∪ {L ⇒}. Nun kann wieder das mgu-Lemma angewendet werden.

Nächster Schritt: Identische Substitutionen sind berechnete Antworten von logischen Konsequenzen.

Lemma 5.17 Sei L ein positives Literal. Falls ∀(L) logische Konsequenz aus P ist, dann ist die Identität {} eine S-berechnete Antwort für P ∪ {L ⇒}.

Beweis: L enthält Variablen X_{1}, ..., X_{n}. Seien c_{1}, ..., c_{n} \underline{neue} Konstanten (nicht in P oder L), und sei σ = {X_{1}/c_{1}, ..., X_{n}/c_{n}}. ∀(L) ist logische Konsequenz aus P, damit ist auch σ(L) logische Konsequenz aus P. Mit dem vorangehenden Satz 5.16 folgt die Existenz einer SLD-Widerlegung für P ∪ {σ(L) ⇒}. Da die c_{i} nicht in L oder P vorkommen, ersetze in dieser Ableitung c_{i} durch X_{i}, dadurch erhält man eine SLD-Widerlegung für P ∪{L ⇒}, bei der kein X_{i} ersetzt wird.

Lemma 5.18 (Lifting-Lemma) Gegeben P, A, σ. Falls eine SLD-Widerlegung für P ∪{σ(A)} mit mgu’s σ_{1}, ..., σ_{n} existiert, dann existieren auch eine SLD-Widerlegung für P ∪ {A} mit mgu’s σ′_{1}, ..., σ′_{n} und eine Substitution φ mit σ_{n} ∘ ... ∘ σ_{1} ∘ σ = φ ∘ σ′_{n} ∘ ... ∘ σ′_{1}.

Beweis: Betrachte den ersten Schritt σ(A) ⊢_{σ_{1}} A_{1}. Sei B_{1}, ..., B_{k} ⇒ B die verwendete Klausel und σ(L) das ausgewählte Literal. o.B.d.A sei σ(B) = B. Dann gilt: σ_{1}(σ(L)) = σ_{1}(B) = σ_{1}(σ(B)), also ist A ⊢_{σ_{1}∘σ} A_{1} ein uneingeschränkter SLD-Schritt (da σ nicht notwendig ein mgu ist). Wegen des mgu-Lemmas 5.15 gibt es eine gewünschte SLD-Widerlegung.

Satz 5.19 (Vollständigkeit der SLD-Resolution) Für jede korrekte Antwort σ für P ∪ {A} existieren eine S-berechnete Antwort σ′ für P ∪{A} und eine Substitution φ, so daß σ(x) = φ(σ′(x)) für alle Variablen x in A.

Beweis: Sei A : L_{1}, ..., L_{k} ⇒. Dann ist ∀(σ(L_{1} ∧ ... ∧ L_{k})) logische Konsequenz aus A. Nach Lemma 5.17 ist die Identität {} eine S-berechnete Antwort für jedes P ∪ {σ(L_{i}) ⇒}. ^{1} Kombiniere diese zu einer SLD-Widerlegung für die Anfrage P ∪ {σ(A)} mit S-berechneter Antwort {}. Seien σ′_{1}, ..., σ′_{n} die mgu’s in dieser Ableitung, σ′_{n} ∘ ... ∘ σ′_{1} die Identität auf der Anfrage. Dann existieren nach dem Lifting-Lemma 5.18 eine SLD-Widerlegung für P ∪{A} mit mgu’s σ_{1}, ..., σ_{n} und eine Substitution φ mit φ ∘ σ_{n} ∘ ... ∘ σ_{1} = \underbrace{σ′_{n} ∘ ... ∘ σ′_{1}}_{\{\}} ∘σ. Sei σ′ die Einschränkung von

σ_{n} ∘ ... ∘ σ_{1} auf Variablen in A, dann folgt φ(σ′(x)) = sigma(x).

Die Bedeutung der Sätze 5.14 und 5.19 ist die Äquivalenz der deklarativen und operationellen Semantik.

Die Auswahlregel S war bisher beliebig. Im folgenden: FIRST (in Prolog)

Wie findet man SLD-Widerlegungen?

Beispiel:

(1) q(X, Y), p(Y, Z) ⇒ p(X, Z), (2) ⇒ p(X, X), (3) ⇒ q(a, b). Anfrage: p(S, b) ⇒ SLD-Ableitungen:

1. p(S, b) ⇒ ⊢_{(1)} q(S, Y), p(Y, b) ⇒ ⊢_{(3),[S/a,Y/b]} p(b, b) ⇒ ⊢_{(1)} (Umbennenung der Variablen in Klausel 1) \underline{q(b, Y_{1})}, p(Y_{1}, b) ⇒ Fehlschlag.

2. p(S, b) ⇒ ⊢_{(1)} q(S, Y), p(Y, b) ⇒ ⊢_{(3),[S/a,Y/b]} p(b, b) ⇒ ⊢_{(2)} □.

Erfolg: σ = {S/a}.

Systematische Methode zum Finden von SLD-Widerlegung (Beschreibung: markierte Bäume.

1Bemerkung: nicht σ(P), da alle Regeln in P ∀-quantifiziert sind.

Definition (SLD-Baum) Ein SLD-Baum für P ∪ {A} ist ein markierter Baum, dessen Kanten mit Anfragen markiert sind, mit:

1. Die Wurzel ist mit A markiert.

2. Ist S ein Knoten und sind S_{1}, ..., S_{n} alle Resolventen aus S und Klauseln in P, dann hat S die Söhne S_{1}, ..., S_{n}.

3. Die leere Klausel hat keinen Sohn.

Beispiel:

[figure: q(b, Y_{1}), p(Y_{1}, b) ⇒; Fehlschlag; □, σ = {S/a}; p(b, b) ⇒; q(S, Y), p(Y, b) ⇒; □, σ = {S/b}; p(S, b) ⇒; 1; 2; 3; 1; 2]

Es ergeben sich drei verschiedene SLD-Ableitungen (inclusive einem Fehlschlag).

Definition Ein Erfolgszweig ist eine Kantenfolge von der Wurzel zum Blatt □, ein Mißerfolgszweig ist eine Kantenfolge von der Wurzel zu einem Blatt ≠ □, und ein unendlicher Zweig ist eine unendliche Knotenfolge von der Wurzel.

Nach Vollständigkeitssatz 5.19 gilt: Wenn P ∪ {A} unerfüllbar ist, dann enthält der SLD-Baum für P ∪ {A} einen Erfolgszweig. Wie findet man diesen?

Definition (SLD-Strategie) Eine SLD-Strategie (Suchregel) ist eine Methode zum Durchsuchen eines (SLD-) Baumes.

Erfolgreiche SLD-Strategie: Breitendurchlauf durch Ebene für Ebene des Baumes.

Beispiel:

        w
     /  |  \
    a   b   c
  / | \    / \
  x y z   r   s

Breitendurchlauf: w a b c x y z r s Sichere SLD-Strategie: Erfolgszweige werden immer gefunden. Nachteil: Hoher Verwaltungsaufwand. Speichere jeweils eine Ebene. Wenn jeder Knoten zwei Söhne hat, dann hat Ebene 10 (10 SLD-Schritte) 1024 Knoten! ⇒ riesiger Speicheraufwand. Diese Methode ist also für eine praktische Implementierung ungeeignet.

Daher verzichtet man in Prolog auf eine sichere Strategie. Unterschied zwischen Prolog und rein logischer Programmierung!

5.6 Beweisen in Prolog

Syntaktischer Vergleich:

logische Programme  Prolog
Konstanten: a,b,c,...  Atome: a,b,c,...

                             Zahlen: 0,1,...

Terme: f(...)  Struktur, Term: f(...)
Prädikate: p(...)  Prädikate: p(...)
Klauseln: ⇒ A  Faktum: A.
A_{1}, ..., A_{n} ⇒ A  Regel: A :- A1,...,An.
Anfrage: A_{1}, ..., A_{n} ⇒  Anfrage: ?- A1,...,An.

Semantischer Vergleich:

Deklarative Semantik  nur operationelle Semantik

⟺ operationelle Semantik

Programm: Menge von Klauseln Programm: Folge von Klauseln

(Ordnung: Reihenfolge der Eingabe)

Suchstrategie von Prolog: Tiefendurchlauf durch SLD-Baum Voraussetzung: Ordnung der Klauseln entspricht Ordnung der Söhne im SLD-Baum.

DFS(Knoten) = IF <Knoten ist Blatt>
              THEN <besuche Knoten>
              ELSE     { Knoten hat Soehne K1,...,Kn }
                <besuche Knoten>
                DFS(K1);
                ...
                DFS(Kn);

Für den Beispiel-Baum w: DF S(w): w a x y z b c r s

Problem bei DFS: Unendliche Zweige, die links von Erfolgszweigen stehen.

Beispiel: (1) p :- p., (2) p. DFS terminiert nicht, d.h. findet keine Lösung. Vermeidung durch Vertauschen von (1) und (2).

In Prolog sind zwei Reihenfolgen relevant:

1. Reihenfolge der Klauseln

2. Reihenfolge der Literale in rechten Regelseiten

Dadurch ergibt sich ein Unterschied zur logischen Programmierung (bei der keine Reihenfolgen existieren).

6 Nichtdeklarative Bestandteile von Prolog

Prolog: \underline{Pro}grammieren in \underline{Log}ik

Programm: Beschreibung logischer Sachverhalte. Der Computer zieht Schlußfolgerungen.

Diese Idealvorstellung ist praktisch nicht anwendbar. In diesem Kapitel fragen wir: wo sind Abstriche von der reinen Logik?

6.1 Beweisstrategie

Backtracking Verfahren:

• Lösungssuche in mehreren Schritten.

• Bei Alternative: probiere eine aus,

• bei Sackgassen: mache Beweisschritte rückgängig und probiere eine andere Alternative aus.

Prolog verwendet Backtracking zur Lösungssuche.

Resolutionsprinzip (ohne Unifikation) Um ?- A_{1}, ..., A_{k−1}, A_{k}, A_{k+1}, ..., A_{n}. zu beweisen, reicht es aus, ?- A_{1}, ..., A_{k−1}, L_{1}, ..., L_{p}, A_{k+1}, ..., A_{n}. zu beweisen, falls L :- L_{1}, ..., L_{p} und A_{k} = L. Auch auf Fakten anwendbar: p = 0 ⇒ Verkürzung der Anfrage. Kann eine Anfrage auf die leere Anfrage □ verkürzt werden, wird die Antwort ”yes“ gegeben.

Das Resolutionsprinzip ist nicht eindeutig:

1) Welches Literal einer Anfrage wird abgearbeitet?

2) Welche/s Regel/Faktum wird zur Abarbeitung verwendet?

Zu 1) In Prolog wird grundsätzlich das erste (=linke) Literal abgeleitet. Kapitel 5: Dies beeinflußt nicht die Vollständigkeit. Zu 2) Kapitel 5: Eine sichere Methode ist, alle Fakten/Regeln gleichzeitig zu untersuchen. Der Nachteil ist, daß dies sehr aufwendig ist. In Prolog wird daher auf diese sichere Methode verzichtet! Stattdessen wird das Backtracking-Verfahren verwendet.

1. Klauseln haben eine Reihenfolge (wie im Programmtext).

2. Im Beweisschritt: Wähle erste passende Klausel zur Ableitung des linken Literals. Bei Sackgassen: Mache Beweisschritt rückgängig und wähle nächste Klausel zur Ableitung.

3. Vor einem Beweisschritt: Benenne die Variablen aus der Klausel um, so daß sie verschieden von den Variablennamen in der Anfrage sind.

4. Bei einem Beweisschritt: Ersetze die Variablen durch Terme (Unifikation). Die Variablen werden gebunden bzw. instanziiert.

Die Punkte 1 bis 4 beschreiben Prologs Beweisstrategie.

Beispiel: Programm:

  p(a).
  p(b).
  q(b).
?- p(X),q(X).

⊢_{{X/a}} (1. Klausel)

?- q(a).

Sackgasse. Ableitung rückgängig machen

?- p(X),q(X).

⊢_{{X/b}} (2. Klausel)

?- q(b).

⊢_{{}} □, Antwort: X=b

Probleme der Beweisstrategie: Das Backtracking-Verfahren ist unvollständig.

Beispiel: Programm p:-p. p. Die Anfrage ?- p. terminiert nicht, obwohl ?- p. beweisbar ist.

Beispiel für Relevanz der Reihenfolge der Klauseln: Programm

  last([K|R],E) :- last(R,E).
  last([E],E).
?- last(L,3).

⊢_{{L=[K_{1}|R_{1}],E_{1}=3}} (1. Klausel)

?- last(R1,3).

⊢_{{R_{1}=[K_{2}|R_{2}],E_{2}=3}}

?- last(R2,3).

⊢ ... terminiert nicht. Bei Vertauschung der Klauseln:

?- last(L,3).

⊢_{{L=[E],E=3}} (Faktum) □, Antwort: L=[3]

Beispiel für Relevanz der Reihenfolge der Literale in rechten Regelseiten: Programm

  groesser_gleich (X,Z) :- groesser_gleich (Y,Z),
                          addiere_1 (Y,X).
  groesser_gleich (X,X).
  addiere_1 (0,S(0)).
  addiere_1 (S(X),S(Y)) :- addiere_1 (X,Y).

terminiert nicht bei ?- groesser_gleich (G,0). wegen linksrekursiver Regel (allgemein: p(...) :- p(...),...), terminiert aber bei Vertauschung der ersten beiden Regeln.

Fazit: Das Beweisverfahren von Prolog ist unvollständig. Nicht alles, was logisch beweisbar ist, kann Prolog herleiten. Durch Kenntnis der Beweisstrategie können Endlosbeweise vermieden werden:

1. Spezialfälle vor Allgemeinfällen

2. Vorsicht bei linksrekursiven Regeln

Bei Problemen mit Endlosbeweisen: Debugging.

6.2 Der ”Cut“-Operator

Prolog-Beweisstrategie: Backtracking. Bei Implementierung muß man sich die aktuellen Informationen an allen Alternativpunkten speichern. ⇒ bei langen Beweisen kann es zu einem Speicherüberlauf kommen. Durch ”!“ (Cut) kann der Benutzer das Backtracking teilweise unterdrücken. ⇒ geringerer Speicherbedarf. Der Cut schneidet Teile der SLD-Baumes ab. Diese Teile können Erfolgszweige enthalten! Bisher: eventuell Endlosbeweise statt ”yes“. Mit Cut: eventuell ”no“ statt ”yes“. Gründe für Cut:

1. Effizienz (Speicherbedarf, Laufzeit)

2. Kennzeichnen von Funktionen

3. Vermeidung von Laufzeitfehlern mit Arithmetik (”is“)

Konzept: ”!“ darf anstelle von Literalen auf rechten Regelseiten stehen: p :- q,!,r Bedeutung (prozedural): Falls diese Klausel zum Beweis verwendet wird, dann gilt:

1. Falls q nicht beweisbar ist, wähle nächste Klausel für p.

2. Falls q beweisbar ist, dann ist p nur dann beweisbar, wenn r beweisbar ist. (Also kein Alternativbeweis für q, keine andere Klausel für p.)

ja :- ab(X),!,X=b.
ja.
ab(a).
ab(b).

Dann ist rein logisch ?- ja. auf zwei Arten beweisbar. Dennoch antwortet Prolog mit ”no“. ⇒ Vorsicht mit Cut!

Sinnvolleres Beispiel:

istKindVon (K,E) :- weiblich (E), !, istMutterVon (E,K).
istKindVon (K,E) :- istVaterVon (E,K).

Häufig wird der Cut zur Fallunterscheidung genutzt:

p :- q, !, r.
p :- s.

entspricht ”if q then r else s.“

Beispiel:

max (X,Y,Z) :- X>=Y, !, Y=Z.
max (X,Y,Z) :- Y=Z.

6.3 Negation

Reine Logikprogramme erlauben keine Negation (negative Bedingungen). Für praktische Anwendungen ist Negation aber notwendig.

Beispiel:

istSchwesterVon (S,P) :- weiblich (S),
                         istMutterVon (M,S),
                         istMutterVon (M,P),
                         "not S=P".

Zur Formulierung negativer Aussagen bietet Prolog Negation als Fehlschlag:

\+p ( ⊬ p) ist beweisbar, falls alle Beweise für p fehlschlagen.

Beispiel:

?- \+ monika=susanne.
yes.
?- \+ maennlich (andreas).
no.

Negation als Fehlschlag ist nicht logische Negation.

Beispiel: p :- \+p. Bedeutung bei logischer Negation: ¬p ⇒ p ≡ ¬(¬p) ∨ p ≡ p. Das bedeutet: ?- p. müßte beweisbar sein. Prolog gerät jedoch in eine Endlosschleife.

Was ist die Bedeutung von \+ p. ? Ist p falsch (in allen Modellen)? Nein! Die Herbrandbasis B_{P} ist Modell von P, d.h. es gibt ein Modell, in dem p wahr ist. Dies bedeutet: \+p ist nie logische Konsequenz aus P.

Lösung: Closed World Assumption (CWA) (Reiter 1978): Falls ein variablenfreies Prädikat p nicht logische Konsequenz aus P ist, dann gilt ¬ p. (Also: alles, was nicht zwingend wahr ist, ist falsch.) CWA ist eine neue Inferenzregel. Da die ”logische Konsequenz“-Eigenschaft unentscheidbar ist, müssen wir das abschwächen:

Negation as (finite failure) (NF) (Clarke 1978): Falls alle Beweise für p fehlschlagen und endlich sind, dann gilt \+p.

NF ist schwächer als CWA: Falls der SLD-Baum für p fehlgeschlagen ist und einen unendlichen Zweig enthält, dann gilt \+p bezüglich CWA, aber nicht bezüglich NF.

Andererseits ist NF effektiv implementierbar:

Beispiel: p :- \+q. ist implementierbar durch

  p :- q, !, fail.
  p.

Was ist die logische Entsprechung zu NF? Die bisherige Semantik ist ungeeignet (Klauseln als Implikationen). Betrachte die Vervollständigung (Clark’s Completion) eines Programmes:

1. Sei = ein binäres Prädikatssymbol.

2. Sei p(t_{1}, ..., t_{n}) :– L_{1}, ..., L_{m} eine Klausel aus P. Dann transformiere diese in die Formel

(∃Y_{1}...∃Y_{l} X_{1} = t_{1} ∧ ... ∧ X_{n} = t_{n} ∧ L_{1} ∧ ... ∧ L_{m}) ⇒ p(X_{1}, ..., X_{n}).

Dabei seien X_{1}, ..., X_{n} neue Variablen und Y_{1}, ..., Y_{l} die ursprünglichen Variablen.

3. Seien F_{1} ⇒ p(X_{1}, ..., X_{n}), ..., F_{k} ⇒ p(X_{1}, ..., X_{n}) alle transformierten Klauseln für ein Prädikat p. Dann heißt

∀(F_{1} ∨ ... ∨ F_{k} ⟺ p(X_{1}, ..., X_{n}))

die vervollständigte Definition von p.

4. Die Gleichheitstheorie besteht aus folgenden Formeln:

• ∀X : X = X

• ∀X∀Y ∀Z : X = Y ∧ Y = Z ⇒ X = Z

• ∀X∀Y : X = Y ⇒ Y = X

• ∀(X_{1} = Y_{1} ∧ ... ∧ X_{n} = Y_{n} ⇒ f(X_{1}, ..., X_{n}) = f(Y_{1}, ..., Y_{n})) für alle Funktionssymbole f

• ∀(X_{1} = Y_{1} ∧ ... ∧ X_{n} = Y_{n} ∧ p(X_{1}, ..., X_{n}) ⇒ p(Y_{1}, ..., Y_{n})) für alle Prädikatssymbole p

• ∀(f(X_{1}, ..., X_{n}) ≠ g(Y_{1}, ..., Y_{m})) für alle Funktionssymbole f ≠ g

• ∀(X ≠ t), falls X in t vorkommt

• ∀(X_{1} ≠ Y_{1} ∨ ... ∨ X_{n} ≠ Y_{n} ⇒ f(X_{1}, ..., X_{n}) ≠ f(Y_{1}, ..., Y_{n})) für alle Funktionssymbole f (wobei s ≠ t für ¬(s = t) steht)

5. Die Vervollständigung (Clark’s Completion) eines Programmes P ist die Formelmenge bestehend aus der Gleichheitstheorie und den vervollständigten Definitionen der Prädikate. Bezeichnung: comp(P).

Intuitiv werden bei der Vervollständigung die Implikationen durch Äquivalenzen ersetzt. Dadurch erhalten wir die Entsprechung zur CWA-Regel. Wir definieren nun ”logische Konsequenz“ und ”korrekte“ Antworten bezüglich comp(P). Außerdem: Einschränkung der Selektionsfunktion S: S selektiert nur dann ein negatives Literal \+L, falls L variablenfrei ist. Problem: Floundering: Die Anfrage enthält nur noch negative Literale mit Variablen.

Definition (SLDNF-Resolution) Wie SLD-Resolution, jedoch mit folgender Abweichung: Bei Selektion eines negativen Literals \ + L: Berechne ?–L. Falls diese Berechnung nur Fehlschläge enthält und endlich ist, dann ist \ + L bewiesen.

SLDNF-Resolution ist korrekt bezüglich comp(P), aber im allgemeinen nicht vollständig wegen

1. Floundering

2. unendlichen Beweisen bei negativen Literalen Beispiel zu 1):

p(X).
q(a).
r(b).
?- p(X), \+q(X).

Rein logisch ist {X/b} eine korrekte Antwort. Diese Lösung kann aber nicht bewiesen werden.

Beispiel zu 2):

r :- \+p.
r :- p.
p :- p.

Hier ist die Identität {} eine korrekte Antwort bezüglich der Anfrage ?–r. Diese ist nicht berechenbar.

Vollständigkeitsergebnisse für eingeschränkte Klassen von Programmen und Zielen ⇒ Lloyd-Buch

Achtung: Selektionsfunktion nicht sicher! Negative Literale werden auch selektiert, wenn L noch Variablen enthält.

Negation as failure:

• keine Variablenbindung (Ausweg: ”konstruktive Negation“)

• nur variablenfreie Literale negieren (sonst falsche Antworten!)

Beispiel:

p(a,a).
p(a,b).
?- \+p(b,b).
yes.
?- \+\+p(b,b).
no.
?- \+p(X,b).

no. (← rein logisch: X = b !) ?- \+\+p(X,b). X=_0 (← rein logisch falsche Antwort, da z.B. falsch für X = b.)

⇒ Beim Beweis negativer Literale: Literal muß variablenfrei sein!

  istSchwesterVon (S,P) :- weiblich (S),
                          istMutterVon (M,S),
                          istMutterVon (M,P),
                          \+ S=P.     % darf nicht erste Bedingung sein

Ansonsten (falls \+ S=P erste Bedingung) würde

  ?- istSchwesterVon (angelika,P).

”no.“ ergeben (z.B. P = angelika)

Ausweg: verzögerte Negation (in den meisten Prolog-Systemen möglich; nicht in SWI-Prolog) Idee: Verzögere den Beweis von negativen Literalen \+L solange, bis L variablenfrei ist.

Beispiel:

  istSchwesterVon (S,P) :- \+S=P, weiblich(S),
                          istMutterVon (M,S),
                          istMutterVon (M,P).
  ?- istSchwesterVon (angelika,P).
⊢ ?- \+ angelika = P, weiblich (angelika),
    istMutterVon (M,angelika), istMutterVon (M,P).
⊢ ?- \+ angelika = P, istMutterVon (M,angelika), istMutterVon (M,P).
⊢ ?- \+ angelika = P, istMutterVon (christine,P).
⊢ ?- \+ angelika = herbert

→ ”yes“.

• Verzögerung zulässig wegen flexibler Selektionsstrategie

• Implementierung: Prolog-System mit Coroutining, z.B. Sicstus-Prolog:

     statt \+L nun: when(ground(L),\+L)

⇒ logisch korrekte Negation

6.4 Zyklische Strukturen

Unifikation: X = t: Binde X an t nur, falls X in t nicht vorkommt (occur check, Vorkommenstest) Fast alle Prolog-Systeme haben keinen occur check. Dann ist X = f(X) unifizierbar mit σ = {X/f(f(f(...))}: zyklische Struktur.

Probleme: Ausgabe und Unifikation zyklischer Strukturen; Logik wird zerstört.

  test :- X=1+X.
  ?- test.
  yes.

obwohl rein logisch test nicht beweisbar ist.

Unendliche Unifikation:

  ?- X=f(X), Y=f(Y), X=Y.

führt zu Endlosschleife. (Dies tritt in der Praxis aber kaum auf!)

6.5 Arithmetik

Bisher: 3 ∗ 5 verschieden von 15.

Definition (arithmetischer Ausdruck) Ein arithmetischer Ausdruck ist ein Term mit Funktoren +, −, /, ∗, mod (Infixoperatoren), +, − (Präfixoperatoren) und Zahlen und Variablen (← an arithmetische Ausdrücke gebunden).

Beispiel: 3 ∗ 5, X ∗ 5 + Y

is(X,Y) ist vordefiniert. is ist ein Infixoperator, und is(X,Y) ist beweisbar, wenn

1. Y ein variablenfreier arithmetischer Ausdruck ist und

2. der ausgerechnete Wert von Y (also eine Zahl) mit X unifizierbar ist.

  ?- 16 is 3*5+1.
  yes.
  ?- 2+1 is 2+1.
  no.

Anmerkungen:

1. is ist ein partielles Prädikat: es gibt eventuell eine Fehlermeldung, falls Y kein variablenfreier arithmetischer Ausdruck ist.

2. Die Reihenfolge bei der Verwendung von is ist relevant:

       ?- X=2, Y is 3-X.
       X=2, Y=1
       ?- Y is 3-X, X=2.

→ Fehlermeldung

Beispiel: Fakultätsfunktion (Reihenfolge wichtig!)

  fak (0,1).
  fak (N,F) :- N1 is N-1, fak (N1,F1), F is F1*N.
  ?- fak (6,F).
  F=720

6.6 Ein-/Ausgabe von Daten 53

Wird nun mit ”;“ die Berechnung einer zweiten Lösung aufgerufen, gerät Prolog in eine Endlosschleife (durch Berechnung von 0! mit der zweiten Regel). Dies kann vermieden werden, indem die erste Klausel in

  fak (0,F) :- !, F=1.

umgeschrieben wird. Vergleichsprädikate

• X =:= Y: Wertgleichheit

• X =\= Y: Wertungleichheit

   • X > Y
   • X < Y
   • X >= Y
   • X =< Y

Diese rechnen X und Y aus (wie bei is) und vergleichen die Ergebnisse. Weitere Arithmetik:

• Gleitkommazahlen (Punktnotation)

• Logarithmus, trigonometrische Funktionen Die Arithmetik ist logisch unvollständig:

  ?- 5 is 3+2.
  yes
  ?- X is 3+2.
  X=5
  ?- 5 is Y+2.

→ Fehler (Lösung: → Constraint Logic Programming)

6.6 Ein-/Ausgabe von Daten

Bisher: append(\underbrace{[a,f],[f,e]}_{Eingabe},L).

liefert Ausgabe L=[a,f,f,c]. Der write-Befehl: write (X)

• X beliebiger Term, • write (X) ist immer beweisbar (genau einmal)

• Nebeneffekt: Ausgabe von X auf dem Bildschirm, wobei die Operatoren berücksichtigt werden (Infix)

• Beim Backtracking kein Rücksetzen der Ausgabe

Beispiel:

?- write (+(2,3)), a=b.
2+3  no.

Der nl-Befehl: nl Wie write, aber Zeilenvorschub:

?- write (a), nl, write (b), nl.
a
b
yes.

Der read-Befehl: read (X)

• Nebeneffekt: Nächster Term wird gelesen (abgeschlossen mit ”.“ und Blank/Zeilenvorschub)

• beweisbar genau dann, wenn der gelesene Term mit X unifizierbar ist

• Es gibt nur einen Beweis.

• Kein Rücksetzen der Eingabe bei Fehlschlag (→ nichtlogisches Prädikat)

Beispiel: Kleine Interaktion für Verwandtschaftsbeispiel: Interaktive Ausgabe des Vaters:

vater :- write ('Wessen Vater?'), nl,
         read (P),
         istVaterVon (V,P),
         write ('Vater von'), write (P),
         write (' ist '), write (V), write ('.'), nl.
?- vater.
Wessen Vater?
maria.
Vater von maria ist anton.
yes.
?-

Ein-/Ausgabe einzelner Zeichen: get0(N) → N = ASCII-Wert des nächsten gelesenen Zeichens.

Weiter: Dateizugriff, Anschlüsse an Fenstersysteme

6.7 Zerlegung und Konstruktion von Termen

Der =..-Befehl: T=..L ist beweisbar, falls

• T Struktur, L Liste

• f(t_{1}, ..., t_{n}) = ..[f, t_{1}, ..., t_{n}]

• T und L dürfen beim Beweis nicht gleichzeitig Variablen sein.

Anwendung:

1. Zerlegung von Termen:

       ?- f(a,g(b)) =.. L.
       L = [f,a,g(b)]

2. Konstruktion von Termen:

       ?- T =.. [datum,1,3,90].
       T = datum(1,3,90)
Beispiel: sucheKonst (T,L):

(T Grundterm, L Liste der Konstanten in T)

  sucheKonst (T,L) :- addKonst (T,[],L).
  addKonst (T,L,[K|L]) :- T=..[K], !.     % T ist Konstante
  addKonst (T,L,NewL) :- T=..[F|Arg], addKonstInListe (Arg,L,NewL).
  addKonstInListe ([],L,L).
  addKonstInListe ([T|TListe],L,NewL) :-
          addKonst (T,L,LmitT),
          addKonstInListe (TListe,LmitT,NewL).
  ?- sucheKonst (3+4*5-f(a,b),L).
  L = [b,a,5,4,3]

Das var-Prädikat: var (X) beweisbar genau dann, wenn X eine freie Variable ist.

Erweiterung von sucheKonst auf Terme mit Variablen: Zusätzlich erste Klausel

  addKonst (T,L,L) :- var (T), !.

6.8 Daten als Programme

Die Klausel p :- q,r,s. entspricht dem Term :-(p,','(q,','(r,s))).

Umgekehrt: Terme ⇝ Programme

call (X)

• X instanziiert mit Term, der als Anfrage interpretiert wird (ohne ?-)

• beweisbar, falls ?- X. beweisbar ist Beispiel:

  ?- X=3, call(is(Y,X*2)).
  X=3
  Y=6
  ?- T =.. [is, Y, 2*5], call (T).
  T=10 is 2*5
  Y=10
map (P,L1,L2)

P Prädikat (zwei-stellig), map wendet P auf Elemente von L_{1} an.

Beispiel:

  zweifach (X,Y) :- Y is 2*X.
  ?- map (zweifach,[2,5,3],L).
  L=[4,10,6]
  map (P,[],[]).
  map (P,[E1|R1],[E2|R2]) :-
       T =.. [P,E1,E2],      % T = P(E1,E2)
       call (T),
       map (P,R1,R2).

Semantik: Prädikatenlogik zweiter Stufe (Quantifizierung über Prädikate)

6.9 Programme als Daten

Datenbank (des Prolog-Systems) = Folge aller Klauseln, die gegenwärtig dem System bekannt sind; Liste von Termen

Manipulation der Datenbank: Einfügen in die Datenbank:

• asserta (K) Seiteneffekt: Füge Klausel K am Anfang der Datenbank ein

• assertz (K) Seiteneffekt: Füge Klausel K am Ende der Datenbanl ein

Bei Backtracking: Einfügung bleibt.

Beispiel: (Datenbank leer)

  ?- asserta (:-(p,','(q,r))), asserta (p), fail.
  no.

Inhalt der Datenbank jetzt: p. p :- q,r.

?- listing. listet alle gegenwärtig bekannten Klauseln auf (bei Sicstus Prolog: nicht bei compiliertem Code)

neueKlauseln :- repeat,
                read (T),
                speicher_pruefe (T).
speicher_pruefe (end_of_file).
speicher_pruefe (T) :- assertz (T), !, fail.
repeat.
repeat :- repeat.

(repeat: unendliche viele Beweise → failure loop)

Löschen von Klauseln:

• retract (K). beweisbar, wenn in der Datenbank eine Klausel existiert, die mit K unifizierbar ist (K muß mindestens einen Prädikatnamen enthalten)

• Nebeneffekt: diese Klausel wird gelöscht.

• Backtracking: lösche weitere Klausel.

Beispiel: Löschen aller Klauseln eines Prädikats P (= p(X_{1}, ..., X_{n}) )

loescheKlauseln (P) :- retract (P), fail.
loescheKlauseln (P) :- retract (:- (P,Rumpf)), fail.
loescheKlauseln (P).
?- loescheKlauseln (letztes(L,E)).

• clause (H,B) beweisbar, wenn eine Klausel H :- B in der Datenbank existiert. (falls H. in Datenbank ⇒ B = true.)

7 Fortgeschrittene Programmiertechniken

7.1 Differenzlisten

append (L1,L2,L3)

• ist definiert über Aufbau der Liste L_{1}. ⇒ Laufzeit linear in Länge von L_{1}.

• Verbesserung: direkter Zugriff auf das Listenende

Differenzlisten: Liste darstellen als ”Differenz“ zweier Listen: [a,b,c] entspricht

[a,b,c,d] - [d]
[a,b,c] - []
[a,b,c|L] - L (allgemein)

Allgemein: Repräsentiere [e1,...,en] durch [e1,...,en|L]-L.

Vorteil: M-L Differenzliste ⇒ konstanter Zugriff auf das Ende (L)

Konkatenation von Differenzlisten:

  append_dl (L-M,M-N,L-N).
  ?- append_dl ([1,2|L1]-L1, [3,4|L2]-L2, L3).
  L3 = [1,2,3,4|L2]-L2

Nur ein Resolutionsschritt!

Anwendung: Umkehren einer Liste. Zunächst naiv:

  rev ([],[]).
  rev ([E|R],L) :- rev (R,UR), append (UR,[E],L).

Laufzeit: quadratisch in der Länge der ersten Liste.

Erste Verbesserung: Darstellung des zweiten Argumentes von rev als Differenzliste:

  rev_dl ([],L-L).
  rev_dl ([E|R],L-M) :- rev_dl (R,UR-T), append_dl (UR-T,[E|N]-N,L-M).
(T=[E|N], M=N, L=UR)

Zweite Verbesserung:

  rev_dl ([],L,L).
  rev_dl ([E|R],L,M) :- rev_dl (R,L,[E|M]).
  rev (L,M) :- rev_dl (L,M,[]).

⇒ lineare Laufzeit

Differenzlisten sind im allgemeinen kein universeller Ersatz für Listen sondern Listen mit offenem Ende, die genau einmal konkateniert werden können:

Beispiel:

  ?- DL = [a|L]-L,
     append_dl (DL,[b|M]-M,X),
     append_dl (DL,[c|N]-N,Y).
  no.

(L=[b|M] und L=[c|N], Widerspruch) ⇒ Der Benutzer muß die ”Einmal-Konkatenation“ sicherstellen!

7.2 Meta-Interpretierer

Programme ⟷ Daten: Programmierung eines Interpreters für Prolog in Prolog: Meta-Interpretierer

Vorteil: Erweitern von Meta-Interpretierern:

  \item{Beweisstrategie "andern}
  \item{Sprachumfang erweitern}
  \item{neue Programmierumgebungen (Debugger)}

Meta-Interpretierer für Prolog: prove (Goal)

  prove (true).
  prove ( (A,B) ) :- prove (A), prove (B).
  prove (A) :- clause (A,G), prove (G).

Beispiel:

  app ([],L,L).
  app ([E|R],L,[E|RL]) :- app (R,L,RL).
  ?- prove (app([1],[2],L)).
⊢ ?- clause (app([1],[2],L),G), prove (G).
⊢ ?- prove (app([],[2],RL)).    % L = [1|RL]
⊢ ?- clause (app([],[2],RL),G1), prove (G1).
⊢ ?- prove (true).              % RL = [2]

⊢ □; L = [1, 2]

Anmerkung:

• funktioniert so bei SWI-Prolog

• bei Sicstus Prolog: Definition aller Prädikate, auf die mit clause zugegriffen wird: :– dynamic p_{1}/n_{1}, ..., p_{k}/n_{k}

Erweitertet Meta-Interpretierer: Berechnung der Beweislänge: lprove (Goal, Length)

  lprove (true,0).
  lprove ( (A,B), L) :- lprove (A,LA), lprove (B,LB),
                        L is LA+LB.
  lprove (A,L) :- clause (A,G), lprove (G,LG), L is LG+1.
  ?- lprove (app ([a,b,c],[d],[a,b,c,d]), L).
  L = 4

Weitere Möglichkeiten:

• Ausgabe des Beweisverlaufs

• Interpretation mit Tiefenbeschränkung

• Vollständige Suche mit iterierter Tiefenbeschränkung

• Interpretation mit Lemma-Generierung

7.3 Debugging von Prolog-Programmen

Konzept: Jedes Literal, das bewiesen ist, entspricht einer Box (Box-Modell von Byrd):

[figure: Literal; call; fail; redo; exit]

Der Debugger zeigt jedes Betreten / Verlassen der Box an:

• call: erster Beweis des Literals

• redo: weitere Beweise

• exit: erfolgreicher Beweis

• fail: Fehlschlag

Beispiel:

p(a).
p(b).
q(b).
?- trace, p(X), q(X).
call:  p(_15)
exit:  p(a).
call:  p(a).
fail:  q(a).
redo:  p(
exit:  p(b).
call:  q(b).
exit:  q(b).
X=b

Tracer als Meta-Interpretierer:

tprove (true) :- !.
tprove ((A,B)) :- !, tprove (A), tprove (B).
tprove (A) :- callfail (A), clause (A,G),
              tprove (G), exitredo (A).
callfail (A) :- write ('call: '), write (A), nl.
callfail (A) :- write ('fail: '), write (A), nl, fail.
exitredo (A) :- write ('exit: '), write (A), nl.
exitredo (A) :- write ('redo: '), write (A), nl, fail.

8 Erweiterungen der reinen Logikprogrammierung

8.1 Flexible Berechnungsregeln

Probleme: bei links-rechts-Abarbeitung

• not P: warten, bis P variablenfrei

• Endlosschleifen:

     append ([],L,L).
     append ([E|R],L,[E|RL]) :- append (R,L,RL).
     ?- append ([1|V],W,L), append (L,X,[2|Y]).

(das erste Literal hat unendlich viele Lösungen: L = [1, , , , ...])

• Ineffiziente Berechnungen:

     sort (L,M) :- perm (L,M), ord (M).

⇒ Generierung von n! Permutationen (n = |L|)

• Laufzeitfehler bei Arithmetik:

     ?- X is Y+5, Y=3.

→ Error in arithmetic expression

Verzögerte Auswertung von Literalen (when-Deklaration):

?- append (X,Y,Z) when X or Z

(werte append nur aus, falls erstes oder drittes Argument an eine Struktur oder Konstante gebunden ist) Auswirkung im append-Beispiel:

?- append([1|V],W,L), append (L,X,[2|Y]).
⊢_{{L=[1|RL]}} ?- append (V,W,RL), append ([1|RL],X,[2|Y]).

(vorne V und RL beides Variablen; nicht auswerten!) ⊢ fail

Effizienzverbesserung:

sort (L,M) :- ord (M), prem (L,M).

(ord(M): korrekte Lösungen, perm(M): potentielle Lösungen)

?- ord(X) when X.
?- sort([4,3,2,1],L).

⊢ ?- ord(L), perm([4,3,2,1],L).
⊢ ... ⊢ ?- ord([4,3|R]), perm([4,3,2,1],[4,3|R]).

⊢ fail, Backtracking

Konsequenz: Es werden nicht alle Permutationen erzeugt.

Statt ”generate + test“ nun ”test + generate“ und when-Deklaration

Vermeidung von Laufzeitfehlern:

  ?- X is E when ground(E).
  ?- X is Y+5, Y=3.
⊢ ?- X is 3+5, Y=3.
  X=8

Flexible Berechnungsregeln:

• kein Standard (nicht implementiert in SWI)

• in vielen kommerziellen Systemen unterschiedlich realisiert

• Sicstus-Prolog: Block-Deklarationen

       :- block append (-,?,-)

(an erster und dritter Stelle: ungebundene Variablen)

⇒ blockiere Abarbeitung, falls erstes und drittes Argument ungebunden sind.

• Implementierung durch Koroutinen

• Bessere Beweiskontrolle durch automatische Transformation und Generierung von when-Deklarationen (NU-Prolog, Naish 1987)

• Computation = Logic + Control (Control: when-Deklarationen)

• Andorra-Berechnungsmodell (Warren 1987)

Erst deterministische Literale auswerten (deterministisch : ⟺ höchstens eine Klausel anwendbar)

1. Wende erst Resolutionsschritte auf alle deterministischen Literale an.

2. Falls eine Anfrage keine deterministischen Literale enthält: Resolutionsschritt für linkes Literal

8.2 Constraints

Motivation:

?- X is 5+3.
X=8
?- 8 is Y+3.
error

Prolog-Arithmetik ist logisch unsauber.

Konsequenz: Prolog-Programme nur noch in bestimmten Modi ausführbar. Lösung: Spezielle Verfahren zur Lösung von arithmetischen (Un)gleichungen

Arithmetische Constraints: (Un)gleichungen zwischen arithmetischen Ausdrücken ⇒ Constraint Logic Programming

Beispiel: Hypothekenberechnung Parameter:

P: Kapital

T: Laufzeit

IR: monatlicher Zinssatz

B: Restbetrag

MP: monatliche Rückzahlung

mortgage (P,T,IR,B,MP) :-
    T>0,
    T=<1, B=P*(1+T*IR)-T*MP.
mortgage (P,T,IR,B,MP) :-
    T>1,
    mortgage (P*(1+IR)-MP, T-1,IR,B,MP).

Monatliche Rückzahlung:

?- mortgage (100000,180,0.01,0,MP).
MP = 1200.17

Zeitdauer zur Finanzierung:

?- mortgage (100000,T,0.01,0,1400).
T = 125.901

Relation zwischen P,B,MP:

?- mortgage (P,150,0.01,B,MP).
P = 0.166783*B+83.3217*MP

CLP:

• Erweiterung der Logikprogrammierung

• Ersetze Terme durch constraint-Strukturen

• Ersetze Termunifikation durch Lösungsalgorithmen für Constraints. Beispiel: CLP(R) (IBM, R für reelle Zahlen)

• Struktur: Terme + reelle Zahlen

• Constraints: (Un)gleichungen mit arithmetischen Ausdrücken

• Lösungsalgorithmus:

– klassische Unifikation für Terme

– Gauß-Elimination für Gleichungen

– Simplex-Verfahren für Ungleichungen Weitere Constraint-Strukturen:

• Boolesche Ausdrücke (A and (B or C))

⇒ Hardware-Entwicklung und -verifikation

• unendliche zyklische Bäume (→ Graphen)

• Listen

• endliche Bereiche ⇝ Anwendungen in OR (Planungsaufgaben, z.B. Container-

beladung, Fertigung, Flughafenabfertigung, ...) CLP(X): Rahmen für CLP, X beliebige aber feste Constraint-Struktur, bestehend aus

• Signatur Σ (Menge von Funktions- und Prädikatsymbolen)

• Struktur D über Σ (entspricht Interpretation, d.h. Wertemenge + entsprechende Prädikate und Funktionen)

• Klasse L von Formeln über Σ (Teilmenge der PL 1)

• Theorie T (Axiomatisierung der wahren Formeln aus L, d.h. c ∈ L wahr gdw.

T ⊧ c Übliche Einschränkungen:

1. Σ enthält das Prädikat = (Identität auf D)

2. Es gibt Constraints ⊤, ⊥ ∈ L (top, bottom; entsprechen true und false)

3. L ist abgeschlossen unter Variablenumbenennung, Konjunktion, Existenzquantifizierung.

Klauseln über CLP(X): p(t̄) :– c, p_{1}(t̄_{1}), ..., p_{k}(t̄_{k}) mit t̄, t̄_{i} Folgen von Termen, c ∈ L Anfragen über CLP(X): ?– c, p_{1}(t̄_{1}), ..., p_{k}(t̄_{k}). , wobei c ∈ L erfüllbar. Resolutionsschritt mit p_{1}(s̄) :– c′, L_{1}, ..., L_{m} ergibt die Anfrage

?– c ∧ c′ ∧ t̄_{1} = s̄, L_{1}, ..., L_{m}, p_{2}(t̄_{2}), ..., p_{k}(t̄_{k})

falls c ∧ c′ ∧ t̄_{1} = s̄ erfüllbar.

Wesentliche Ergebnisse (Jaffar / Lassez: Popl ’87) Standardresultate von Logikprogrammierung (Korrektheit und Vollständigkeit) gelten analog in CLP(X). Notwendig: Algorithmus zur Entscheidung von Erfüllbarkeit in X (inkrementell: nicht in jedem Schritt wieder von vorne rechnen) z.B. X=IR: inkrementelle Version von

• Gauß-Eliminationsverfahren

• Simplexverfahren

Bei ”harten Constraints“: kein voller Erfüllbarkeitstest, sondern

• verzögerte Auswertung (z.B. nicht-lineare Constraints in CLP(IR): X ∗ Y = 5, warte, bis X oder Y einen festen Wert hat)

• nur lokale Konsistenzprüfung bei endlichen Domains (offensichtliche Widersprüche aufdecken) (CLP(FD)) (finite domains), da globale Konsistenzprüfung (Test auf Erfüllbarkeit) NP-vollständig → Van Heutenryck: Constraint Satisfaction in Logic Programming, MIT Press 1989

9 Implementierungen von Prolog

Möglichkeiten:

1. Interpretierer (portabel, ineffizient)

2. Übersetzer (effizient, weniger portabel)

3. Spezialhardware (möglicherweise effizient; Entwicklungszeit!, teuer

Meistverbreitet: Übersetzer Keine direkte Übersetzung in Maschinencode sondern in eine abstrakte Maschine:

• orientiert an Prolog

• effizient implementierbar auf Standard-Hardware

• Zwischenebene der Übersetzung ”Standardmaschine“ für Prolog: Warren’s Abstract Machine (WAM von D.H.D. Warren 1983; gute Beschreibung in Ait-Kaci, 1991)

Implementierung der WAM:

• Emulator in C (portabel, nicht sehr effizient)

• Übersetzung in C (portabel, gute Abstimmung mit Optimierung des C-Compilers nötig)

• Übersetzung in Maschinencode (effizient, aber nicht so portabel)

9.1 Grundideen der Warren Abstract Machine

Fasse Klauseln als Prozeduren auf

\underbrace{p(X, Y)}

Prozedurkopf

:– q(X), r(Y, Z), s(X, Z)

Prozedurrumpf

mit Parametern X, Y und lokaler Variable Z

Notation in imperativer Sprache:

  procedure p(X,Y);
  var Z;
  begin
    call q(X);
    call r(Y,Z);
    call s(X,Z)
  end

Alle Prozeduren sind rekursiv → Laufzeitstack zur Implementierung

• enthält lokale Variablen und Rücksprungadresse

• ”push“ bei Prozeduraufruf

• ”pop“ bei Prozedurende

Verfeinerung des vorigen Beispiels:

  p(X,Y): allocate X,Y,Z   % push, Speicher fuer X,Y,Z
          call q(X)
          call r(Y,Z)
          call s(X,Z)
          deallocate       % pop
          return

Parameterübergabe:

• Reserviere hierfür Argumentregister A_{1}, A_{2}, ...

• bei Prozeduraufruf: i-tes aktuelles Argument steht in A_{i}

• vor Prozeduraufruf: Lade aktuelle Argumente in A_{i}

• zu Beginn des Prozedurrumpfes: Schreibe A_{i} in entsprechende Variablen

Neue Befehle:

• get V, A_{i}: speichere Wert von A_{i} in Variable V

• put V, A_{i}: speichere Wert von V in A_{i}

p/2: allocate X,Y,Z
get X,A1
get Y,A2
put X,A1
call q/1
put Y,A1
put Z,A2
call r/2
put X,A1
put Z,A2
call s/2
deallocate
return

Argumente können komplexe Terme sein.

• get T, A_{i}: Unifiziere Term T mit Term, der in A_{i} steht

• put T, A_{i}: Speichere Term T in A_{i}

Beispiel: p(f(X), g(Y) :– q(h(g(X))).

p/2: allocate X,Y
get f(X),A1
get g(Y),A2
put h(g(X)),A1
call q/1
deallocate
return

Nachteil: In A_{i} stehen Terme (beliebig groß) Lösung: Speichere alle Terme in speziellem Bereich, genannt Heap. Register A_{i} und Variablen X, Y enthalten Verweise in den Heap.

Darstellung von Strukturen im Heap:

Funktor
1. Argument
...
n. Argument

(n + 1 Speicherzellen; in Argumenten eventuell Verweise auf Unterstrukturen)

Optimierung: Variablen und Konstanten direkt in Argumenten speichern. Notwendig: Markierung von Argumenten (Verweis? Konstante?) WAM-Darstellung von Prolog-Termen: Paar, bestehend aus

• Etikett (”tag“)

• Wert

Etikett Wert
reference Adresse
structure Adresse
list  Adresse der Liste
integer Wert der Zahl
atom  Nummer des Atoms

Atome (und Funktoren) durch Compiler numerieren. Listen: kein Abspeichern des Funktors →

1. Argument  (Listenkopf)
2. Argument  (Listenrest)

Variablen:

• gebundene Variablen: Verweis auf Bindung

• ungebundene Variablen: Verweis auf sich selbst

Beispiel: Darstellung von f(g(X), X) auf Heap:

...
1001: str   9
1002: ref   8
...
1039: str   f
1040: ref   1001
1041: ref   1002

• get T, A_{i}: unifiziere T mit A_{i}; falls notwendig, speichere T im Heap ab

• put T, A_{i}: erzeuge Darstellung von T im Heap, setze A_{i} auf die entsprechende Heap-Adresse Implementierung des Backtracking

Backtracking = Zurücksetzen auf früheren Berechnungszustand Naive Lösung:

• Vor einem Resolutionsschritt, bei dem es mehrere Alternativen gibt, speichere aktuellen Maschinenzustand und Verweis auf Alternative.

• Im Failure-Fall: Zurückspeichern des Maschinenzustandes und Sprung zur Alternative → Stack für Maschinenzustände

Beispiel:

  1)  p :- q,r.
  2)  p :- s.
  3)  q.
  4)  q :- u.
  ?- p.

Backtrack-Stack vor Aufruf von r:

  Zustand vor p, Alternative 2
  Zustand vor q, Alternative 4

Nachteil: Sicherung eines Zustandes sehr aufwendig Lösung: Statt den Heap vollständig im Backtrack-Stack zu speichern, protokolliere nur die Änderungen im Heap. Somit enthält der Backtrack-Stack nur einige Maschinenregister (z.B. Argumentregister A_{1}, ...) und Verweis auf nächste Alternative.

Neues Problem: Im Umgebungsstack stehen Umgebungen, die üblicherweise nach Verlassen der Prozedur (Klausel) gelöscht werden. Dadurch kann beim Backtracking eine passende Umgebung schon gelöscht worden sein:

Beispiel:

  1)  p :- q(X),r(X).
  2)  q(X) :- s(X).
  3)  r(1).
  4)  s(x) :- u(x).
  5)  s(x) :- v(x).
  6)  u(2).
  7)  v(1).
  ?- p.

Stackzustände vor u(x) in (4): Umgebung für (1) Zustand vor s(x), Alternative (5)

Umgebung für (2)

Umgebung für (4)

Somit hat der Umgebungsstack vor Aufruf von v(2) die folgende Form: Umgebung für (1)

Da der Beweis von v(2) fehlschlägt, muß der Zustand vor s(x) wiederhergestellt werden. Aber die Umgebung für die Klausel ist schon gelöscht worden.

Einfache Lösung: Speichere aktuellen Umgebungsstack im Backtracking-Stack. Nachteil: Viele Umgebungen werden mehrfach abgespeichert. Praktikable Lösung: Verschmelze Backtrack-Stack und Umgebungsstack zu einem Stack, so daß dieser sowohl Umgebungen als auch Backtrackpunkte enthält.

Beispiel: Stackzustand vor Aufruf von u(x):

Umgebung für (1)

Umgebung für (2)

Zustand vor u(x), Alternative (5)

Umgebung für (4)

Prinzip: Eine Umgebung wird nur dann gelöscht, wenn sich darüber kein Choicepoint befindet.

9.2 Die Warren Abstract Machine (WAM)

9.2.1 Speicherbereiche und Register der WAM

Die WAM enthält folgende Speicherbereiche:

• Code-Bereich: WAM-Instruktionen des auszuführenden Programmes

• Stack-Umgebungen:

1. Felder für Variablen

2. Verweis in den Rumpf einer anderen Klausel

3. Verweis auf eine andere Umgebung

• Stack: Backtrackpunkte: Informationen, um früheren Maschinenzustand wiederherzustellen

• Heap: Enthält nur Terme, die bei der Unifikation entstehen

• Trail: Protokolliert Variablen, die bei der Unifikation gebunden werden und die beim Backtracking auf ”ungebunden“ gesetzt werden müssen 9.2 Die Warren Abstract Machine (WAM) 71

• PDL (Push Down List): kleiner Stack zur Implementierung der Unifikation Code-Bereich → | Heap → | Stack → | Trail → ... ← PDL niedrige Adressen hohe Adressen Wichtig: Beim Schrumpfen des Stacks dürfen Variablenbindungen nicht in undefinierte Bereiche zeigen. Daher: bei einer Variablenbindung muß der Zeiger immer von der hohen zur niedrigen Adresse zeigen. Register:

Bezeichner Name
P  program pointer
CP  continuation program pointer
E  last environment
B  last backtrack point
TR  top of trail
H  top of heap
S  structure pointer (zu modifizierende Terme)
RW  read-write register
A_{1}, A_{2}, ... argument register
X_{1}, X_{2}, ... temporary variables

Eine Umgebung besteht aus folgenden Komponenten:

• ECP: letzter Wert von CP

• EE: letzter Wert von E

• Y_{1}, Y_{2}, ...: permanente Variablen Ein Backtrackpunkt enthält folgende Komponenten:

• BA_{1}, ..., BA_{n}: gesicherte Werte der Argumentregister

• BCP: gesicherter Wert von CP

• BCE: gesicherter Wert von E

• BB: gesicherter Wert von B

• BTR: gesicherter Wert von TR

• H: gesicherter Wert von H

• BP: Verweis auf die nächste alternative Klausel Definition (temporäre Variable) Eine Variable in einer Klausel ist temporär, wenn gilt:

1. Die Variable kommt im Kopf der Klausel, in einer Struktur oder im letzten Literal der Klausel vor.

2. Die Variable kommt nicht in zwei verschiedenen Literalen des Rumpfes vor.

3. Wenn die Variable im Klauselkopf vorkommt, dann kommt sie höchstens noch im ersten Literal des Rumpfes vor.

Definition (permanente Variable) Eine Variable ist permanent, wenn sie nicht temporär ist.

9.2.2 Instruktionssatz

Der Instruktionssatz der WAM:

Faktum  Rumpf (Literal) Rumpf (mehrere Literale)
p ← p ← q p ← q, r, s
get-Instr. für p get-Instr. für p allocate
proceed  put-Instr. für q get-Instr. für p
execute q  put-Instr. für q

call q,N

put-Instr. für r call r,N1 % N1 ≤ N put-Instr. für s deallocate execute s

• proceed: am Ende eines Faktums: P := CP (Programmzähler bzw. Continuation Pointer)

• execute L: am Ende eines Rumpfs (mit einem Literal): P := L (≡ Jump)

• allocate: erzeugt neue Umgebung:

Ce := E E := top of stack % kann berechnet werden aus E,B und letztem Aufruf E.ECP := CP E.EE := Ce

• deallocate: gibt aktuelle Umgebung frei:

CP := E.ECP E := E.EE

• call Pr,N: Aufruf eines Prädikats:

CP :=<Codeadresse nach dieser Anweisung> P := P r (N = # noch benötigter permanenter Variablen)

ECP ← E

EE Y_{1} ... Y_{n} top of stack

Instruktionen zur Verknüpfung von Klauseln: Seien K_{1}, ..., K_{m} alle Klauseln für p/n. Übersetzung:

p/n: try_me_else L2,n (← Erzeuge neuen Backtrack-Punkt, sichere Register A_{1}, ..., A_{n}, CP, E, B, T R, H; BP := L2)

< Code für K_{1} > L2: retry_me_else L3 (← Ändere nächste Alternative: B.BP := L3)

< Code für K_{2} >

  L3:  retry_me_else L4

... Lm: trust_me_else fail (← lösche aktuellen Backtrack-Punkt: B := B.BB)

Rückspeicherung aus dem Backtrack-Punkt: bei Fehlschlag (implizit in get-Instruktion)

Indizierung von Klauseln:

  1)  append ([],L,L).
  2)  append ([E|R],L,[E|RL]) :- ...

↑ Fallunterscheidung

  append/3: switch_on_term L1,L1c,L1l,fail
  L1:       try_me_else L2,3
  L1c:      < Code fuer (1) >
  L2:       trust_me_else fail
  L2l:      < Code fuer (2) >

(L1c für Konstanten, L1l für Listen)

Zu switch_on_term L1,L2,L3,L4 : Betrachte Argument A_{1}:

• freie Variable → P := L1

• Konstante → P := L2

• Liste → P := L3

• Struktur → P := L4

Weitere Indizierungsinstruktionen, Fallunterscheidung nach verschiedenen Konstanten Verfeinerung der get/put-Instruktionen

Struktur der Argumente ist zur Compile-Zeit bekannt ⇒ get/put-Instruktionen spezialisieren (→ Literatur)

Beispiel: p(g(X), f(a), X). WAM-Code: p/3: get_structure g/1,A1 % unifiziere A_{1} mit Strukturkopf g/1

unify_variable X1 % unifiziere erstes Argument von A_{1}

mit der temporären Variable X_{1}

      get_structure f/1,A2 % unifiziere A_{2} mit f

unify_constant a % unifiziere erstes Argument von A_{2} mit a get_value X1,A3 % unifiziere A_{3} mit Wert von X_{1}

      proceed

Weitere Optimierungen:

• bessere Registerallokation

• Vermeidung von Variablenumspeicherung

• Sortierung permanenter Variablen, so daß Speicherplatz frühzeitig frei wird (vergleiche call P r, \underline{N}) (”environment trimming“)

Beispiel:

  append ([],L,L).
  append ([E|R],L,[E|RL]) :- append (R,L,RL).

Optimierter Code:

  append/3: switch_on_term L1,L1c,L2l,fail
  L1:       try_me_else L2,3
  L1c:      get_nil A1
            get_value A2,A3   % Unif. von A2,A3
            % optimiert: nicht mehr in Hilfsvariablen laden
            proceed
  L2:       trust_me_else fail
  L2l:      get_list A1
            unify_variable X4   % X4=E
            unify_variable A1   % R=A1  (Optimierung!)
            get_list A3
            unify_value X4      % Unif.
            unify_variable A3   % RL=A3
               % Optimierung: bessere Register-Allokation
            execute append/3

Eigenschaften:

• kein Anlegen von Umgebungen

• kein rekursiver Aufruf (execute = jump) (tail recursion optimization)

• Aufbau von Backtrack-Punkten nur, falls ein Argument freie Variable

• ?– append([1, 2, 3, ..., n], [....], L). ⇒ Abarbeitung wie bei while-Schleife

• Einzelne WAM-Instruktionen sind leicht implementierbar → MC-Code

9.3 Globale Analyse

Zur Compilezeit: Laufzeitinformationen ausnutzen: Modi von Prädikaten (Argumente innen gebunden oder frei) → Spezialisierung von get-Instruktionen Typ von Argumenten: immer Listenstruktur Problem: Laufzeitaspekte unentscheidbar. Lösung: Approximation → abstrakte Interpretation. Systeme: Aquarius-Prolog (Peter van Roy) → > 1.000.000 Regelschritte pro Sekunde; schneller als optimierender C-Compiler.

Index

=.., 55 Äquivalenz der deklarativen und ope-

rationellen Semantik, 40 Übersetzer, 19 äquivalent, 29

ableitbar, 36 Ableitungen

Ein-Schritt-, 34 Abtrennungsregel, 10 Allabschluß, 35 allgemeines Resolutionsprinzip, 14 allgemeingültig, 26 allgemeinster Unifikator, 12 Allquantor, 23 Andorra-Berechnungsmodell, 62 Anfrage, 6, 10, 24 Anonyme Variable, 9 Antisymmetrie, 31 Antwort, 35

S-berechnet, 37 Argumentregister, 67 Arithmetik, 52 Arithmetische Constraints, 63 arithmetischer Ausdruck, 52 Assoziativität, 8 Atome, 7 Aufzahlung des Suchbaums, 15 Ausdruck

arithmetisch, 52 Auswahlregel, 35

Backtracking, 44 Implementierung, 69 unvollstandig, 45

Beweisen mit Resolutionsprinzip, 15 Block-Deklarationen, 62 bottom, 32 Box, 60 Breitendurchlauf, 42 Byrd, 60

call, 55 Clark’s Completion, 48, 49 Clarke, 48 Closed World Assumption, 48 CLP, 63 CLP(X), 64 Code-Bereich, 70 Colmeraner, 3 Constraint, 53 Constraint Logic Programming, 63 Constraint-Struktur, 64 Constraints, 62 Coroutining, 51, 62 Cut, 46

Fallunterscheidung, 47 CWA, 48

Datenbank, 56 Datenstrukturen, 20 Debugger, 60 Debugging, 46 Definition

vervollstandigt, 49 deklarative Semantik, 35 Differenzieren

symbolisch, 18 Differenzlisten, 57 disagreement set, 12 Disjunktion, 23 dynamische Semantik, 35

Effizienz Beweisverfahren, Hornklauseln, 31 Cut, 46

Ein-Schritt-Ableitungen, 34 Elementare Programmiertechniken, 15 Elimination von Existenzquantoren, 29 erfüllbar, 26 Erfüllbarkeitsäquivalenz, 30 erfolgreiche SLD-Ableitung, 37 Erfolgszweig, 42 Existenzquantor, 23 Existenzquantoren

Eliminierung (Skolem), 29

Fakten, 10

Prolog, 5 Faktum, 24 Fallunterscheidung, 47 fehlerhafte Unifikation, 13 fehlgeschlagene SLD-Ableitung, 37 Fixpunktcharakterisierung des kleinsten

Herbrand-Modelles, 35 Floundering, 49 Formel, 23

geschlossen, 23 Formeln

Transformation in Klauseln, 28 frei, 23 Funktionen

als Relationen, 19 Kennzeichnen mit Cut, 46

Funktor Prolog, 7

gebunden, 23, 45 gerichtet, 32 geschlossene Formel, 23 get0, 54 glb(A), 32 Gleichheit

Prolog, 15 Gleichheitstheorie, 49 Globale Analyse, 75 größte untere Schranke, 32 größter Fixpunkt, 32 größtes Element, 32 greatest lower bound, 32 Grundinstanz, 34 Grundterm, 9

Heap, 67, 70 Herbrand-Basis, 27 Herbrand-Interpretation, 27 Herbrand-Modell, 28

kleinstes, 33 Herbrand-Universum, 27 Homomorphismus, 11 Hornklausel, 24 Implementierung des Backtracking, 69 Implikation, 23 Inferenzregel, 48 Infixoperator, 8 instanziiert, 45 Instruktionssatz der WAM, 72 Interpretation, 25

syntaktische: Herbrand-, 28 Term-, 28

is, 52

Klammern, 8 Klausel, 6, 24 Kleene

Satz von, 33 kleinste obere Schranke, 31 kleinster Fixpunkt, 32 kleinstes Element, 32 kleinstes Herbrand-Modell, 33 KNF, 30 Konjunktion, 23 Konjunktive Normalform, 30 Konstanten

Prolog, 7 Konstruktion von Termen, 55 konstruktive Negation, 50 Kopf, 24 Koroutinen, 62 korrekt, 35 Korrektheit

Unifikationsalgorithmus, 13 Kowalski, 3

Satz von, 33

least upper bound, 31 leere Klausel, 24 Lifting-Lemma, 39 linksassoziativ, 8 linksrekursiv, 46 Listen, 7

Prolog, 7 Literal, 10, 24 Lloyd, 50 Logikprogrammierung

Prinzip der, 3

theoretische Grundlagen, 22 logisch äquivalent, 28, 29 logische Konsequenz, 26 logische Programme, 22 logisches Programm, 24 lub(A), 31

Manipulation der Datenbank, 56 map, 56 markierte Bäume, 40 Meta-Interpretierer, 59 mgu, 12 mgu-Lemma, 38 Mißerfolgszweig, 42 Modell, 26 Modus ponens, 10 monoton, 32 most general unifier, 12 Muster, 17

Naish, 62 Negation, 11, 23

verzogert, 51 Negation als Fehlschlag, 47 Negation as (finite failure), 48 NF, 48 Nichtdeterminismus, 11 Nichtterminierung, 11 nl, 54

obere Schranke, 31 Objekte

Prolog, 7 occur check, 13, 51

fehlerhafte Unifikation, 13 zyklische Terme, 13

Operationelle Semantik, 37 operationelle Semantik, 35 Operator

Infix-, 8 Postfix-, 8 Prafix-, 8

Operator T_{P}, 34 Operatoren

Prolog, 8 Ordinalzahlen, 33 partielle Ordnung, 31 Pattern, 17 PDL, 71 Pereira, 3, 19 permanent, 72 permanente Variable, 72 Postfixoperator, 8 Prädikat, 22 Prädikatenlogik erster Stufe, 22, 23 Pränex-Form, 29 Präzedenz, 8 Pradikat

Prolog, 6 Pradikatenlogik

erster Stufe, 6 Prafixoperator, 8 Programmiertechniken elementare, 15 Programmklausel, 24 Prolog, 3

Anfrage, 6 Gleichheit, 15 Klausel, 6 Objekte, 7 Pradikat, 6 Regeln, 5 Relation, 6 Zahlen, Atome und Strukturen, 7

Prolog-Syntax, 4

Prologs Beweisstrategie, 45 prozedurale Semantik, 35 Push Down List, 71

quantifiziert, 23

read, 54

rechtsassoziativ, 8 Reflexivität, 31 Regeln, 10

in Prolog, 5 Register der WAM, 71 Reiter, 48 Relation

Prolog, 6 Resolutionsprinzip, 3, 44 allgemeines, 14 beweisen mit, 15 einfach, 10 einfaches, 10

Resolvente, 36 Robinson, 3, 12

Unifikationssatz, 13 Roussel, 3 Rumpf, 24

S-berechnete Antwort, 37 Satz von Kleene, 33 Satz von Tarski, 32 Satz von van Emden und Kowalski, 33 Schranken, 31 Semantik

deklarativ, 35 deklarative, 33 dynamische, 35 operationelle, 35 prozedurale, 35 statisch, 35

Sichere SLD-Strategie, 42 Skolemform, 30 Skolemisierung, 29 SLD-Ableitung, 36

erfolgreich, 37 fehlgeschlagen, 37 unendlich, 37

SLD-Baum, 40, 41 SLD-Resolution, 35

Korrektheit, 37 Vollständigkeit, 38, 40

SLD-Resolutionsschritt, 36 SLD-Strategie, 42

sicher, 42 SLD-Widerlegung, 37

uneingeschränkt, 37 SLDNF-Resolution, 49 Stack, 70 Stack-Umgebungen, 70 statische Semantik, 35 Stelligkeit, 23 stetig, 32 Strukturen

Prolog, 7 strukturerhaltend, 11 Substitution, 11 Suchbaum, 15 Suchraum, 16 Suchregel, 42 symbolisches Differenzieren, 18 Syntax

Prolog, 4

Tarski

Satz von, 32 Term, 9, 22 Term-Interpretation, 28 Termgleichheit, 9 Terminierung

Unifikationsalgorithmus, 13 Theorembeweiser, 31 theoretische Grundlagen der Logikpro-

grammierung, 22 Tiefendurchlauf, 43 top, 32 Tracer, 60 Trail, 70 Transformation in Pränex-Form, 29 Transformation von Formeln in Klau-

seln, 28 Transitivität, 31

Umkehrfunktion, 19 Umkehrrelation, 19 uneingeschränkte SLD-Widerlegung, 37 unendliche SLD-Ableitung, 37 unendlicher Zweig, 42 unentscheidbar

Eigenschaft ‘logische Konsequenz’,

48 Pradikatenlogik erster Stufe, 6

unerfüllbar, 26 Unerfüllbarkeitstests, 30 Unifikation, 10, 12

fehlerhafte, 13 Unifikationsalgorithmus, 12

Korrektheit, 13 Terminierung, 13 Unifikationssatz, 38 Unifikationssatz von Robinson, 13 Unifikator, 12

allgemeinster (mgu), 12 unifizierbar, 12 Universum, 25 Unstimmigkeitsmenge, 12 untere Schranke, 31 unvollstandig

Backtracking, 45

van Emden

Satz von, 33 var, 55 Variable

anonyme, 9 frei, 23 gebunden, 23 permanent (WAM), 72 temporar (WAM), 71

Variablen, 5, 9 Variablenbelegung, 25 Variablennamen, 9 Verband, 32 Vergleich Prolog vs. imperative Spra-

chen, 6 Vier-Farben-Problem, 15 vollständiger Verband, 32 Vollständigkeit der SLD-Resolution, 38,

40 Vorkommenstest, 13, 51

wahr, 25 Wahrheit von Formeln, 25 WAM, 66

Register, 70, 71 Speicherbereiche, 70

WAM-Darstellung von Prolog-Termen,

68 Warren, 3, 19, 62 Warren’s Abstract Machine, 66 Warren, D.H.D., 66 when, 61 Widerspruchsbeweis, 37 write, 53 Zahlen

Prolog, 7 Zeichen

Prolog, 7 Zerlegung von Termen, 55 zyklische Struktur, 51 zyklische Terme, 13