Document

Transcript

Logik für Informatiker Wintersemester 2015/16 Logik für Informatiker im Wintersemester 2015/16 Prof. Dr. Dietmar Seipel Prof. Dr. Dietmar Seipel Logik für Informatiker Wintersemester 2015/16 Inhaltsverzeichnis Vorwort v 1 Aussagenlogik 1 1.1 Grundbegriffe der Aussagenlogik . . . . . . . . . . . . . . . 1 1.2 Äquivalenz und Normalformen . . . . . . . . . . . . . . . . 36 1.3 Hornformeln . . . . . . . . . . . . . . . . . . . . . . . . . 74 1.4 Minimale Modelle für Klauselmengen . . . . . . . . . . . . 89 1.5 Der Endlichkeits/Kompaktheits–Satz . . . . . . . . . . . . . 110 1.6 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 Prof. Dr. Dietmar Seipel ii Logik für Informatiker Wintersemester 2015/16 2 Prädikatenlogik 151 2.1 Grundbegriffe der Prädikatenlogik . . . . . . . . . . . . . . 152 2.2 Normalformen . . . . . . . . . . . . . . . . . . . . . . . . . 183 2.3 Unentscheidbarkeit . . . . . . . . . . . . . . . . . . . . . . 213 2.4 Herbrand–Theorie . . . . . . . . . . . . . . . . . . . . . . . 218 2.5 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 241 2.6 Hyperresolution für Hornformeln . . . . . . . . . . . . . . . 283 2.7 SLD–Resolution . . . . . . . . . . . . . . . . . . . . . . . 302 Prof. Dr. Dietmar Seipel iii Logik für Informatiker Wintersemester 2015/16 3 Logikprogrammierung 337 3.1 Grundlagen von P ROLOG . . . . . . . . . . . . . . . . . . . 338 3.2 SLDNF–Resolution . . . . . . . . . . . . . . . . . . . . . . 389 3.3 Sortieren und Suchbäume . . . . . . . . . . . . . . . . . . . 399 3.4 Suche in Graphen . . . . . . . . . . . . . . . . . . . . . . . 423 Literatur Prof. Dr. Dietmar Seipel 438 iv Logik für Informatiker Wintersemester 2015/16 Vorwort Anwendungen: • Zermelo und Fraenkel: Axiome der Mengenlehre • Formulierung von Theoremen: Fermat • Theorembeweisen • Boolesche Schaltkreise: Analyse und Optimierung • Datenbanken: S QL • Logikprogrammierung: P ROLOG • Semantic Web: Ontologien, OWL, S WRL • ... Prof. Dr. Dietmar Seipel v Logik für Informatiker Wintersemester 2015/16 Mathematische Axiome und Theoreme Die Russellsche Antinomie ist ein von Bertrand Russell und Ernst Zermelo entdecktes Paradoxon der naiven Mengenlehre, das Russell 1903 publizierte. Dies führte zur Entwicklung der axiomatischen Mengenlehre. Russell bildete seine Antinomie mit Hilfe der ”Klasse aller Klassen, die sich nicht selbst als Element enthalten”, die als Russellsche Klasse R bezeichnet wird, vgl. Wikipedia: R := { x | x ∈ / x }. Oft wird die Russellsche Klasse auch als ”Menge aller Mengen, die sich nicht selbst als Element enthalten” definiert; das entspricht der damaligen Mengenlehre, die noch nicht zwischen Klassen und Mengen unterschied. In der axiomatischen Mengenlehre weiß man, daß es eine solche Menge nicht geben kann. Prof. Dr. Dietmar Seipel vi Logik für Informatiker Wintersemester 2015/16 Die Logik bietet einen exakten Formalismus zur Repräsentation und Verarbeitung von mathematischem Wissen in Form von • Axiomen und • Theoremen. Beim Theorembeweisen können mit Hilfe von Kalkülen automatisch neue Theoreme aus den Axiomen und den bereits bekannten Theoremen hergeleitet werden. Durch die steigende Rechnerleistung ist zu erwarten, daß zukünftig verstärkt Theoreme automatisch oder semi–automatisch bewiesen werden können. Prof. Dr. Dietmar Seipel vii Logik für Informatiker Wintersemester 2015/16 Zermelo und Fraenkel: Axiome der Mengenlehre vgl. Wikipedia ZF hat unendlich viele Axiome, da zwei Axiomenschemata (8. und 9.) verwendet werden, die zu jedem Prädikat mit bestimmten Eigenschaften je ein Axiom angeben. Als logische Grundlage dient die Prädikatenlogik der ersten Stufe mit Identität und dem undefinierten Elementprädikat ∈. Die Infix–Notation A ∈ B ist gleichbedeutend mit der Präfix–Notation ∈ (A, B). 1. Extensionalitätsaxiom oder Axiom der Bestimmtheit: Zwei Mengen sind genau dann gleich, wenn sie dieselben Elemente enthalten. ∀A ∀B (A = B ←→ ∀C (C ∈ A ←→ C ∈ B)) Prof. Dr. Dietmar Seipel viii Logik für Informatiker Wintersemester 2015/16 2. Leermengenaxiom oder Nullmengenaxiom: Es gibt eine Menge ohne Elemente. ∃B ∀A ¬(A ∈ B) Aus dem Extensionalitätsaxiom folgt unmittelbar die Eindeutigkeit dieser Menge B, das heißt, daß es auch nicht mehr als eine solche Menge gibt. Diese wird meist als ∅ geschrieben und leere Menge genannt. Das bedeutet: Die leere Menge ist in ZF das einzige Urelement. Andere Urelemente sind nur beim allgemeineren originalen Axiom der Bestimmtheit von Zermelo möglich. Prof. Dr. Dietmar Seipel ix Logik für Informatiker Wintersemester 2015/16 3. Paarmengenaxiom: Für alle A und B gibt es eine Menge C, die genau A und B als Elemente hat. ∀A ∀B ∃C ∀D (D ∈ C ←→ (D = A ∨ D = B)) Auch diese Menge C ist eindeutig bestimmt. Sie wird geschrieben als {A, B}. Die Menge {A, A} wird üblicherweise als {A} geschrieben. 4. Vereinigungsaxiom: Für jede Menge A gibt es eine Menge B, die genau die Elemente der Elemente von A als Elemente enthält. ∀A ∃B ∀C (C ∈ B ←→ ∃D (D ∈ A ∧ C ∈ D)) Auch die Menge B ist eindeutig bestimmt und heißt die Vereinigung ∪ der Elemente von A, geschrieben als A. Zusammen mit dem ∪ Paarmengenaxiom lässt sich die Vereinigung A ∪ B := {A, B} definieren. Prof. Dr. Dietmar Seipel x Logik für Informatiker Wintersemester 2015/16 5. Unendlichkeitsaxiom: Es gibt eine (induktive) Menge A, die • die leere Menge ∅ und • mit jedem Element x auch die Menge x ∪ {x} enthält. ∃A ( ∃ X ∈ A ∀ Y ∈ A ¬(Y ∈ X) ∧ ∀X (X ∈ A → X ∪ {X} ∈ A) ) Es gibt viele derartige Mengen. Der Schnitt aller dieser Mengen ist die kleinste Menge mit diesen Eigenschaften und bildet die Menge der natürlichen Zahlen; die Bildung der Schnittmenge erfolgt durch Anwendung des Aussonderungsaxioms (s.u.). Die natürlichen Zahlen werden also dargestellt durch IN := {∅, {∅}, {∅, {∅}}, {∅, {∅}, {∅, {∅}}} , . . . }. Prof. Dr. Dietmar Seipel xi Logik für Informatiker Wintersemester 2015/16 Die weiteren Axiome (6. bis 10.) führen wir ohne prädikatenlogische Definition der Vollständigkeit halber auf: 6. Potenzmengenaxiom, 7. Fundierungsaxiom oder Regularitätsaxiom, 8. Aussonderungsaxiom, 9. Ersetzungsaxiom (Fraenkel), 10. Auswahlaxiom. Prof. Dr. Dietmar Seipel xii Logik für Informatiker Wintersemester 2015/16 6. Potenzmengenaxiom: Für jede Menge A gibt es eine Menge P , deren Elemente genau die Teilmengen von A sind. 7. Fundierungsaxiom oder Regularitätsaxiom: Jede nichtleere Menge A enthält ein Element B, so dass A und B disjunkt sind. Das Element B, welches zu A disjunkt ist, ist im allgemeinen nicht eindeutig bestimmt. Das Fundierungsaxiom verhindert, dass es unendliche oder zyklische Folgen von Mengen gibt, bei denen jeweils eine in der nächsten enthalten ist, x1 3 x2 3 x3 3 . . . , denn dann könnte man eine Menge A = {x1 , x2 , x3 , . . . } bilden, die dem Axiom widerspricht: Für jedes xi ∈ A ist xi+1 ∈ xi ∩ A, die beiden Mengen sind also nicht disjunkt. Prof. Dr. Dietmar Seipel xiii Logik für Informatiker Wintersemester 2015/16 8. Aussonderungsaxiom: Hier handelt es sich um ein Axiomenschema mit je einem Axiom zu jedem einstelligen Prädikat P : Zu jeder Menge A existiert eine Teilmenge B von A, die genau die Elemente C von A enthält, für die P (C) wahr ist. Aus dem Extensionalitätsaxiom ergibt sich sofort, daß es genau eine solche Menge gibt. Diese wird mit { C ∈ A | P (C) } notiert. 9. Ersetzungsaxiom (Fraenkel): Ist A eine Menge und wird jedes Element von A eindeutig durch eine beliebige Menge ersetzt, so geht A in eine Menge B über. Die Ersetzung wird präzisiert durch zweistellige Prädikate mit ähnlichen Eigenschaften wie eine Funktion, und zwar als Axiomenschema für jedes zweistellige Prädikat F : Die Menge B ist eindeutig bestimmt und wird als { Y | D ∈ A ∧ F (D, Y ) } notiert. Prof. Dr. Dietmar Seipel xiv Logik für Informatiker Wintersemester 2015/16 10. Auswahlaxiom: Ist A eine Menge von paarweise disjunkten nichtleeren Mengen, dann gibt es eine Menge, die genau ein Element aus jedem Element von A enthält. Dieses Axiom hat eine komplizierte Formel, die mit dem Eindeutigkeitsquantor ∃! etwas vereinfacht werden kann: Eine andere übliche verbale Formulierung des Auswahlaxioms lautet: Ist A eine Menge nichtleerer Mengen, dann gibt es eine Funktion f (von A in seine Vereinigung), die jedem Element B von A ein Element von B zuordnet (ein Element von B auswählt). In der Mathematik wird häufig auch das Auswahlaxiom benutzt, das ZF zu ZFC erweitert. Prof. Dr. Dietmar Seipel xv Logik für Informatiker Wintersemester 2015/16 Theorem von Fermat Sei n > 2 eine beliebige ganze Zahl. Dann erfüllen keine 3 positiven ganzen Zahlen a, b und c die Gleichung an + bn = cn . Für n = 2 findet man leicht solche Zahlen (vgl. auch Satz von Pythagoras). ∀ n ∈ IN ( n > 2 −→ ¬ (∃ a ∈ IN+ ∃ b ∈ IN+ ∃ c ∈ IN+ (an + bn = cn )) ). Dieses Theorem wurde schon im Jahre 1637 von Pierre de Fermat postuliert, es konnte aber erst 1995 von Andrew Wiles vollständig bewiesen werden. Komplexitätstheorie Eine bislang immer noch unbeantwortete Frage der theoretischen Informatik ist, ob die beiden Komplexitätsklassen P und N P gleich sind. Prof. Dr. Dietmar Seipel xvi Logik für Informatiker Wintersemester 2015/16 Logische Schaltkreise: Analyse und Optimierung Prof. Dr. Dietmar Seipel xvii Logik für Informatiker Wintersemester 2015/16 Datenbanken und Logikprogrammierung Relationen in einer Familien–Datenbank: PARENT NAME PARENT Elizabeth George Charles Elizabeth William Charles G RANDPARENT NAME G RANDPARENT Charles George William Elizabeth Die Menge aller logischen Fakten zu einem n–stelligen Prädikat – hier parent und grandparent – entspricht einer n–stelligen Relation: parent(’Elizabeth’, ’George’), parent(’Charles’, ’Elizabeth’), parent(’William’, ’Charles’). Analog: 3 Fakten für grandparent. Prof. Dr. Dietmar Seipel xviii Logik für Informatiker Wintersemester 2015/16 Familienstammbaum: - Charles Diana George - Elizabeth Philip - - William - Harry Anne - Andrew - Edward Der Familienstammbaum umfaßt hier 4 Generationen; Frauen sind in Rot, Männer in Blau angezeigt. Prof. Dr. Dietmar Seipel xix Logik für Informatiker Wintersemester 2015/16 Berechnung der Großeltern: • in Datenbanken: Tupelkalkül { p1 .name, p2 .parent | parent(p1 ) ∧ parent(p2 ) ∧ p1 .parent = p2 .name } • in der Logikprogrammierung: Bereichskalkül { X, Z | parent(X, Y ) ∧ parent(Y, Z) } Tupelvariablen p1 und p2 ; Bereichsvariablen X, Y und Z. Im Tupelkalkül werden Verbundbedingungen explizit angegeben, wogegen ein Verbund im Bereichskalkül durch gleichbenannte Variablen gebildet wird. Prof. Dr. Dietmar Seipel xx Logik für Informatiker Wintersemester 2015/16 Logikprogrammierung: P ROLOG Prädikatensymbole: parent, grandparent, ancestor , alle 2–stellig Regeln: Kopf ← Rumpf , man sagt “ Kopf falls Rumpf ” Rumpf ist Konjunktion von Atomen oder deren Negation grandparent(X , Z ) ← parent(X , Y ) ∧ parent(Y , Z ) ancestor (X , Y ) ← parent(X , Y ) ancestor (X , Z ) ← ancestor (X , Y ) ∧ parent(Y , Z ) Bedeutung: ∀X, Y, Z : ((ancestor(X, Y ) ∧ parent(Y, Z)) → ancestor(X, Z)) Fakten: parent(’Elizabeth’, ’George’) parent(’Charles’, ’Elizabeth’) parent(’William’, ’Charles’) Prof. Dr. Dietmar Seipel xxi Logik für Informatiker Wintersemester 2015/16 Z Man kann mittels der Regel grandparent(X , Z ) ← parent(X , Y ) ∧ parent(Y , Z ) z.B. folgende neuen Fakten ableiten. I parent 6 Y grandparent parent 6 X Dazu ersetzt man in der Regel die Variablen wie folgt: • Für { X 7→ ’Charles’, Y 7→ ’Elizabeth’, Z 7→ ’George’ } erhalten wir grandparent(’Charles’, ’George’) ← parent(’Charles’, ’Elizabeth’) ∧ parent(’Elizabeth’, ’George’). Mit Hilfe der entsprechenden Fakten aus dem Regelrumpf kann man dann grandparent(’Charles’, ’George’) ableiten. • Für { X 7→ ’William’, Y 7→ ’Charles’, Z 7→ ’Elizabeth’ } kann man grandparent(’William’, ’Elizabeth’) ableiten. Prof. Dr. Dietmar Seipel xxii Logik für Informatiker Wintersemester 2015/16 Datenbanken: S QL Falls parent als zweispaltige Relation PARENT realisiert wäre, so könnte man die Relation G RANDPARENT zu grandparent wie folgt in S QL berechnen: C REATE V IEW G RANDPARENT (NAME , G RANDPARENT ) A S S ELECT P1.NAME , P2.PARENT F ROM PARENT P1, PARENT P2 W HERE P1.PARENT = P2.NAME In der entsprechenden Regel wird die Bedingung P1.PARENT = P2.NAME durch die zweimalige Verwendung der Variablen Y ausgedrückt: grandparent(X , Z ) ← parent(X , Y ) ∧ parent(Y , Z ) Prof. Dr. Dietmar Seipel xxiii Logik für Informatiker Wintersemester 2015/16 Vergleich: Transformiert man ein S ELECT–Statement nach P ROLOG, so ergibt sich folgendes: • der S ELECT–Teil entspricht dem Regelkopf, • der F ROM–Teil entspricht den Prädikaten im Regelrumpf, • Gleicheitsbedingungen aus dem W HERE–Teil können direkt durch gleiche P ROLOG–Variablen ausgedrückt oder wie alle weiteren arithmetischen Bedingungen in den Regelrumpf übernommen werden. In P ROLOG erfolgt die Selektion nicht über Attribute, sondern über die Argumentposition. Die Relation A NCESTOR kann man in S QL im allgemeinen nicht berechnen, da man nicht weiß wieviele Stufen die zugrunde liegende Relation PARENT hat. Prof. Dr. Dietmar Seipel xxiv Logik für Informatiker 1 1.1 Wintersemester 2015/16 Aussagenlogik Grundbegriffe der Aussagenlogik atomare/elementare sprachliche Gebilde: A = „Bayern München ist deutscher Fußballmeister“ B = „Würzburg ist eine große Stadt“ C = „Würzburg hat über 300.000 Einwohner“ Man nennt diese Gebilde auch atomare Formeln oder Atome. Atome können – je nach Interpretation – wahr oder falsch sein. In der Praxis hat man oft eine Standard–Interpretation im Sinne, von der wir in der Logik aber absehen. Prof. Dr. Dietmar Seipel 1 Logik für Informatiker Wintersemester 2015/16 Wir bezeichnen alle denkbaren Atome mit Buchstaben A, B, C, . . . , oder durchnummeriert mit A1 , A2 , . . . , oder mit allgemeinen Zeichenketten (z.B. „Erkältung“), ohne ihnen eine inhaltliche Interpretation zu geben. Wir interessieren uns dafür, wie sich die Wahrheitswerte von komplexeren Formeln aus den Wahrheitswerten der atomaren Formeln zusammensetzen: F = A ∨ ¬B Baumdarstellung: A B ? ¬ U ∨ ? F Prof. Dr. Dietmar Seipel 2 Logik für Informatiker Wintersemester 2015/16 Wahrheitswerte: • 0 (falsch), • 1 (wahr) 4 mögliche Interpretationen: A B F I1 0 0 1 I2 1 0 1 I3 0 1 0 I4 1 1 1 Für jede Belegung I (Interpretation) der beteiligten Atome A und B mit Wahrheitswerten, ergibt sich der Wahrheitswert I(F ) für die Formel F . Prof. Dr. Dietmar Seipel 3 Logik für Informatiker Wintersemester 2015/16 Definition (Syntax der Aussagenlogik) Aufbau (komplexer) Formeln 1. Alle atomaren Formeln sind Formeln. Die Menge der atomaren Formeln bezeichnen wir mit A. 2. Für alle Formeln F und G sind auch • die Konjunktion (F ∧ G) und • die Disjunktion (F ∨ G) Formeln. Die Klammen kann man meist weglassen. 3. Für jede Formel F ist auch die Negation ¬F wieder eine Formel. Die Menge aller Formeln bezeichnen wir mit F. Es gilt A ⊆ F. Eine Formel F , die als Teil einer Formel G auftritt, heißt Teilformel von G. Prof. Dr. Dietmar Seipel 4 Logik für Informatiker Wintersemester 2015/16 Beispiel (Formeln, Teilformeln) • G = (A ∨ ¬B) hat die Teilformeln A, B, ¬B, G • F = ((A ∧ B) ∨ (¬A ∧ ¬B)) hat die Teilformeln A, B, ¬A, ¬B, (A ∧ B), (¬A ∧ ¬B), F Abkürzende Schreibweisen: (F1 → F2 ) für (¬F1 ∨ F2 ) (Implikation) (F1 ↔ F2 ) für ((F1 ∧ F2 ) ∨ (¬F1 ∧ ¬F2 )) (Äquivalenz) ∨n ( i=1 Fi ) für (. . . ((F1 ∨ F2 ) ∨ F3 ) ∨ . . . ∨ Fn ) ∧n ( i=1 Fi ) für (. . . ((F1 ∧ F2 ) ∧ F3 ) ∧ . . . ∧ Fn ) Prof. Dr. Dietmar Seipel 5 Logik für Informatiker Wintersemester 2015/16 Wegen der Kommutativität und der Assoziativität der Junktoren ∧ und ∨, kommt es auf die Reihenfolge und Klammerung in den folgenden Formeln nicht an: (F1 ∧ F2 ) ist gleichwertig zu (F2 ∧ F1 ), (F1 ∨ F2 ) ist gleichwertig zu (F2 ∨ F1 ), ((F1 ∧ F2 ) ∧ F3 ) ist gleichwertig zu (F1 ∧ (F2 ∧ F3 )), ((F1 ∨ F2 ) ∨ F3 ) ist gleichwertig zu (F1 ∨ (F2 ∨ F3 )). Es wird sich später zeigen, daß folgende Formeln unter jeder denkbaren Interpretation I wahr sind; man nennt sie Tautologien: ((F1 ∧ F2 ) ↔ (F2 ∧ F1 )), ((F1 ∨ F2 ) ∨ F3 ) ↔ (F1 ∨ (F2 ∨ F3 )), (¬(F1 ∧ F2 ) ↔ (¬F1 ∨ ¬F2 )). Die letzte Formel entspricht einer der beiden Regeln von De Morgan. Prof. Dr. Dietmar Seipel 6 Logik für Informatiker Wintersemester 2015/16 Die beiden arithmetischen Operatoren Multiplikation und Addition sind ebenfalls kommutativ und assoziativ, die Division allerdings nicht: 8 ÷ 4 = 2 6= 0.5 = 4 ÷ 8, (8 ÷ 4) ÷ 2 = 1 6= 4 = 8 ÷ (4 ÷ 2). Es gilt wie in der Arithmetik die Regel “Punkt vor Strich”. Dabei entspricht die Konjunktion ∧ der Multiplikation (Punkt), und die Disjunktion ∨ entspricht der Addition (Strich). Also gilt: • F1 ∧ F2 ∨ F3 entspricht (F1 ∧ F2 ) ∨ F3 . • Die andere Zusammenfassung F1 ∧ (F2 ∨ F3 ) erreicht man durch Klammerung. Prof. Dr. Dietmar Seipel 7 Logik für Informatiker Wintersemester 2015/16 Wahrheitswerte: 0,1 Boolesche Operatoren: ∧, ∨, ¬ Verknüpfungstafeln: ∧ 0 1 ∨ 0 1 0 0 0 0 0 1 1 0 1 1 1 1 ¬ 0 1 1 0 abgeleitete Verknüpungstafeln: F →G 0 1 F ↔G 0 1 0 1 1 0 1 0 1 0 1 1 0 1 vertikal F , horizontal G Prof. Dr. Dietmar Seipel 8 Logik für Informatiker Wintersemester 2015/16 Definition (Semantik der Aussagenlogik) Eine Interpretation ist eine Abbildung I : D → {0, 1}, die zunächst für eine Teilmenge D ⊆ A der atomaren Formeln definiert ist (Belegung). Sie kann wie folgt zu einer (partiellen) Abbildung I : F → {0, 1} auf der Menge F aller Formeln erweitert werden: 1. Für atomare Formeln A ∈ D ist I bereits definiert. 2. Für Konjunktionen und Disjunktionen gilt I((F ⊗ G)) = I(F ) ⊗ I(G), für ⊗ ∈ {∧, ∨} (Homomorphismus). Prof. Dr. Dietmar Seipel 9 Logik für Informatiker Wintersemester 2015/16 D.h. I((F ∧ G)) I((F ∨ G))  1, falls I(F ) = 1 und I(G) = 1 = 0, sonst  1, falls I(F ) = 1 oder I(G) = 1 = 0, sonst 3. Für eine Formel ¬F gilt I(¬F ) = ¬I(F ). D.h.  1 falls I(F ) = 0 I(¬F ) = 0, sonst Induktive Definition: „von einfachen Formeln auf komplexere Formeln gehen“ Prof. Dr. Dietmar Seipel 10 Logik für Informatiker Wintersemester 2015/16 Eine Interpretation I heißt zu einer Formel F passend, falls I für alle in F vorkommenden atomaren Formeln A definiert ist (d.h. A ∈ D). Dann ist die Erweiterung von I auch auf F definiert, d.h. I(F ) ∈ {0, 1}. Ansonsten erklären wir I auf F als undefiniert. Beispiel (Interpretationen) Zur Formel F = ¬((A ∧ B) ∨ C) sind die folgenden beiden Interpretation I und J passend: I A B C 1 0 1 J A B C D 1 0 1 1 I und J definieren alle in F vorkommenden Atome, nämlich A, B und C. J definiert sogar noch ein weiteres Atom D. Prof. Dr. Dietmar Seipel 11 Logik für Informatiker Wintersemester 2015/16 Formel: F = ¬((A ∧ B) ∨ C) Baumdarstellung: A B R ∧ R Prof. Dr. Dietmar Seipel C ∨ ? ¬ ? F 12 Logik für Informatiker Wintersemester 2015/16 Interpretation I: I A B C 1 0 1 Auswertung der Formel: I(¬ ((A ∧ B) ∨ C)) = I(A) = 1 ¬ I((A ∧ B) ∨ C) = ¬ (I(A ∧ B) ∨ I(C)) = ¬ (((I(A) ∧ I(B)) ∨ I(C)) = 0. | {z } | {z } | {z } 1 1 0 | {z } 1 | {z } 1 Prof. Dr. Dietmar Seipel R I(B) = 1 I(C) = 0 ∧ 1 R ∨ 1 ? ¬ 0 ? I(F ) = 0 13 Logik für Informatiker Wintersemester 2015/16 Boolesche Funktion Wenn man eine Formel F als boolesche Funktion f auffaßt, die zu gegebenen Wahrheitswerten ai = I(Ai ) für die in F vorkommenden Atome Ai einen Wahrheitswert berechnet, dann gilt f (a1 , . . . , an ) = I(F ). Also kann man z.B. für F = ¬ ((A1 ∧ A2 ) ∨ A3 ) schreiben: f (a1 , a2 , a3 ) = ¬ ((a1 ∧ a2 ) ∨ a3 ), f (1, 1, 0) = ¬ ((1 ∧ 1) ∨ 0) = 0. Die Interpretation I wird also zu einer Variablenbelegung (1, 1, 0): I Prof. Dr. Dietmar Seipel A1 A2 A3 1 1 0 14 Logik für Informatiker Wintersemester 2015/16 Exkurs: Auswertung in P ROLOG In der Logikprogrammierung werden auch die Rückgabewerte von Berechnungen als Parameter der zugehörigen Prädikate behandelt. Sei die Liste Assignment = [A1 =v1 ,...,An =vn ] eine Zuweisung von Wahrheitswerten vi an die atomaren Formeln Ai , d.h. eine Interpretation. Für eine atomare Formel A wird der Wahrheitswert Value mittels member(A=Value, Assignment) in Assignment nachgeschaut: evaluate_boolean_formula(Assignment, A, Value) :boolean_formula_is_atomic(A), member(A=Value, Assignment). Mittels boolean_formula_is_atomic(A) wird getestet, ob A eine atomare Formel ist, d.h. ohne Konjunktion, Disjunktion bzw. Negation. Prof. Dr. Dietmar Seipel 15 Logik für Informatiker Wintersemester 2015/16 Berechnungsbeispiel mit Trace in P ROLOG: [trace] ?- Formula = a, Assignment = [a=1, b=0], eval(Assignment, Formula, Value). Call: (8) Call: (9) Exit: (9) Call: (9) Exit: (9) Exit: (8) Value = 1. eval([a=1, b=0], a, Value) ? creep boolean_formula_is_atomic(a) ? skip boolean_formula_is_atomic(a) ? creep member(a=Value, [a=1, b=0]) ? skip member(a=1, [a=1, b=0]) ? skip eval([a=1, b=0], a, 1) ? skip evaluate_boolean_formula wurde als eval abgekürzt. Prof. Dr. Dietmar Seipel 16 Logik für Informatiker Wintersemester 2015/16 Die Konjunktion in P ROLOG /* boolean_and(U, V, W) n. • Wir setzen I(Am ) = 0, für m ≤ n, und erfüllen damit die Formeln Fm , mit 1 ≤ m ≤ n, und • wir setzen I(Am ) = 1, für m > n, und erfüllen damit die Formel F0 . Damit ist I ein Modell für M 0 . Prof. Dr. Dietmar Seipel 122 Logik für Informatiker Wintersemester 2015/16 Hier hat sogar jede echte Teilmenge M 0 ( M ein Modell. Wir setzen • I(An ) = 0, für alle n ∈ IN+ , mit Fn ∈ M 0 , und • I(An ) = 1, für alle n ∈ IN+ , mit Fn 6∈ M 0 . Dann erfüllt I alle Formeln Fn , mit n ∈ IN+ und Fn ∈ M 0 . • Falls F0 6∈ M 0 , so erfüllt I auch M 0 . • Falls F0 ∈ M 0 , so muß es wegen M 0 ( M eine Formel Fn geben, mit n ∈ IN+ und Fn 6∈ M 0 . Dann ist I(An ) = 1, und somit erfüllt I auch F0 . Also erfüllt I auch wieder M 0 . Prof. Dr. Dietmar Seipel 123 Logik für Informatiker Wintersemester 2015/16 Eine alternative Beweisidee für den Endlichkeitssatz baut auf dem Erfüllbarkeits–Algorithmus auf. Wir starten mit einem leeren Berechnungsbaum, und wir verwenden sukzessive die endlichen Klauselmengen Mn0 zur Erweiterung. • Falls irgendwann alle Äste abgestorben sind, so ist Mn0 unerfüllbar. • Andernfalls bleibt immer mindestens ein Ast am Leben. Wir können dann wie folgt einen Ast finden, der nicht abstirbt: • Wir starten in der Wurzel des Berechnungsbaums. • Wir folgen einem Ast, dessen Teilbaum nicht komplett abstirbt. Auf diese Weise finden wir eine Menge I von Atomen, so daß die zugehörige Interpretation I 0 ein Modell für M ist. Prof. Dr. Dietmar Seipel 124 Logik für Informatiker Wintersemester 2015/16 1.6 Resolution Ein Klausel K ist eine Disjunktion von Literalen: K = L1 ∨ . . . ∨ Ln . Die Reihenfolge der Literale in K ist unerheblich; wir können K auch als Menge { L1 , . . . , Ln } von Literalen ansehen. Deswegen schreiben wir Li ∈ K, für 1 ≤ i ≤ n, und wir bezeichnen mit K\Li = L1 ∨ . . . ∨ Li−1 ∨ Li+1 ∨ . . . ∨ Ln die Klausel, welche man aus K durch Weglassen von Li erhält. Eine endliche Klauselmenge M entspricht einer Formel F in KNF: F = (L1,1 ∨ . . . ∨ L1,n1 ) ∧ . . . ∧ (Lm,1 ∨ . . . ∨ Lm,nm ). Prof. Dr. Dietmar Seipel 125 Logik für Informatiker Wintersemester 2015/16 Definition (Resolvente) Seien K1 und K2 Klauseln mit A ∈ K1 und ¬A ∈ K2 , für ein Atom A. Dann heißt K = (K1 \A) ∨ (K2 \¬A) eine Resolvente von K1 und K2 nach A. K1 K2 U  K Spezialfall Für K1 = A ∨ K und K2 = ¬A ∨ K erhalten wir die Resolvente (K1 \A) ∨ (K2 \¬A) = K ∨ K = K. Prof. Dr. Dietmar Seipel 126 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolvente) Für die beiden Klauseln K1 = A ∨ B ∨ C, K2 = ¬A ∨ B ∨ ¬D gilt K1 \ A = B∨C A∨B∨C ¬A ∨ B ∨ ¬D R B ∨ C ∨ ¬D K2 \ ¬A = B ∨ ¬D, und wir erhalten die Resolvente K = B ∨ C ∨ ¬D. Nur wenn eine Klausel K ein Atom A und dessen Negation ¬A enthält (z.B. K = A ∨ B ∨ ¬A), dann kann man sie mit sich selbst resolvieren: K1 = K2 = K. Dann ist K eine Tautologie, und die Resolvente ist wieder K. Prof. Dr. Dietmar Seipel 127 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolvente) Die beiden möglichen Resolventen aus K1 = A ∨ ¬B ∨ C und K2 = B ∨ ¬C sind Tautologien: A ∨ ¬B ∨ C B ∨ ¬C R A ∨ C ∨ ¬C A ∨ ¬B ∨ C B ∨ ¬C R A ∨ ¬B ∨ B ¬A A R 2 Wir bezeichnen hier die leere Disjunktion 2D kurz mit 2. Prof. Dr. Dietmar Seipel 128 Logik für Informatiker Wintersemester 2015/16 Resolutionslemma Sei M ein Klauselmenge und K1 , K2 ∈ M . Ist K eine Resolvente von K1 und K2 (nach einem Atom A), so sind M und M ∪ {K} äquivalent: M ≡ M ∪ {K}. Beweis: Sei I eine zu M – und damit auch zu M ∪ {K} – passende Interpretation. Falls I |= M ∪ {K}, dann gilt natürlich auch I |= M . Also nehmen wir nun I |= M an. Sei K1 = A ∨ K10 und K2 = ¬A ∨ K20 . Dann gilt K = K10 ∨ K20 . • Falls I |= A, so folgt aus I |= K2 auch I |= K20 . • Falls I |= ¬A, so folgt aus I |= K1 auch I |= K10 . Also gilt in beiden Fällen I |= K10 ∨ K20 = K. Deshalb gilt I |= M ∪ {K}. Prof. Dr. Dietmar Seipel 129 Logik für Informatiker Wintersemester 2015/16 Definition (Resolutionsmengen) Sei M eine Klauselmenge. Res(M ) = M ∪ { K | K ist eine Resolvente zweier Klauseln K1 , K2 ∈ M }. Ferner definieren wir: Res 0 (M ) = M, Res n+1 (M ) = Res(Res n (M )), für n ≥ 0, ∪ ∗ Res (M ) = n≥0 Res n (M ). Offensichtlich gilt die sogenannte Monotonie–Eigenschaft: M ⊆ M 0 ⇒ Res(M ) ⊆ Res(M 0 ). Prof. Dr. Dietmar Seipel 130 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolutionsmengen) Für die Klauselmenge M = { c ∨ ¬a, a ∨ b, c1 ∨ c2 ∨ ¬a, d ∨ ¬b } erhalten wir die folgenden Resolutionsmengen: Res 0 (M ) = M, Res 1 (M ) = M ∪ { b ∨ c, b ∨ c1 ∨ c2 , a ∨ d }, Res 2 (M ) = Res 1 (M ) ∪ { c ∨ d, c1 ∨ c2 ∨ d }, Res 3 (M ) = Res 2 (M ). 1. Iteration: • Aus c ∨ ¬a und a ∨ b erhalten wir b ∨ c. • Aus a ∨ b und c1 ∨ c2 ∨ ¬a erhalten wir b ∨ c1 ∨ c2 . • Aus a ∨ b und d ∨ ¬b erhalten wir a ∨ d. Prof. Dr. Dietmar Seipel 131 Logik für Informatiker Wintersemester 2015/16 c ∨ d kann redundant auf zwei unterschiedlichen Wegen abgeleitet werden: c ∨ ¬a U  b∨c a∨b d ∨ ¬b U  c∨d a∨b c ∨ ¬a d ∨ ¬b U  a∨d U  c∨d In diesem Fall sind die verwendeten Klauseln aus M (an den Blättern des Baumes) jeweils dieselben. Nur die inneren Knoten der Bäume sind anders. Prof. Dr. Dietmar Seipel 132 Logik für Informatiker Wintersemester 2015/16 2. Iteration: • Aus c ∨ ¬a und a ∨ d erhalten wir c ∨ d. • Aus c1 ∨ c2 ∨ ¬a und a ∨ d erhalten wir c1 ∨ c2 ∨ d. • Aus d ∨ ¬b und b ∨ c erhalten wir ebenfalls c ∨ d. • Aus d ∨ ¬b und b ∨ c1 ∨ c2 erhalten wir ebenfalls c1 ∨ c2 ∨ d. Sowohl c ∨ d als auch c1 ∨ c2 ∨ d werden also redundant auf zwei unterschiedlichen Wegen abgeleitet. In der Praxis versucht man redundante Ableitungen möglichst zu vermeiden. Prof. Dr. Dietmar Seipel 133 Logik für Informatiker Wintersemester 2015/16 Für die Klauselmenge M = { p ∨ q, ¬p ∨ ¬q, p ∨ ¬q, ¬p ∨ q } erhalten wir die folgenden Resolutionsmengen: Res 0 (M ) = M, Res 1 (M ) = M ∪ { p, q, ¬p, ¬q, p ∨ ¬p, q ∨ ¬q }, Res 2 (M ) = Res 1 (M ) ∪ { 2 }, Res 3 (M ) = Res 2 (M ). Aus ¬p ∨ ¬q und p ∨ ¬q erhalten wir z.B. die Resolvente ¬q. In Iteration 2 kann die leere Klausel 2 kann auf zwei unterschiedlichen Wegen abgeleitet werden: • aus p und ¬p und • aus q und ¬q. Prof. Dr. Dietmar Seipel 134 Logik für Informatiker Wintersemester 2015/16 Man kann zeigen: M = Res 0 (M ) ⊆ Res 1 (M ) ⊆ . . . ⊆ Res n (M ) ⊆ Res ∗ (M ). Außerdem gilt: M ≡ Res n (M ) ≡ Res ∗ (M ), für alle n ∈ IN0 , und wegen Res 0 (M ) ⊆ Res 1 (M ) auch ∪ ∪ ∗ n Res (Res(M )) = n≥1 Res (M ) = n≥0 Res n (M ) = Res ∗ (M ). Resolutionssatz der Aussagenlogik (Widerlegungsvollständigkeit) Eine Klauselmenge M ist genau dann unerfüllbar, wenn 2 ∈ Res ∗ (M ). Beweis: Korrektheit: Angenommen 2 ∈ Res ∗ (M ). Dann ist Res ∗ (M ) unerfüllbar, und wegen M ≡ Res ∗ (M ) ist auch M unerfüllbar. Prof. Dr. Dietmar Seipel 135 Logik für Informatiker Wintersemester 2015/16 Vollständigkeit: Angenommen M ist unerfüllbar. Aufgrund des Endlichkeitstatzes gibt es bereits eine endliche Teilmenge M 0 ⊆ M , welche unerfüllbar ist. Wir können zusätzlich voraussetzen, daß M 0 keine Tautologien der Form A ∨ ¬A ∨ C enthält. Seien A1 , . . . , An alle in M 0 vorkommenden Atome. Wir zeigen nun per Induktion nach n, daß 2 ∈ Res ∗ (M ). n = 0: Da M 0 = ∅ erfüllbar ist, gilt M 0 = {2} und somit 2 ∈ M 0 ⊆ Res ∗ (M 0 ) ⊆ Res ∗ (M ). n → n + 1: Wir resolvieren Klauselpaare K1 ∨ An+1 und K2 ∨ ¬An+1 aus M 0 nach An+1 und setzen: M1 = { K1 | K1 ∨ An+1 ∈ M 0 }, M2 = { K2 | K2 ∨ ¬An+1 ∈ M 0 }. Prof. Dr. Dietmar Seipel 136 Logik für Informatiker Wintersemester 2015/16 Sei ferner M3 = { K3 ∈ M 0 | An+1 kommt nicht in K3 vor } die Menge aller Klauseln aus M 0 , in denen An+1 werder positiv als An+1 noch negativ als ¬An+1 vorkommt. Dann gilt M 00 = (M1 ∨ M2 ) ∪ M3 ⊆ Res(M 0 ), wobei M1 ∨ M2 = { K1 ∨ K2 | K1 ∈ M1 , K2 ∈ M2 }. Die Menge M 00 enthält nur Formeln über A1 , . . . , An . Angenommen M 00 ist erfüllbar mit einem Modell I. • Angenommen I 6|= M1 und I 6|= M2 . Dann gibt es K1 ∈ M1 und K2 ∈ M2 mit I 6|= K1 und I 6|= K2 , und somit I 6|= K1 ∨ K2 ∈ M1 ∨ M2 ⊆ M 00 , ein Widerspruch. • Also gilt I |= M1 oder I |= M2 (oder beides). Prof. Dr. Dietmar Seipel 137 Logik für Informatiker Wintersemester 2015/16 Wir zeigen: wenn M 0 unerfüllbar ist, dann ist auch M 00 unerfüllbar. M0 ≡ M M1 ? R M2 M3 N ? M = (M1 ∨ M2 ) ∪ M3 ⊆ Res(M 0 ) 00 M 0 = ({An+1 } ∨ M1 ) ∪ ({¬An+1 } ∨ M2 ) ∪ M3 Wenn M 0 die Atome A1 , . . . , An+1 enthält, dann kann M 00 nur noch die Atome A1 , . . . , An enthalten. Prof. Dr. Dietmar Seipel 138 Logik für Informatiker Wintersemester 2015/16 Wir konstruieren nun ein Modell I 0 für M 0 : M 0 = ({An+1 } ∨ M1 ) ∪ ({¬An+1 } ∨ M2 ) ∪ M3 . 1. Falls I |= M1 , so setzen wir:  I(B), falls B ∈ {A , . . . A } 1 n I 0 (B) = 0, falls B = An+1 • Wegen I |= M1 gilt I 0 |= {An+1 } ∨ M1 . • Wegen I 0 |= ¬An+1 gilt auch I 0 |= {¬An+1 } ∨ M2 . 2. Falls I |= M2 , so setzen wir:  I(B), falls B ∈ {A , . . . , A } 1 n I 0 (B) = 1, falls B = An+1 • Wegen I |= An+1 gilt I 0 |= {An+1 } ∨ M1 . • Wegen I 0 |= M2 gilt auch I 0 |= {¬An+1 } ∨ M2 . In beiden Fällen gilt wegen I |= M3 auch I 0 |= M3 . Prof. Dr. Dietmar Seipel 139 Logik für Informatiker Wintersemester 2015/16 Also gilt in beiden Fällen I 0 |= M 0 , im Widerspruch zu der Annahme, daß M 0 unerfüllbar ist. Also haben wir gezeigt, daß M 00 unerfüllbar ist. Da M 00 nur noch die n Atome A1 , . . . , An enthalten kann, gilt somit nach Induktionsannahme 2 ∈ Res ∗ (M 00 ). Wegen Res ∗ (M 00 ) ⊆ Res ∗ (Res(M 0 )) = Res ∗ (M 0 ) ⊆ Res ∗ (M ), gilt nun also 2 ∈ Res ∗ (M ). Prof. Dr. Dietmar Seipel 140 Logik für Informatiker Wintersemester 2015/16 Die Konstruktion aus dem Beweis zum Resolutionssatz funktioniert für beliebige Klauselmengen M und Atome A: M1 = { K1 | K1 ∨ A ∈ M }, M2 = { K2 | K2 ∨ ¬A ∈ M }, M3 = { K3 ∈ M | A kommt nicht in K3 vor }. Die Transformation M 7→ M 00 = (M1 ∨ M2 ) ∪ M3 erhält die Widerlegungseingenschaften: M ist unerfüllbar ⇔ 2 ∈ Res ∗ (M ) ⇔ M 00 ist unerfüllbar ⇔ 2 ∈ Res ∗ (M 00 ) M 00 enthält das Atom A nicht mehr. Prof. Dr. Dietmar Seipel 141 Logik für Informatiker Wintersemester 2015/16 Beispiel (Transformation) Aus der Klauselmenge M = { p ∨ q, ¬p ∨ ¬q, p ∨ ¬q, ¬p ∨ q } erhalten wir für das Atom A = p: M1 = { q, ¬q } = M2 , M3 = ∅, M 00 = M1 ∨ M2 = { q ∨ ¬q, q, ¬q } ≡ { q, ¬q }. Tautologien – wie q ∨ ¬q – kann man frühzeitig aus der weiteren Betrachtung ausschließen. Die nochmalige Transformation für das Atom A = q erzeugt aus M 00 nun M 0000 = { 2 }. Also ist M unerfüllbar. Prof. Dr. Dietmar Seipel 142 Logik für Informatiker Wintersemester 2015/16 Definition (Deduktion) Eine Deduktion (Herleitung, Beweis) einer Klausel K aus einer Klauselmenge M ist eine Folge K1 , K2 , . . . , Km von Klauseln, mit Km = K, und ∀ 1 ≤ i ≤ m: • Ki ∈ M oder • Ki ist die Resolvente aus zwei Klauseln Ki1 und Ki2 , mit 1 ≤ i1 ≤ i2 ≤ i − 1. Eine Klauselmenge M ist genau dann unerfüllbar, wenn eine Deduktion der leeren Klausel K = 2 aus M existiert. Prof. Dr. Dietmar Seipel 143 Logik für Informatiker Wintersemester 2015/16 Beispiel (Deduktion) Für die Klauselmenge M = { c ∨ ¬a, a ∨ b, c1 ∨ c2 ∨ ¬a, d ∨ ¬b } erhalten wir z.B. die folgende Deduktion K1 , . . . , K5 von K = c ∨ d: K1 = c ∨ ¬a K2 = a ∨ b U  K3 = b ∨ c K4 = d ∨ ¬b U  K5 = c ∨ d Prof. Dr. Dietmar Seipel 144 Logik für Informatiker Wintersemester 2015/16 Beispiel (Deduktion) M = { p ∨ q, ¬p ∨ ¬q, p ∨ ¬q, ¬p ∨ q }. Deduktion: K1 = p ∨ q, Resolutionsgraph: K1 K2 K4 K5 K2 = p ∨ ¬q, K3 = p, K4 = ¬p ∨ ¬q, N K3 N K6 K5 = ¬p ∨ q, K6 = ¬p, K7 = 2. Prof. Dr. Dietmar Seipel R K7 = 2 145 Logik für Informatiker Wintersemester 2015/16 Definition (Lineare Deduktion) Eine lineare Deduktion (Herleitung, Beweis) einer Klausel K aus einer Klauselmenge M ist eine Folge K1 , K2 , . . . , K2·m+1 ungerader Länge von Klauseln, mit K2·m+1 = K und • K1 ∈ M und • ∀ 1 ≤ i ≤ m: K2·i+1 ist eine Resolvente aus K2·i−1 und einer Klausel K2·i ∈ M . K1 und die Klauseln K2·i mit geradem Index sind also alle in M , die anderen Klauseln K2·i+1 mit ungeradem Index sind Resolventen. Prof. Dr. Dietmar Seipel 146 Logik für Informatiker Wintersemester 2015/16 K1 ∈ M K2 ∈ M ? K3 ? K2·i−1 K2·i ∈ M ? K2·i+1 ? K2·m−1 K2·m ∈ M ? K2·m+1 Prof. Dr. Dietmar Seipel 147 Logik für Informatiker Wintersemester 2015/16 Beispiel (Lineare Deduktion) 1. Für die Horn–Klauselmenge M = { c ∨ ¬a, a ∨ b, c1 ∨ c2 ∨ ¬a, d ∨ ¬b } haben wir bereits eine lineare Deduktion K1 , . . . , K5 von K = c ∨ d gesehen. 2. Man kann zeigen, daß es für die Nicht–Horn–Klauselmenge M = { p ∨ q, ¬p ∨ ¬q, p ∨ ¬q, ¬p ∨ q } keine lineare Deduktion der leeren Klausel K = 2 gibt. Die oben angegebene Deduktion von K = 2 war nicht linear. Prof. Dr. Dietmar Seipel 148 Logik für Informatiker Wintersemester 2015/16 Aus dem Erfüllbarkeitstest für Horn–Klauselmengen folgt: Für alle unerfüllbaren Horn–Klauselmengen M gibt es eine lineare Deduktion K1 , K2 , . . . , K2·m+1 der leeren Klausel K = 2, die mit einer Integritätsbedingung K1 ∈ M beginnt. Für diese Deduktion gilt dann: • Auch alle anderen Klauseln K2·i+1 mit ungeradem Index sind Integritätsbedingungen. • Alle Klauseln K2·i mit geradem Index sind Regeln (einschließlich der Fakten) aus M mit einem positiven Atom, dem Kopfatom. Auch die leere Klausel K = 2 kann man als Integritätsbedingung ansehen, da sie keine positiven Atome enthält. Prof. Dr. Dietmar Seipel 149 Logik für Informatiker Wintersemester 2015/16 Beispiel (Lineare Deduktion) Für die unerfüllbare Horn–Klauselmenge M = { a, b, ¬a ∨ ¬b } gibt es z.B. die folgende lineare Deduktion von K = 2: K1 = ¬a ∨ ¬b K2 = a ? K3 = ¬b K4 = b ? K5 = 2 Prof. Dr. Dietmar Seipel 150 Logik für Informatiker 2 Wintersemester 2015/16 Prädikatenlogik In der Prädikatenlogik kann man die in der Aussagenlogik bereits betrachteten atomaren Aussagen eleganter formulieren: A = „Bayern München ist deutscher Fußballmeister“: deutscher _fussballmeister (’Bayern Muenchen’, 2013 ). B = „eine Stadt mit mindestens 100000 Einwohnern ist groß“: grosse_stadt(Stadt) ← einwohner (Stadt, X ) ∧ X ≥ 100000 . C = „Würzburg hat über 300.000 Einwohner“: einwohner (’Wuerzburg’, 300000 ). Dann kann man generische Aussagen machen. Z.B. ist die Formel zu B auf alle Städte mit mindestens 100000 Einwohnern anwendbar. Prof. Dr. Dietmar Seipel 151 Logik für Informatiker 2.1 Wintersemester 2015/16 Grundbegriffe der Prädikatenlogik Erweiterung der Aussagenlogik um Variablen– } Funktions– U, V, W, X, Y, Z Symbole Prädikaten– f, g, h a, b, c p, q, r und Quantoren: • Existenzquantor: ∃, • Allquantor: ∀. Die bekannten Junktoren ∧, ∨, ¬ und → sind weiterhin erlaubt. Wir nehmen im Folgenden meist an, daß Variablensymbole mit Großbuchstaben beginnen, und daß Funktions– und Prädikatensymbole mit Kleinbuchstaben beginnen oder in Hochkommata eingeschlossen sind. Prof. Dr. Dietmar Seipel 152 Logik für Informatiker Wintersemester 2015/16 Beispiel (Prädikatenlogiche Formeln) 1. Konvergenz, Grenzwert: limn→∞ f (n) = a ist in der Analysis definiert als ∀  > 0 ∃ n0 ∀ n ≥ n0 |f (n) − a| < . Hier sind – ausnahmsweise – , n0 und n Variablensymbole (nur über diese kann man quantifizieren), 0, a, f , − und || sind Funktionssymbole, und >, ≥ und < sind Prädikatensymbole. Funktionssymbole ohne Argumente – wie 0 und a – nennt man auch Konstantensymbole; ihre Stelligkeit ist 0. f und || sind 1–stellig, − ist 2–stellig. Hier sind auch alle Prädikatensymbole 2–stellig. Für f (n) = 1/n gilt z.B. limn→∞ f (n) = limn→∞ 1/n = 0 = a. Für jede vorgegebene reelle Zahl  > 0 existiert ein n0 ∈ IN , etwa n0 = d1/e + 1, so daß für alle n ≥ n0 gilt |1/n − 0| < . Prof. Dr. Dietmar Seipel 153 Logik für Informatiker Wintersemester 2015/16 2. Konjunktion: (∃ Jahr weltmeister (brasilien, Jahr )) ∧ (∀ Jahr ¬weltmeister (nigeria, Jahr )) • Brasilien war bereits Fußballweltmeister, d.h.: es gibt ein Jahr, in dem Brasilien Fußballweltmeister war; • Nigeria aber noch nicht. 3. Implikation: ∀ Stadt ∀X ( grosse_stadt(Stadt) ← einwohner (Stadt, X ) ∧ X ≥ 100000 ) ist äquivalent zu ∀ Stadt ( grosse_stadt(Stadt) ← ∃X ( einwohner (Stadt, X ) ∧ X ≥ 100000 ) ) Prof. Dr. Dietmar Seipel 154 Logik für Informatiker Wintersemester 2015/16 4. Die unendliche Formelmenge M = { Fn | n ∈ IN0 } aus Kapitel 1 mit ∨∞ F0 = A1 ∨ A2 ∨ . . . = n=1 An , Fn = ¬An , für n ∈ IN+ , mit der unendlichen – in der Aussagenlogik eigentlich nicht erlaubten – Disjunktion F0 kann man für An = p(n) in der Prädikatenlogik als eine Formel G1 ∧ G2 ausdrücken mit G1 = ∃n ∈ IN+ p(n), G2 = ∀n ∈ IN+ ¬p(n). Auch hier ist – ausnahmsweise – n wieder ein Variablensymbol. Die unendliche Formelmenge M 0 = { G1 } ∪ { ¬p(n) | n ∈ IN+ } zeigt, daß der Kompaktheitssatz in der Prädikatenlogik nicht gilt. Prof. Dr. Dietmar Seipel 155 Logik für Informatiker Wintersemester 2015/16 Syntax Wir setzen folgende abzählbaren Mengen voraus: • Variablensymbole: V = { X1 , X2 , . . . }, • Funktionssymbole: F = { f1 , f2 , . . . }, • Prädikatensymbole: P = { p1 , p2 , . . . }. Jedes Funktions– bzw. Prädikatensymbol hat eine Stelligkeit k ∈ IN0 . Schöningh schreibt fik , pki , wir schreiben fi /k, pi /k. Allerdings kann dasselbe Funktions– bzw. Prädikatensymbol in einer Formel mit unterschiedlichen Stelligkeiten auftreten. In f (f (a), f (a, a, a)) ist das erste Auftreten von f zweistellig, das zweite einstellig, und das dritte dreistellig. Eigentlich handelt es sich dabei um unterschiediche Funktionssymbole f /2, f /1 und f /3 mit demselben Namen f . Prof. Dr. Dietmar Seipel 156 Logik für Informatiker Wintersemester 2015/16 Induktive Definitionen Terme 1. Jedes Variablensymbol X ∈ V ist ein Term. 2. Ist f ein Funktionssymbol der Stelligkeit k, und sind t1 , . . . , tk (ebenso viele) Terme, so ist auch f (t1 , . . . , tk ) ein Term. 3. Ist k = 0, so schreibt man kurz f ausstelle von f (), und man nennt f dann eine Konstante. Beispiel (Terme) • f1 (X2 ), • f3 (f2 , f1 (X3 )). Stelligkeiten: Prof. Dr. Dietmar Seipel f1 f2 f3 1 0 2 157 Logik für Informatiker Wintersemester 2015/16 Formeln 1. Für ein k–stelliges Prädikatensymbol p und Terme t1 , . . . tk ist p(t1 , . . . , tk ) eine atomare Formel. Falls k = 0 ist, so schreiben wir kurz p anstelle von p(). 2. Für jede Formel F ist auch ¬F eine Formel. 3. Sind F1 und F2 Formeln, so auch (F1 ∧ F2 ) und (F1 ∨ F2 ). 4. Falls X ein Variablensymbol ist und F eine Formel, so sind auch ∃X F und ∀X F Formeln. Man kann wieder redundante Klammerpaare weglassen, und Teilformeln werden analog zur Aussagenlogik definiert. Man könnte weitere Formeln mittels anderer Junktoren bilden, z.B. die Implikation F1 → F2 . Andererseits könnte man diese Formel auch wie ¬F1 ∨ F2 auffassen. Prof. Dr. Dietmar Seipel 158 Logik für Informatiker Wintersemester 2015/16 Beispiel (Formeln) 1. In der Formel F = (∃X1 p1 (X1 , f1 (X2 ))) ∨ (∀X2 p2 (X2 , f3 (f2 , f1 (X3 )))) haben die Prädikatensymbole die folgenden Stelligkeiten: p1 p2 2 2 2. Man kann auch über Variablensymbole quantifizieren, die nicht in der betroffenen Formel vorkommen: F = ∀X p(Y ). 3. In der folgenden Implikation bezeichnen die beiden Vorkommen von X dasselbe: F = ∀X ( student(X) → person(X) ). 4. In F = ∀X ( p(X ) → ∃X q(X) ) bezieht sich die Allquantifizierung ∀X auf p(X), die Existenzquantifizierung ∃X auf q(X). Es gibt keinen Zusammenhang zwischen den beiden Vorkommen von X. Prof. Dr. Dietmar Seipel 159 Logik für Informatiker Wintersemester 2015/16 Klammerungsregeln 1. Wir nehmen an, daß die Quantoren am stärksten binden. D.h. QX F ⊗ G bedeutet (QX F ) ⊗ G, für einen Quantor Q ∈ { ∀, ∃ } und einen Junktor ⊗ ∈ { ∧, ∨, → }. Z.B. bedeutet ∀X ∀ Y ( ∃Z (p(X, Z) ∧ p(Z, Y )) → p(X, Y ) ) dasselbe wie ∀X ∀ Y ( (∃Z (p(X, Z) ∧ p(Z, Y ))) → p(X, Y ) ) 2. Wir nehmen an, daß die Negation stärker bindet als die Konjunktion, die Disjunktion und die Implikation, und wir nehmen an, daß die Konjunktion stärker bindet als die Disjunktion (Punkt vor Strich) und die Implikation, und die Disjunktion stärker als die Implikation. D.h. F ∨ ¬ G ∧ G0 → H bedeutet (F ∨ ((¬ G) ∧ G0 )) → H. Prof. Dr. Dietmar Seipel 160 Logik für Informatiker Wintersemester 2015/16 Schreibweisen Die Formel ∀  > 0 ∃ n0 ∀ n ≥ n0 |f (n) − a| <  müßte man eigentlich ausführlicher wie folgt schreiben: ∀ (  ∈ IR ∧  > 0 → ∃n0 ( n0 ∈ IN ∧ ∀n ( n ∈ IN ∧ n ≥ n0 → |f (n) − a| <  ) ) ). In der Kurzschreibweise wurde implizit angenommen, daß  eine reelle Zahl ist, und daß n und n0 natürliche Zahlen sind. Daneben wurde die vereinfachende Infix– bzw. Zirkumfix–Notation für Funktions– und Prädikatensymbole verwendet. Manchmal schreibt man anstelle von ∀X F auch ∀X : F ; analog für ∃. Prof. Dr. Dietmar Seipel 161 Logik für Informatiker Wintersemester 2015/16 Infix– und Zirkumfix–Notation Zur leichteren Lesbarkeit kann man gewisse binäre Funktions– und Prädikatensymbole in Infix–Notation schreiben. Anstelle der Präfix–Notation (t1 , t2 ) schreiben wir dann die Infix–Notation t1 t2 . Die atomare Formel |f (n) − a| <  mit dem binären Prädikatensymbol < und dem binären Funktionssymbol − würde in Präfix–Notation wie folgt aussehen: < ( || (−(f (n), a)),  ) Einen Term ||(t) mit dem unären Funktionssymbol || (Betrag) können wir in Zirkumfix–Notation |t| schreiben. Prof. Dr. Dietmar Seipel 162 Logik für Informatiker Wintersemester 2015/16 Freie und gebundene Variablen 1. Ein Vorkommen einer Variable X in einer Formel F heißt gebunden, falls X quantifiziert in einer Teilformel von F der Form ∃X G oder ∀X G vorkommt (d.h. im Geltungsbereich eines Quantors über X). 2. Andernfalls heißt das Vorkommen von X frei. 3. Eine Formel F ohne Vorkommen von freien Variablen heißt geschlossen, oder eine Aussage. Andernfalls heißt F offen. Beispiel: Die folgende Formel F ist offen: F = (∃X1 p1 (X1 , f1 (X2 ))) ∨ (∀X2 p2 (X2 , f3 (f2 , f1 (X3 )))). • Die beiden unterstrichenen Vorkommen der Variablen X1 und X2 sind gebunden. Alle anderen Vorkommen sind frei. • Das (einzige) Vorkommen von X3 ist frei. Prof. Dr. Dietmar Seipel 163 Logik für Informatiker Wintersemester 2015/16 Definition (Semantik der Prädikantenlogik) Eine Struktur ist ein Paar A = (UA , IA ) mit 1. UA ist eine beliebige, nicht–leere Menge, genannt Grundmenge von A, Grundbereich, Individuenbereich, Universum. 2. IA ist eine partielle Abbildung auf V ∪ F ∪ P mit • jedem k–stelligen Prädikantensymbol p ∈ P ∩ def (IA ) ist ein k–stelliges Prädikat IA (p) über UA zugeordnet, d.h. eine Relation k . IA (p) ⊆ UA • jedem k–stelligen Funktionssymbol f ∈ F ∩ def (IA ) ist eine k k–stellige Funktion IA (f ) : UA → UA zugeordnet. • jedem Variablensymbol X ∈ V ∩ def (IA ) ist ein Individuum IA (X) ∈ UA zugeordnet. k die Menge aller k–Tupel mit Komponenten aus UA . Dabei ist UA Prof. Dr. Dietmar Seipel 164 Logik für Informatiker Wintersemester 2015/16 Der Definitionsbereich def (IA ) der partiellen Abbildung IA ist meist eine echte Teilmenge von V ∪ F ∪ P: def (IA ) ⊆ V ∪ F ∪ P. Die Struktur A paßt zu einer Formel F , falls IA für alle in F vorkommenden Prädikaten–, Funktions– und Variablensymbole für freie Variablen definiert ist. Abkürzung: IA (α) = αA , für alle α ∈ V ∪ F ∪ P. Falls α außerhalb des Definitionsbereichs def (IA ) liegt, so ist αA undefiniert. Prof. Dr. Dietmar Seipel 165 Logik für Informatiker Wintersemester 2015/16 Beispiel (Struktur) Die folgende Struktur A paßt zur Formel F = ∀X p(X, f (X)) ∧ q(g(a, Z)). Die Grundmenge von A und die Interpretation der Prädikaten– und Funktionssymbole seien wie folgt: UA = IN0 = { 0, 1, 2, . . . }, pA = { (m, n) ∈ IN02 | m < n }, qA = { (n) ∈ IN01 | n ist eine Primzahl }, f A (n) = n + 1, d.h. f A ist die Nachfolgerfunktion auf IN0 , g A (n, m) = n + m, d.h. g A ist die Additionsfunktion auf IN0 . Das 0–stellige Funktionssymbol a werde als aA = 2 interpretiert, und die Variablensymbole als X A = 23, Z A = 3. Prof. Dr. Dietmar Seipel 166 Logik für Informatiker Wintersemester 2015/16 In dieser Struktur A gilt F offensichtlich (die entsprechenden Definitionen der Semantik folgen noch), denn • die Nachfolgerfunktion f A paßt zur Kleiner–Relation pA : p(X, f (X)) entspricht in A dem Vergleich X < X + 1; und • g A (aA , Z A ) = 2 + 3 = 5 ist in der Primzahl–Relation q A . Ändert man dagegen q A zu q A0 = { (n) ∈ IN01 | n ist eine gerade Zahl }, und läßt den Rest unverändert, so gilt F in der veränderten Struktur A0 nicht, da 5 keine gerade Zahl ist. Wenn man eine fest vorgegebene Interpretation eines Funktions– oder Prädikatensymbols betrachten will, dann muß man diese durch Hinzunahme geeigneter Axiome zu F erzwingen. Prof. Dr. Dietmar Seipel 167 Logik für Informatiker Wintersemester 2015/16 Definition (Semantik der Prädikatenlogik) Wir betrachten im folgenden Formeln F und zu F passende Strukturen A. Der Wert A(t) eines Terms t wird induktiv definiert als: 1. A(t) = tA , falls t ∈ V eine Variable ist. 2. A(t) = f A (A(t1 ), . . . , A(tk )), falls t = f (t1 , . . . , tk ) ein komplexer Term ist. Eine Herbrand–Struktur bildet alle Terme auf sich selbst ab. Für X ∈ V und u ∈ UA sei A[X|u] diejenige Struktur B, welche man aus A erhält, indem man X A auf X B = u ändert und A ansonsten unverändert läßt: • für alle α ∈ P ∪ F ∪ V \ {X} gilt αB = αA , • X B = u (unabhängig von X A ). Prof. Dr. Dietmar Seipel 168 Logik für Informatiker Wintersemester 2015/16 Der Wahrheitswert A(F ) wird dann ebenfalls induktiv definiert:   1, falls (A(t ), . . . , A(t )) ∈ pA 1 k A(p(t1 , . . . , tk )) =  0, sonst A(¬G) = ¬A(G), A(F1 ∧ F2 ) = A(F1 ) ∧ A(F2 ), A(F1 ∨ F2 ) = A(F1 ) ∨ A(F2 ),   1, falls für alle u ∈ U gilt A A [X|u] (G) = 1 =  0, sonst   1, falls es ein u ∈ U gibt mit A A [X|u] (G) = 1, =  0, sonst A(∀XG) A(∃XG) Damit gilt offensichtlich auch A(F → G) = A(F ) → A(G). Prof. Dr. Dietmar Seipel 169 Logik für Informatiker Wintersemester 2015/16 Die Definitionen für die booleschen Junktoren sind exakt analog zur Aussagenlogik. Die Fallunterscheidungen könnte man wie folgt abkürzen: A(p(t1 , . . . , tk )) = (A(t1 ), . . . , A(tk )) ∈ pA , A(∀XG) = ∧u∈UA A[X|u] (G), A(∃XG) = ∨u∈UA A[X|u] (G). 1. Ersteres gilt, da der Test e ∈ M auf Elementschaft in einer Menge einen der Wahrheitswerte 1 oder 0 als Resultat hat. 2. Die – potentiell unendliche – Konjunktion im zweiten Teil ist genau dann 1, wenn für alle u ∈ UA gilt A[X|u] (G) = 1. 3. Die – potentiell unendliche – Disjunktion im dritten Teil ist genau dann 1, wenn es (mindestens) ein u ∈ UA gibt mit A[X|u] (G) = 1. Prof. Dr. Dietmar Seipel 170 Logik für Informatiker Wintersemester 2015/16 Die Prädikatenlogik verallgemeinert die Aussagenlogik. Die atomaren Formeln p der Aussagenlogik entsprechen 0–stelligen Prädikatensymbolen. Es gibt es nur zwei mögliche Relationen pA ⊆ UA0 = {( )} : • Falls pA = {( )} nur das 0–stellige Tupel ( ) enthält, so ist A(p) = 1. • Falls pA = {} leer ist, so ist A(p) = 0. In der Aussagenlogik gibt es keine höherstelligen Prädikatensymbole, und deswegen braucht man auch keine Variablen– bzw. Funktionssymbole um Terme zu bilden. Auch die Quantifizierung ist in der Aussagenlogik sinnlos, da es dort keine Variablensymbole gibt. Prof. Dr. Dietmar Seipel 171 Logik für Informatiker Wintersemester 2015/16 Definition (Modelle) 1. Eine Struktur A erfüllt eine Formel F , falls A zu F paßt und A(F ) = 1 ist. 2. Dann sagen wir auch, daß die Formel F in A gilt. 3. Dann ist A ein Modell von F , und wir schreiben auch A |= F . Herbrand–Strukturen In der Praxis arbeitet man meist mit geschlossenen Formeln F und Herbrand–Strukturen A = (UA , IA ) : 1. Ihre Grundmenge UA besteht aus den Termen über den Funktionssymbolen von F . Terme werden nicht interpretiert. 2. Herbrand–Strukturen können also alleine durch die Interpretation der Prädikatensymbole charakterisiert werden. Prof. Dr. Dietmar Seipel 172 Logik für Informatiker Wintersemester 2015/16 Beispiel (Grundmenge UA einer Herbrand–Struktur) • In der Formel F = married (a, b) ∧ ∀X (student(X ) → person(X )) gibt es nur 0–stellige Funktionssymbole (Konstanten); diese bilden die Grundmenge UA = { a, b }. • Die Formel F = p(f (a), g(b)) enthält zwei Konstanten (0–stellige Funktionssymbole) a und b und zwei einstellige Funktionssymbole f und g. Hier ist die Grundmenge UA unendlich groß, denn sie enthält alle Terme, die man daraus bilden kann: UA = { a, b, f (a), f (b), g(a), g(b), f (f (a)), f (g(a)), . . . }. Prof. Dr. Dietmar Seipel 173 Logik für Informatiker Wintersemester 2015/16 • Die Formel G = boolean_normalize_knf (−((a, (b; c))), F ) enthält drei Konstanten (0–stellige Funktionssymbole) a, b und c, ein einstelliges Funktionssymbol ”−”, und zwei zweistellige Funktionssymbole ”,” und ”;”. Auch hier ist die Grundmenge UA unendlich groß, denn sie enthält alle Terme, die man daraus bilden kann: UA = { a, b, c, −a, . . . , (a, b), (a; b), −(a, (b; c)), . . . }. Diese Terme bilden Datenstrukturen zur Repräsentation von aussagenlogischen Formeln. Die entsprechenden Regeln zum Prädikatensymbol boolean_normalize_knf /2 werten diese Terme nicht aus; sie operieren nur symbolisch darauf. Ähnlich kann man auch Listen und Bäume als Terme repräsentieren. Prof. Dr. Dietmar Seipel 174 Logik für Informatiker Wintersemester 2015/16 Variablenbelegungen • Für geschlossene Formeln F ist die Belegung der Variablen X ∈ V mit Werten X A ∈ UA irrelevant. • Für eine quantifizierte Variable X werden sowieso alle Strukturen A[X|u] für u ∈ UA untersucht – ohne den Wert X A zu beachten. • Der Wert X A einer Variable X ist nur relevant, falls X mindestens einmal frei in F vorkommt. Für die Formel F = ( ∀X p(X) ) ∧ q(X) mit je einem gebundenen und einem freien Vorkommen des Variablensymbols X, ist X A nur für das zweite Vorkommen von X relevant. Es gilt pA[X|u] = pA und A(F ) = ∧u∈UA A[X|u] (p(X)) ∧ A(q(X)) = ∧u∈UA (u) ∈ pA ∧ (X A ) ∈ q A . Prof. Dr. Dietmar Seipel 175 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Struktur, Modell) Wir betrachten die folgende geschlossene Formel F : F = f ∧ ∀X r, f = married (a, b), r = student(X ) → person(X ). a und b sind verheiratet, und jeder Studierende ist eine Person. Wir betrachten eine Herbrand–Struktur A. Diese bildet alle Funktionssymbole auf sich selbst ab. Hier gibt es nur 0–stellige Funktionssymbole (Konstanten); diese bilden die Grundmenge UA . UA = { a, b }, αA = α, für alle Konstanten α ∈ UA . Prof. Dr. Dietmar Seipel 176 Logik für Informatiker Wintersemester 2015/16 Wir werden später sehen, daß man das gebundene Variablensymbol X in ∀X r umbenennen könnte, z.B. in Y . Dann würde man die Teilformel ∀ Y ( student(Y ) → person(Y ) ) erhalten, die – entsprechend unserer Anschauung – zu ∀X r äquivalent ist, da man für X und Y sowieso alle Werte u ∈ UA einsetzen kann. A interpretiert die Prädikatensymbole wie folgt: married A = { (a, b) }, student A = { (a), (b) }, person A = { (a) }. Diese Interpretationen könnte man durch eine einzige Menge von Atomen repräsentieren: I = { married (a, b), student(a), student(b), person(a) }. Prof. Dr. Dietmar Seipel 177 Logik für Informatiker Wintersemester 2015/16 Dann gilt A(f ) = (a, b) ∈ married A = 1, A(∀X r) = ∧u∈UA ( (u) ∈ student A → (u) ∈ person A ) = ( (a) ∈ student A → (a) ∈ person A ) ∧ ( (b) ∈ student A → (b) ∈ person A ) = 0, da (b) ∈ student A und (b) 6∈ person A . Da student und person 1–stellige Prädikatensymbole sind, werden Tupel 1 (u) ∈ UA mit nur einer Komponente untersucht. Also ist die untersuchte Struktur A zwar ein Modell von f , aber kein Modell von ∀X r, und somit auch kein Modell von F . Die Struktur A paßt zu F auch ohne eine Interpretation X A des Variablensymbols X anzugeben, da über X quantifiziert wird. Prof. Dr. Dietmar Seipel 178 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Struktur, Modell) Wir betrachten die folgende geschlossene Formel F : F = f1 ∧ f2 ∧ f3 ∧ ∀X ∀Y ∀Z r, f1 = father (a, b), f2 = brother (b, c), f2 = brother (b, d ), r = father (X , Y ) ∧ brother (Y , Z ) → uncle(X , Z ). Ein Onkel Z von X ist ein Bruder des Vaters Y . Man könnte father und brother auch mittels zweier Prädikate parent und male definieren. Wir betrachten wieder eine Herbrand–Struktur A, die die Konstanten (hier die einzigen Funktionssymbole) in F auf sich selbst abbildet: UA = { a, b, c, d }, αA = α, für alle Konstanten α ∈ UA . Prof. Dr. Dietmar Seipel 179 Logik für Informatiker Wintersemester 2015/16 A interpretiert die Prädikatensymbole wie folgt: father A = { (a, b) }, brother A = { (b, c), (b, d) }, uncle A = { (a, c) }. Für die Variablenbelegung X A = a, Y A = b, Z A = c, ist A ein Modell für die Fakten f1 , f2 , f3 , und die Regel r: A(r) = A(father (X , Y )) ∧ A(brother (Y , Z )) → A(uncle(X , Z )) = (a, b) ∈ father A ∧ (b, c) ∈ brother A → (a, c) ∈ uncle A = 1 ∧ 1 → 1 = 1. Der Wahrheitswert von e ∈ M ist 1, falls e ∈ M gilt, sonst 0. Prof. Dr. Dietmar Seipel 180 Logik für Informatiker Wintersemester 2015/16 Die Struktur A[Z|d] interpretiert die Prädikatensymbole wie A. A[Z|d] ist ebenfalls ein Modell für die Fakten f1 , f2 , f3 . Da (a, d) 6∈ uncleA , ist A[Z|d] aber kein Modell für die Regel r: A[Z|d] (r) = A[Z |d] (father (X , Y )) ∧ A[Z |d] (brother (Y , Z )) → A[Z |d] (uncle(X , Z )) = (a, b) ∈ father A ∧ (b, d ) ∈ brother A → (a, d ) ∈ uncle A = 1 ∧ 1 → 0 = 0. Also ist A auch kein Modell für die quantifizierte Regel ∀X ∀Y ∀Z r, und somit auch kein Modell für die komplette Formel F . Wenn wir die Interpretation von uncle erweitern zu uncle A0 = { (a, c), (a, d) } und sonst alles wie in A belassen, dann erhalten wir ein Modell A0 von F . Prof. Dr. Dietmar Seipel 181 Logik für Informatiker Wintersemester 2015/16 Logische Folgerung, Erfüllbarkeit, Gültigkeit Seien F und G prädikatenlogische Formeln. 1. G folgt logisch aus F , falls jedes Modell A von F auch ein Modell von G ist. Dann schreiben wir F |= G. 2. F ist erfüllbar, falls es ein Modell von F gibt. 3. F ist gültig, falls jede zu F passende Struktur ein Modell von F ist. Man kann die logische Folgerung auf die Erfüllbarkeit bzw. die Gültigkeit zurückführen: F |= G ⇐⇒ F ∧ ¬ G ist unerfüllbar ⇐⇒ ¬ (F ∧ ¬ G) ist gültig. Man kann die bekannten Begriffe auf Formelmengen F ausdehnen. Eine endliche Formelmenge F = { f1 , . . . , fn } ist dabei äquivalent zu einer Konjunktion f1 ∧ . . . ∧ fn . Prof. Dr. Dietmar Seipel 182 Logik für Informatiker 2.2 Wintersemester 2015/16 Normalformen Wir werden im folgenden sehen, daß man eine prädikatenlogische Formel äquivalent umformen kann, so daß alle Quantoren am Anfang der Formel stehen (Pränexform). Man kann sogar noch – mittels Skolemfunktionen – alle Existenzquantoren entfernen (Skolemform). Die Skolemform ist genau dann erfüllbar, wenn die Ausgangsformel erfüllbar ist. Die Skolemform kann man dann – wie in der Aussagenlogik – auf Klauselform bringen (KNF). Darauf können wir dann eine verallgemeinerte Resolutionsmethode anwenden. Prof. Dr. Dietmar Seipel 183 Logik für Informatiker Wintersemester 2015/16 Definition (Äquivalenz) Zwei prädikatenlogische Formeln F und G heißen äquivalent, falls für alle sowohl zu F als auch zu G passenden Strukturen A gilt: A(F ) = A(G). Dann schreiben wir F ≡ G. Satz (Äquivalenz) 1. Negation vertauscht die Quantoren ∀ und ∃: ¬ ∀X F ≡ ∃X ¬ F, ¬ ∃X F ≡ ∀X ¬ F. Nicht alle Strukturen passen zu F ist z.B. äquivalent zu es gibt Strukturen, die nicht zu F passen. Prof. Dr. Dietmar Seipel 184 Logik für Informatiker Wintersemester 2015/16 2. Falls X in G nicht frei vorkommt: (QX F ⊗ G) ≡ QX (F ⊗ G), für einen Quantor Q ∈ { ∀, ∃ } und einen Junktor ⊗ ∈ { ∧, ∨ }. 3. Ausklammern von Quantoren: (∀X F ∧ ∀X G) ≡ ∀X (F ∧ G), (∃X F ∨ ∃X G) ≡ ∃X (F ∨ G). 4. Vertauschen gleichartiger Quantoren: ∀X ∀Y F ≡ ∀Y ∀X F, ∃X ∃Y F ≡ ∃Y ∃X F. Dagegen sind die folgenden Formeln im allgemeinen nicht äquivalent: Prof. Dr. Dietmar Seipel (∀XF ∨ ∀XG) 6≡ ∀X (F ∨ G), (∃XF ∧ ∃XG) 6≡ ∃X (F ∧ G). 185 Logik für Informatiker Wintersemester 2015/16 Beispiel (Äquivalenz) 1. Nach 1. gilt ¬ ∀X r(X, Y ) ≡ ∃X ¬ r(X, Y ). 2. Da X und Y nicht frei in ¬ q(Z) vorkommen, kann man nach 2. die Quantoren ∀X und ∃Y sich auf beide Formeln erstrecken lassen: ∀X ∃Y p(X, g(Y, f (X))) ∨ ¬ q(Z) ≡ ∀X ∃Y (p(X, g(Y, f (X))) ∨ ¬ q(Z)). Da X frei in q(X) vorkommt, kann man den Quantor ∀X nicht sich auf beide Formeln erstrecken lassen: ∀X p(X) ∧ q(X) 6≡ ∀X ( p(X) ∧ q(X) ). 3. Für Konjunktionen kann man nach 3. universelle Quantoren ausklammern: ∀X p(X) ∧ ∀X q(X) ≡ ∀X ( p(X) ∧ q(X) ). Prof. Dr. Dietmar Seipel 186 Logik für Informatiker Wintersemester 2015/16 4. Dagegen kann man unterschiedliche Quantoren im Allgemeinen nicht vertauschen: ∀X ∃Y F 6≡ ∃Y ∀X F. Für F = Y > X (Infix–Notation) gilt: wenn man > als die Größer–Relation auf den natürlichen Zahlen interpretiert, d.h. UA = IN0 = { 0, 1, 2, . . . }, >A = { (m, n) ∈ IN02 | m > n }, dann erfüllt A die Formel ∀X ∃Y F , da es für alle X ∈ IN0 eine größere Zahl Y ∈ IN0 gibt, während ∃Y ∀X F nicht erfüllt ist, da es kein Y ∈ IN0 gibt, das größer ist als alle Zahlen X ∈ IN0 : A(∀X ∃Y F ) = 1 6= 0 = A(∃Y ∀X F ). Prof. Dr. Dietmar Seipel 187 Logik für Informatiker Wintersemester 2015/16 Äquivalenz vs. Implikation 1. F ≡ G gilt genau dann, wenn F → G und G → F gültig (Tautologien) sind. 2. Aus F ≡ G folgt, daß F → G und G → F gültig sind. Für die nicht geltenden Äquivalenzen (∀XF ∨ ∀XG) 6≡ ∀X (F ∨ G), (∃XF ∧ ∃XG) 6≡ ∃X (F ∧ G). sind zumindest die folgenden Implikationen gültig: Prof. Dr. Dietmar Seipel (∀XF ∨ ∀XG) → ∀X (F ∨ G), (∃XF ∧ ∃XG) ← ∃X (F ∧ G). 188 Logik für Informatiker Wintersemester 2015/16 Definition (Ersetzung von Variablen) 1. Sei F eine Formel, X eine Variable und t ein Term. Dann bezeichnet F [X|t] diejenige Formel, die man aus F erhält, indem man jedes freie Vorkommen von X durch t ersetzt. 2. [X|t] wird als Substitution bezeichnet. 3. Eine Folge θ = [X1 |t1 ] . . . [Xn |tn ] von Substitutionen wird auch als Substitution bezeichnet. 4. Für eine Formel F bezeichnet F θ die Formel (((F [X1 |t1 ])[X2 |t2 ]) . . . )[Xn |tn ], die man durch sukzessive Anwendung der Substitutionen [Xi |ti ] erhält. Prof. Dr. Dietmar Seipel 189 Logik für Informatiker Wintersemester 2015/16 Beispiel (Substitution) Sei θ = [X|h(Z)] [Y |U ]. In der folgenden Formel sind die ersten beiden Vorkommen von X gebunden und werden nicht durch h(Z) ersetzt: (∀X p(X, f (X), g(Y )) ∨ q(X)) θ = (∀Xp(X, f (X), g(U )) ∨ q(h(Z))). Gebundene Umbenennung Ist F = QX G eine Formel mit einem Quantor Q ∈ { ∃, ∀ } und X 0 eine Variable, die in G nicht vorkommt, dann gilt F = QX G ≡ QX 0 G [X|X 0 ]. Beispiel (Gebundene Umbenennung) Für G = p(X, g(Y, f (X))) gilt ∃Y G ≡ Prof. Dr. Dietmar Seipel ∃Y 0 G [Y |Y 0 ] = ∃Y 0 p(X, g(Y 0 , f (X))). 190 Logik für Informatiker Wintersemester 2015/16 Beispiel (Gebundene Umbenennung) 1. Die folgenden offenen Formeln sind nicht äquivalent: F = p(X), G = p(Y ). Für die Struktur A mit der Grundmenge UA = { 1, 2 } und pA = { (1) } und der Variablenbelegung X A = 1, Y A = 2 gilt A(F ) = (1) ∈ pA = 1 6= 0 = (2) ∈ pA = A(G). 2. Die folgenden quantifizierten Formeln sind dagegen äquivalent: F = ∀ X p(X), G = ∀ Y p(Y ). Es gilt G = ∀ Y p(X) [X|Y ]. Für gebundene Vorkommen kann man das Variablensymbol umbenennen. Prof. Dr. Dietmar Seipel 191 Logik für Informatiker Wintersemester 2015/16 Beispiel (Ausklammern nach gebundener Umbenennung) 1. Die folgenden Formeln sind bekanntermaßen im allgemeinen nicht äquivalent: (∀XF ∨ ∀XG) 6≡ ∀X (F ∨ G), (∃XF ∧ ∃XG) 6≡ ∃X (F ∧ G). 2. Sei F = rot(X) und G = blau(X). • Dann besagt (∀XF ∨ ∀XG) : entweder alle Kugeln sind rot, oder alle Kugeln sind blau. • Dagegen besagt ∀X (F ∨ G), daß jede Kugel entweder rot oder blau ist. Aber es kann sowohl rote als auch blaue Kugeln geben. In den folgenden Strukturen mit einfarbigen Kugeln unterscheiden sich auch die Formeln mit der existentiellen Quantifizierung. Prof. Dr. Dietmar Seipel 192 Logik für Informatiker Wintersemester 2015/16 F1 = (∀Xrot(X) ∨ ∀Xblau(X)) 6≡ F2 = ∀X (rot(X) ∨ blau(X)), G1 = (∃Xrot(X) ∧ ∃Xblau(X)) 6≡ G2 = ∃X (rot(X) ∧ blau(X)). Die folgenden Strukturen Ai mit einfarbigen Kugeln erfüllen G2 nicht, da es keine Kugeln gibt, die gleichzeitig rot und blau sind. A1 A2 A3 A1 erfüllt F2 und G1 , aber nicht F1 und G2 , denn jede Kugel ist entweder rot oder blau (mit Punkt in der Mitte), und es gibt rote und blaue Kugeln. A2 und A3 erfüllen F1 und F2 , aber nicht G1 und G2 , denn in beiden Strukturen haben alle Kugeln dieselbe Farbe, rot bzw. blau. Prof. Dr. Dietmar Seipel 193 Logik für Informatiker Wintersemester 2015/16 3. Für ein frisches Variablensymbol X 0 , das nicht in (∀XF ∨ ∀XG) vorkommt, gilt: (∀XF ∨ ∀XG) ≡ (∀X 0 F [X|X 0 ] ∨ ∀XG) ≡ ∀X 0 (F [X|X 0 ] ∨ ∀XG) ≡ ∀X 0 ∀X (F [X|X 0 ] ∨ G). Also gilt z.B. (∀X rot(X) ∨ ∀X blau(X)) ≡ ∀X 0 ∀X (rot(X 0 ) ∨ blau(X)). Prinzipiell können Kugeln mehrfarbig sein. Wenn es aber eine rote Kugel r gäbe, die nicht auch blau ist, und eine blaue Kugel b, die nicht auch rot ist, dann wäre A[X 0 |b][X|r] (rot(X 0 ) ∨ blau(X)) = 0. 4. Für ein frisches Variablensymbol X 0 , das nicht in (∃XF ∧ ∃XG) vorkommt, gilt analog auch: (∃XF ∧ ∃XG) ≡ ∃X 0 ∃X (F [X|X 0 ] ∧ G). Prof. Dr. Dietmar Seipel 194 Logik für Informatiker Wintersemester 2015/16 5. Auch aus einer Implikation kann man nach gebundener Umbenennung ausklammern: F = ∀X ( p(X ) → ∃X q(X) ) ≡ ∀X ( p(X ) → ∃X 0 q(X 0 ) ) ≡ ∀X ∃X 0 ( p(X ) → q(X 0 ) ). Hier mußte X gebunden in X 0 umbenannt werden, da das Vorkommen von X in p(X) durch ∀X und das Vorkommen von X in q(X) durch ∃X gebunden waren. Nach dem Vorziehen des Quantors ∃X 0 erstrecken sich nun beide Quantoren auf p(X ) → q(X 0 ), also auf beide Teilformeln. Prof. Dr. Dietmar Seipel 195 Logik für Informatiker Wintersemester 2015/16 Definition (BPF, bereinigte Pränexform) 1. Eine Formel F heißt bereinigt, • wenn es keine Variable X gibt, die in F sowohl gebunden als auch frei vorkommt, und • wenn hinter allen vorkommenden Quantoren verschiedene Variablen stehen. 2. Eine Formel F heißt Pränex oder in Pränexform, falls sie von der Form Q1 X1 Q2 X2 . . . Qn Xn G ist, mit Quantoren Qi ∈ { ∃, ∀ } und Variablen Xi , und falls ferner G quantorenfrei ist. Satz (BPF) Für jede Formel F gibt es eine äquivalente Formel G in BPF. Prof. Dr. Dietmar Seipel 196 Logik für Informatiker Wintersemester 2015/16 ∨ Beispiel (BPF) Aus ¬ ∀X r(X, Y ) ∨ ¬ ∀X r(X, Y ) ≡ ∃X 0 ¬ r(X 0 , Y ), ∀X ∃Y p(X, g(Y, f (X))) ¬q(Z) ∀X ∃Y p(X, g(Y, f (X))) ∨ ¬ q(Z) ≡ ∀X ∃Y 0 (p(X, g(Y 0 , f (X))) ∨ ¬ q(Z)), folgt: F = (∀X ∃Y p(X, g(Y, f (X))) ∨ ¬ q(Z)) ∨ ¬ ∀X r(X, Y ) ≡ ∀X ∃Y 0 ∃X 0 ( p(X, g(Y 0 , f (X))) ∨ ¬ q(Z) ∨ ¬ r(X 0 , Y ) ). Die Quantoren ∀X und ∃Y beziehen sich nicht auf ¬ ∀X r(X, Y ). Deswegen benennen wir Y vorne in Y 0 gebunden um und X hinten in X 0 . Danach können alle Quantoren ganz nach vorne gezogen werden. Prof. Dr. Dietmar Seipel 197 Logik für Informatiker Wintersemester 2015/16 Die enstandene Formel in BPF hat immer noch 2 freie Vorkommen von Variablensymbolen, nämlich Y und Z. ∀X ∃Y 0 ∃X 0 ∨ ∨ p(X, g(Y 0 , f (X))) ¬ r(X 0 , Y ) ¬q(Z) Die gebundenen Umbenennungen waren erforderlich, • da X einmal universell und einmal existentiell quantifiziert ist, und • da sich der Quantor ∃Y 0 nicht auf ¬ r(X 0 , Y ) beziehen soll. Prof. Dr. Dietmar Seipel 198 Logik für Informatiker Wintersemester 2015/16 Beispiel (BPF) In der folgenden BPF–Formel F kommt das universell quantifizierte Variablensymbol Y nur im Regelrumpf von r vor: F = ∀X ∀Y ∀Z r, r = father (X , Y ) ∧ brother (Y , Z ) → uncle(X , Z ). Dann könnte man den vor r stehenden Allquantor ∀Y auch als Existenzquantor ∃Y in den Regelrumpf von r ziehen: ∀Y r ≡ ∀Y (¬ (father (X , Y ) ∧ brother (Y , Z )) ∨ uncle(X , Z )) ≡ ∀Y ¬ (father (X , Y ) ∧ brother (Y , Z )) ∨ uncle(X , Z ) ≡ ¬ ∃Y (father (X , Y ) ∧ brother (Y , Z )) ∨ uncle(X , Z ) ≡ ∃Y (father (X , Y ) ∧ brother (Y , Z )) → uncle(X , Z ). Prof. Dr. Dietmar Seipel 199 Logik für Informatiker Wintersemester 2015/16 Exkurs: Existenzquantor im Regelkopf Ein Existenzquantor ∃ Y im Kopf einer BPF–Regel, F = ∀X ( kugel (X ) → ∃ Y farbe(X , Y ) ), entspricht dagegen einem vor der Regel stehenden Existenzquantor ∃ Y : F ≡ ∀X ∃ Y ( kugel (X ) → farbe(X , Y ) ). Für eine vorgegebene Struktur A ergibt er eine Disjunktion im Regelkopf: A(F ) = ∧u∈UA ( (u) ∈ kugel A → ∨v ∈UA (u, v ) ∈ farbe A ). Da die Grundmenge U = UA für Herbrand–Strukturen unabhängig von A ist, könnte man F praktisch wie eine Regel mit einem disjunktiven Kopf auffassen: F = ˆ ∀X ( kugel (X ) → ∨v ∈U farbe(X , v ) ). Prof. Dr. Dietmar Seipel 200 Logik für Informatiker Wintersemester 2015/16 In der Praxis möchte man allerdings für v ∈ U nur Farben zulassen, etwa rot, gr¨ u n, blau. Dann meint man eigentlich die folgende Formel: ∀X ( kugel (X ) → farbe(X , rot) ∨ farbe(X , gr¨ u n) ∨ farbe(X , blau) ). Diese könnte man wieder mit einem Existenzquantor ∃ Y im Regelkopf ausdrücken, G = ∀X ( kugel (X ) → ∃ Y (farbe(Y ) ∧ farbe(X , Y )) ). Man könnte dazu ein 1–stelliges Prädikat farbe, das die zugelassenen Farben angibt, mit Hilfe geeigneter Formeln definieren. Prof. Dr. Dietmar Seipel 201 Logik für Informatiker Wintersemester 2015/16 Definition (Skolemform) Zu einer Formel F in BPF erhält man die Skolemform durch Elimination der Existenzquantoren nach folgendem Schema: 1. Wir betrachten den ersten Existenzquantor in F : F = ∀X1 ∀X2 . . . ∀Xn ∃X G. 2. Sei f ein neues bisher in F nicht vorkommendes n–stelliges Funktionssymbol. Dann setzen wir F 0 = ∀X1 ∀X2 . . . ∀Xn G [X|f (X1 , . . . , Xn )]. Nun eliminieren wir nach demselben Schema alle weiteren Existenzquantoren in F 0 . 3. Sobald die so erhaltene Formel F 00 keine Existenzquantoren mehr enthält, ist sie in Skolemform: F 00 = ∀X1 ∀X2 . . . ∀Xk F ∗ mit quantorenfreier Formel F ∗ , die wir Matrix nennen. Prof. Dr. Dietmar Seipel 202 Logik für Informatiker Wintersemester 2015/16 Beispiel (Skolemform) Wir betrachten die folgende Formel F in BPF: F = ∃X ∀Y ∃Z ∀V ∃W ¬p(X, Y, Z, V, W ) F0 = ∀Y ∃Z ∀V ∃W ¬p(a, Y, Z, V, W ) F 00 = ∀Y ∀V ∃W ¬p(a, Y, f (Y ), V, W ) F 000 = ∀Y ∀V ¬p(a, Y, f (Y ), V, g(Y, V )). Wir ersetzen die existentiell quantifizierten Variablen durch Terme: • Zuerst ersetzen wir X durch eine frische Konstante a. • Dann ersetzen wir Z im Scope von Y durch einen Term f (Y ). • Schließlich ersetzen wir W im Scope von Y und V durch einen Term g(Y, V ). Prof. Dr. Dietmar Seipel 203 Logik für Informatiker Wintersemester 2015/16 Beispiel (Skolemform) Das 3–stellige Prädikatensymbol p steht für eine Gruppenoperation; wir schreiben p(X, Y, Z) anstelle von X ◦ Y = Z (Produkt). Die folgende Formel beschreibt die Gruppenaxiome zur Existenz eines links–neutralen Elements (X) und zur Existenz von Links–Inversen (Z): F = ∃X ( ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y, X) ). Wir bringen F zuerst in BPF, und dann mittels zweier Skolemfunktionen e (0–stellig) und i (1–stellig) in Skolemform F 0 : F ≡ ∃X ∀Y ∃Z ( p(X, Y, Y ) ∧ p(Z, Y, X) ), F0 = ∀Y ( p(e, Y, Y ) ∧ p(i(Y ), Y, e) ). Bei der Erzeugung der BPF wurde der bekannte Satz zur Verschiebung der Quantoren ∀Y und ∃Z angewendet. Prof. Dr. Dietmar Seipel 204 Logik für Informatiker Wintersemester 2015/16 Definition (Erfüllbarkeitsäquivalenz) Zwei prädikatenlogische Formeln F und G heißen erfüllbarkeitsäquivalent, wenn gilt: F ist genau dann erfüllbar, wenn G erfüllbar ist. F und G müssen nicht dieselben Modelle haben. Die Erfüllbarkeitsäquivalenz bedeutet aber, daß F und G entweder beide ein Modell besitzen, oder daß keine der beiden Formeln ein Modell besitzt. Beispiel (Erfüllbarkeitsäquivalenz) Indem man die freie Variable X in G = ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y, X) existentiell quantifiziert, erhält man eine erfüllbarkeitsäquivalente Formel F = ∃X ( ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y, X) ). Prof. Dr. Dietmar Seipel 205 Logik für Informatiker Wintersemester 2015/16 Satz (Skolemform) Eine Formel F in BPF ist genau dann erfüllbar, wenn ihre Skolemform erfüllbar ist. Beweis: Wir betrachten den Eliminationsschritt F 7→ F 0 für den ersten Existenzquantor: F = ∀X1 ∀X2 . . . ∀Xn ∃X G. 1. Annahme: F 0 ist erfüllbar mit einer passenden Struktur A0 , d.h. A0 (F 0 ) = 1. Dann paßt A0 auch zu F und es gilt ∀u1 , . . . , un ∈ UA0 : A0[X1 |u1 ]...[Xn |un ] (G[X|f (X1 , . . . , Xn )]) = 1. Prof. Dr. Dietmar Seipel 206 Logik für Informatiker Wintersemester 2015/16 Daraus folgt ∀u1 , . . . , un ∈ UA0 : A0[X |u ]...[X |u ][X|f A0 (u 1 1 n n 1 ,... ,un )] (G) = 1. Daraus folgt 0 ∀u1 , . . . , un ∈ UA0 : ∃u = f A (u1 , . . . , un ) ∈ UA0 : A0[X1 |u1 ]...[Xn |un ][X|u] (G) = 1. Daraus folgt A0 (∀X1 . . . ∀Xn ∃X G) = 1. Also ist A0 auch ein Modell für F . Prof. Dr. Dietmar Seipel 207 Logik für Informatiker Wintersemester 2015/16 2. Annahme: F ist erfüllbar mit einer passenden Struktur A, d.h. A(F ) = 1. Wir können annehmen, daß IA auf keinen anderen als den in F vorkommenden Funktionssymbolen, Prädikatensymbolen und freien Variablen definiert ist. Dann gilt: ∀u1 , . . . , un ∈ UA : ∃u ∈ UA : A[X1 |u1 ]...[Xn |un ][X|u] (G) = 1. Wir erweitern nun die Struktur A zu einer neuen Struktur A0 durch A0 Definition einer Funktion f mit f A0 (u1 , . . . , un ) = u durch Verwendung des Auswahlaxioms. Es gilt UA0 = UA . Prof. Dr. Dietmar Seipel 208 Logik für Informatiker Wintersemester 2015/16 Daraus folgt ∀u1 , . . . , un ∈ UA0 : A0[X |u ]...[X |u ][X|f A0 (u 1 1 n n 1 ,... ,un )] (G) = 1. Daraus folgt ∀u1 , . . . , un ∈ UA0 : A0[X1 |u1 ]...[Xn |un ] (G[X|f (X1 , . . . , Xn )]) = 1. Daraus folgt A0 (∀X1 . . . ∀Xn G[X|f (X1 , . . . , Xn )]) = 1. Also ist A0 ein Modell für F . Prof. Dr. Dietmar Seipel 209 Logik für Informatiker Wintersemester 2015/16 Zusammenfassung (BPF, Skolemform) 1. Für jede Formel F gibt es eine äquivalente Formel G in BPF. 2. F und G haben genau dieselben Modelle. 3. Für jede Formel F gibt es eine Formel H in Skolemform. • F und H müssen nicht dieselben Modelle haben. • Insbesondere unterscheiden sich die Modelle in der Regel aufgrund der Skolemfunktionen in H. • Die Skolemform H wird durch Elimination der Existenzquantoren aus der BPF G konstruiert. 4. Eine Formel F ist genau dann erfüllbar, wenn ihre Skolemform H erfüllbar ist. Prof. Dr. Dietmar Seipel 210 Logik für Informatiker Wintersemester 2015/16 Klauselform Aus einer Formel F kann man über die Skolemform eine Klauselmenge M gewinnen. Eine Klausel ist eine Disjunktion prädikatenlogischer Literale. 1. Durch systematisches Umbenennen der gebundenen Variablen in F bilden wir eine neue, bereinigte Formel F1 , die zu F äquivalent ist. 2. Seien Y1 , . . . , Yn die in F1 vorkommenden freien Variablen. Dann enthält F2 = ∃Y1 . . . ∃Yn F1 keine ungebundenen Variablen mehr, und F2 ist erfüllbarkeitsäquivalent zu F1 . 3. Sei F3 = ∀X1 . . . ∀Xm G3 eine Skolemform zu F2 mit der (quantorenfreien) Matrix G3 . Dann sind alle Variablen in F3 universell quantifiziert, und F3 ist erfüllbarkeitsäquivalent zu F2 . 4. Man kann die Matrix G3 in eine KNF G4 = ∧ki=1 βi mit Klauseln βi umformen. Dann ist F4 = ∀X1 . . . ∀Xm G4 zu F3 äquivalent. Prof. Dr. Dietmar Seipel 211 Logik für Informatiker Wintersemester 2015/16 Insgesamt gilt: • F4 ist erfüllbarkeitsäquivalent zu F , und • alle Variablen in F4 sind universell quantifiziert. Die Klauselmenge M = { β1 , . . . , βk } spielt später bei Inferenzmethoden eine entscheidente Rolle. Man kann mittels der Resolutionsmethode genau dann die leere Klausel aus M ableiten, wenn F unerfüllbar ist. Beispiel (Klauselmenge) Die Formel G = ∀Y p(X, Y, Y ) ∧ ∀Y ∃Z p(Z, Y, X) wird zur Klauselmenge M = { p(e, Y, Y ), p(i(Y ), Y, e) }. Prof. Dr. Dietmar Seipel 212 Logik für Informatiker 2.3 Wintersemester 2015/16 Unentscheidbarkeit Es gibt prädikatenlogische Formeln F , die zwar erfüllbar sind, jedoch nur unendliche Modelle A = (UA , IA ) besitzen, also solche mit unendlicher Grundmenge UA : F = ∀X p(X, f (X)) ∧ ∀X ¬p(X, X) ∧ ∀X ∀Y ∀Z ( (p(X, Y ) ∧ p(Y, Z)) → p(X, Z) ) Dann gibt es das folgende unendliche Modell A = (UA , IA ) : UA = IN0 = { 0, 1, 2, . . . }, pA = { (m, n) ∈ IN02 | m < n }, f A (n) = n + 1. Die Formel F besitzt jedoch kein endliches Modell. Prof. Dr. Dietmar Seipel 213 Logik für Informatiker Wintersemester 2015/16 Angenommen B = (UB , IB ) ist ein Modell mit endlicher Grundmenge UB . Für ein beliebiges Element m0 ∈ UB betrachten wir die Folge m0 , m1 , m2 , . . . ∈ UB , mit mi+1 = f B (mi ). Wegen des ersten Konjunktionsgliedes von F gilt (m0 , m1 ), (m1 , m2 ), . . . , (mi , mi+1 ) ∈ pB , für alle i ∈ IN0 . Wegen des dritten Konjunktionsgliedes von F ist pB transitiv, d.h. (mi , mj ) ∈ pB , für alle i, j ∈ IN0 mit i < j. Da UB endlich ist, muß es zwei Indizes i und j mit i < j geben, mit mi = mj = m. Also gibt es (m, m) ∈ pB , im Widerspruch zum zweiten Konjunktionsglied von F (Irreflexivität). Prof. Dr. Dietmar Seipel 214 Logik für Informatiker Wintersemester 2015/16 Obiges Beispiel zeigt, daß sich die Wahrheitstafelmethode nicht in die Prädikatenlogik übertragen läßt. Entscheidbarkeit Ein (ja/nein–) Problem heißt entscheidbar oder rekursiv, falls es ein Rechenverfahren gibt (z.B. formuliert als Programm in C++), das für alle Eingaben immer nach endlicher Zeit stoppt, und dann korrekt “ja” oder “nein” ausgibt. Anderenfalls heißt ein Problem unentscheidbar. Gültigkeitsproblem der Prädikatenlogik: Gegeben eine prädikatenlogische Formel F . Frage: Ist F eine gültige Formel ? Prof. Dr. Dietmar Seipel 215 Logik für Informatiker Wintersemester 2015/16 Satz (Church) Das Gültigkeitsproblem der Prädikatenlogik ist unentscheidbar. Beweis durch Zurückführung auf das unentscheidbare Postsche Korrespondenzproblem: • Gegeben eine endliche Folge (x1 , y1 ), . . . , (xn , yn ) von Paaren xi , yi ∈ {0, 1}+ von nicht–leeren Strings über {0, 1}. • Frage: Gibt es eine Folge von Indizes i1 , . . . , im ∈ { 1, . . . , n }, mit m ≥ 1, so daß die Konkatenationen der entsprechenden Strings übereinstimmen ? xi1 xi2 . . . xim = yi1 yi2 . . . yim . Prof. Dr. Dietmar Seipel 216 Logik für Informatiker Wintersemester 2015/16 Beispiel (Postsches Korrespondenzproblem) Sei K = ((x1 , y1 ), (x2 , y2 ), (x3 , y3 )) mit x1 = 1 und y1 = 101, x2 = 10 und y2 = 00, x3 = 011 und y3 = 11. Lösung: i1 = 1, i2 = 3, i3 = 2, i4 = 3 x1 x3 x2 x3 z}|{ z }| { z}|{ z }| { x1 x3 x2 x3 = 1 0 1 1 1 0 0 1 1 = y1 y3 y2 y3 . | {z } |{z} |{z} |{z} y1 y3 y2 y3 Folgerung (Erfüllbarkeitsproblem) Das Erfüllbarkeitsproblem der Prädikatenlogik Ist eine gegebene prädikatenlogische Formel F erfüllbar ? ist ebenfalls unentscheidbar. Prof. Dr. Dietmar Seipel 217 Logik für Informatiker 2.4 Wintersemester 2015/16 Herbrand–Theorie Jacques Herbrand, Kurt Gödel, Thoralf Skolem Definition (Herbrand–Universum) Das Herbrand–Universum HUF einer Formel F ist die Menge aller variablenfreien Terme, die aus Bestandteilen von F gebildet werden können. Falls F keine Konstante (d.h., kein 0–stelliges Funktionssymbol) enthält, so nehmen wir eine beliebige Konstante a zur Konstruktion von HUF hinzu. Das Herbrand–Universum HUF ist meist unendlich groß, aber man kann es systematisch konstruieren. Prof. Dr. Dietmar Seipel 218 Logik für Informatiker Wintersemester 2015/16 Induktive Konstruktion: 1. Alle in F vorkommenden Konstanten sind in HUF . 2. Falls F keine Konstanten enthält, so nimmt man eine beliebige Konstante a zu HUF hinzu. 3. Für jedes in F vorkommende • n–stellige Funktionssymbol f und • Terme t1 , . . . , tn ∈ HUF ist auch der Term f (t1 , . . . , tn ) in HUF . Für ein 1–stelliges Funktionssymbol f und eine Konstante a setzen wir • f 0 (a) = a und • f k+1 (a) = f (f k (a)), für alle k ∈ IN0 . Z.B. entsteht f 2 (a) = f (f (a)) durch 2–malige Anwendung von f auf a. Prof. Dr. Dietmar Seipel 219 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Universum) Die Formel F = p(f (a), g(b)) enthält zwei Konstanten (0–stellige Funktionssymbole) a und b und zwei einstellige Funktionssymbole f und g. Daraus setzen sich die Terme des Herbrand–Universums zusammen. 1. a und b sind in HUF . Da F bereits Konstanten enthält, ist keine zusätzliche Konstante erforderlich. 2. Mit den Funktionssymbolen f und g kann man weitere Terme bilden. Die Tatsache, daß a in F nur als Argument von f vorkommt und b nur als Argument von g ist dabei unerheblich. Auch die “gekreuzten” Terme f (b) und g(a) sind in HUF . 3. Falls h1 , . . . , hn eine beliebige Folge von Funktionssymbolen ist, mit hi ∈ {f, g}, so sind auch h1 (. . . (hn (a))) und h1 (. . . (hn (b))) in HUF . 4. HUF = { a, b, f (a), f (b), g(a), g(b), f (f (a)), f (g(a)), . . . }. Prof. Dr. Dietmar Seipel 220 Logik für Informatiker Wintersemester 2015/16 HUF ist genau dann unendlich groß, wenn F ein n–stelliges Funktionssymbol mit n ≥ 1 enthält. Für ein 1–stelliges Funktionssymbol f in F und eine Konstante a ∈ HUF sind z.B. auch alle Terme f k (a) in HUF . Beispiel (Herbrand–Universum) Die Formel F in BPF enthält ein einstelliges Funktionssymbol f : F = ∃X p(f (X)), HUF = { a, f (a), f (f (a)), . . . } = { f k (a) | k ∈ IN0 }. Da F keine Konstanten enthält, nehmen wir die Konstante a zu HUF hinzu. Dasselbe Herbrand–Universum würden wir auch für die variablenfreie Formel F 0 = p(f (a)) erhalten. Prof. Dr. Dietmar Seipel 221 Logik für Informatiker Wintersemester 2015/16 Man kann das Herbrand–Universum HUF wie folgt systematisch als unendliche Vereinigung endlicher Mengen konstruieren: 1. HU1 sei die Menge aller in F vorkommenden Konstanten, bzw. HU1 = { a }, falls F keine Konstanten enthält. 0 2. HUk+1 sei die Menge aller Terme f (t1 , . . . , tn ) aus einem in F vorkommenden n–stelligen Funktionssymbol f und Termen 0 t1 , . . . , tn ∈ HUk , und HUk+1 = HUk ∪ HUk+1 . 3. Dann sind alle Mengen HUk endlich, die Folge (HUk )k∈IN+ ist aufsteigend, und HUF = ∪∞ k=1 HUk . Also ist das Herbrand–Universum HUF abzählbar. Man erhält per Induktion eine injektive Abbildung HUF → IN, indem man sukzessive die endlichen Mengen HUk+1 \ HUk fortlaufend durchnummeriert. Prof. Dr. Dietmar Seipel 222 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Universum) Die folgende Formel F enthält vier Funktionssymbole: F = ∀X ∀Y p(a, f (X), g(Y, b)). a und b sind 0–stellig, und somit Konstanten. f ist 1–stellig, g ist 2–stellig. HU1 = { a, b }, HU2 = HU1 ∪ { f (a), f (b), g(a, a), g(a, b), g(b, a), g(b, b) }, HUk+1 = HUk ∪ { f (t) | t ∈ HUk } ∪ { g(t1 , t2 ) | t1 , t2 ∈ HUk }. Sobald eine Formel F mindestens ein n–stelliges Funktionssymbol f , mit n ≥ 1, enthält, ist das Herbrand–Universum HUF unendlich groß: HUF enthält immer eine Konstante, und man kann aus jedem Term t ∈ HUk+1 \ HUk einen neuen Term f (t, . . . , t) ∈ HUk+2 \ HUk+1 bilden. Prof. Dr. Dietmar Seipel 223 Logik für Informatiker Wintersemester 2015/16 Definition (Herbrand–Strukturen) Sei F eine Formel und A = (UA , IA ) eine zu F passende Struktur. Dann heißt A eine Herbrand–Struktur für F , falls gilt: 1. Die Grundmenge von A ist UA = HUF . 2. Für alle Terme f (t1 , . . . , tn ) ∈ HUF : A(f (t1 , . . . , tn )) = f A (A(t1 ), . . . , A(tn )) = f (t1 , . . . , tn ). Terme werden also von Herbrand–Strukturen durch sich selbst interpretiert. Herbrand–Strukturen für geschlossene Formeln sind vollständig durch die Interpretation pA der Prädikatensymbole charakterisiert. Man nennt die entsprechende Menge I eine Herbrand–Interpretation: I = { p(t1 , . . . , tn ) | t1 , . . . , tn ∈ HUF ∧ (t1 , . . . , tn ) ∈ pA } Eine Herbrand–Struktur, welche ein Modell für eine Formel F ist, heißt Herbrand–Modell für F . Prof. Dr. Dietmar Seipel 224 Logik für Informatiker Wintersemester 2015/16 Beispiel (3–Färbbarkeit) Gesucht ist eine Färbung der Knoten eines Graphen G = h V, E i mit drei Farben (rot, grün, blau), so daß adjazente Knoten unterschiedliche Farben haben: b a d e c Wir repräsentieren die Knoten und Kanten des Graphen als Fakten: f1 = node(a), f2 = node(b), . . . , f5 = node(e), e1 = edge(a, b), e2 = edge(a, c), . . . , e6 = edge(d , e). Prof. Dr. Dietmar Seipel 225 Logik für Informatiker Wintersemester 2015/16 g = color , (X , red ) ∨ color (X , green) ∨ color (X , blue) ← node(X ) c0 = ← edge(X , Y ) ∧ color (X , C ) ∧ color (Y , C ), c1 = ← color (X , red ) ∧ color (X , green), c2 = ← color (X , red ) ∧ color (X , blue), c3 = ← color (X , green) ∧ color (X , blue). Die disjunktive Regel g wählt für jeden Knoten eine Farbe aus. Die Integritätsbedingung c0 verhindert, daß adjazente Knoten die gleiche Farbe bekommen. Die Integritätsbedingungen c1 , c2 , c3 verhindern, daß ein Knoten zwei Farben bekommt. Nebenbemerkung: Jeder planare Graph ist 4–färbbar. Für allgemeine Graphen ist der Test auf 3–Färbbarkeit N P–vollständig. Prof. Dr. Dietmar Seipel 226 Logik für Informatiker Wintersemester 2015/16 Wir betrachten dann die Formel F = f1 ∧ . . . ∧ f5 ∧ e1 ∧ . . . ∧ e6 ∧ ∀Xg ∧ ∀X∀Y ∀C c0 ∧ ∀Xc1 ∧ . . . ∧ ∀Xc3 . F ist äquivalent zur folgenden Formel F 0 in Skolemform: F 0 = ∀X ∀ Y ∀ C (f1 ∧ . . . ∧ f5 ∧ e1 ∧ . . . ∧ e6 ∧ g ∧ c0 ∧ . . . ∧ c3 ). Das Herbrand–Universum ist HUF = { a, b, c, d, e, red , green, blue }. Prof. Dr. Dietmar Seipel 227 Logik für Informatiker Wintersemester 2015/16 b a d e c Die folgende Herbrand–Interpretation I repräsentiert ein Herbrand–Modell für die Formel F : I = { node(a), . . . , node(e), edge(a, b), . . . , edge(d , e), color (a, red ), color (b, green), color (c, blue), color (d , red ), color (e, green) }. Prof. Dr. Dietmar Seipel 228 Logik für Informatiker Wintersemester 2015/16 Die zugehörigen Interpretationen pA der Prädikatensymbole sind folgende: node A = { (a), . . . , (e) }, edge A = { (a, b), . . . , (d, e) }, color A = { (a, red), (b, green), (c, blue), (d, red), (e, green) }. Die Herbrand–Interpretation I faßt diese Mengen pA zu einer einzigen Menge zusammen. Damit man die Tupel (t1 , . . . , tn ) ∈ pA korrekt zuordnen kann, werden sie in I als Atome p(t1 , . . . , tn ) mit Prädikatensymbol notiert: I = { p(t1 , . . . , tn ) | t1 , . . . , tn ∈ HUF ∧ (t1 , . . . , tn ) ∈ pA }. Würde man einfach die Vereinigung der Mengen pA benutzen, so könnte man z.B. nicht wissen, ob ein Paar (t1 , t2 ) zu edge A oder zu color A gehört. Prof. Dr. Dietmar Seipel 229 Logik für Informatiker Wintersemester 2015/16 Satz (Herbrand–Modell) Eine Aussage F in Skolemform ist genau dann erfüllbar, wenn F ein Herbrand–Modell besitzt. Beweis: 1. ⇐: Klar. 2. ⇒: Sei A = (UA , IA ) ein beliebiges Modell für F . Falls F keine Konstanten enthält und a als zusätzliche Konstante gewählt wurde, so setzen wir aA = a0 , für ein beliebiges Element a0 ∈ UA . A ist danach immer noch ein Modell für F . Wir konstruieren nun aus A eine Herbrand–Struktur B = (UB , IB ) für F , d.h. mit der Grundmenge UB = HUF . Dazu müssen wir die Prädikatensymbole p aus F interpretieren. Prof. Dr. Dietmar Seipel 230 Logik für Informatiker Wintersemester 2015/16 Sei p ein n–stelliges Prädikatensymbol, und seien t1 , . . . , tn ∈ HUF : (t1 , . . . , tn ) ∈ pB g.d.w. (A(t1 ), . . . , A(tn )) ∈ pA Wir zeigen nun, daß B ein Modell für F ist. Mehr noch: Für jede Aussage G in Skolemform, die aus den Bestandteilen von F aufgebaut ist, gilt: A |= G ⇒ B |= G. Wir führen eine Induktion über die Anzahl n der Allquantoren von G. n = 0: G enthält keine Quantoren. Dann haben alle Atome von G unter A und B denselben Wahrheitswert, und deshalb gilt A(G) = B(G). n → n + 1: Sei G eine Formel mit n + 1 Allquantoren, und zwar von der Form G = ∀X H, wobei H nur n Allquantoren enthält. Prof. Dr. Dietmar Seipel 231 Logik für Informatiker Wintersemester 2015/16 Wegen A |= G gilt: ∀ u ∈ UA : A[X|u] (H) = 1. Insbesondere gilt für alle u = A(t) ∈ UA mit t ∈ HUG : A[X|A(t)] (H) = 1. Deshalb gilt: ∀ t ∈ HUG : A(H[X|t]) = A[X|A(t)] (H) = 1. Nach Induktionsvoraussetzung gilt nun: ∀ t ∈ HUG : B(H[X|t]) = 1. Deshalb gilt: ∀ t ∈ HUG : B[X|B(t)] (H) = B(H[X|t]) = 1. Also gilt B(G) = B(∀X H) = 1. Prof. Dr. Dietmar Seipel 232 Logik für Informatiker Wintersemester 2015/16 Der obige Satz über Herbrand–Modelle wäre falsch, wenn wir nicht eine frische Konstante a zu HUF hinzunehmen würden, falls F keine Konstanten enthält – denn dann wäre die Grundmenge HUF = ∅. Beispiel (Herbrand–Modell) Für die Formel F = ∃X p(X) ist das Herbrand–Universum HUF = { a }, und das einzige Herbrand–Modell A ist gegeben durch pA = { (a) }. Ohne die frische Konstante a könnte man kein Herbrand–Modell bilden, da F fordert, daß pA mindestens ein Tupel (t), mit t ∈ HUF , enthalten muß. Prof. Dr. Dietmar Seipel 233 Logik für Informatiker Wintersemester 2015/16 Satz (Löwenheim und Skolem) Jede erfüllbare Formel F der Prädikatenlogik besitzt ein abzählbares Modell B = (UB , IB ), d.h. mit einer abzählbaren Grundmenge UB . Man kann für B ein Herbrand–Modell der Skolemform von F wählen. Definition (Herbrand–Expansion) Sei F = ∀X1 ∀X2 . . . ∀Xn G eine Formel in Skolemform mit der (quantorenfreien) Matrix G. Dann ist die Herbrand–Expansion von F definiert als E(F ) = { G[X1 |t1 ] . . . [Xn |tn ] | t1 , . . . , tn ∈ HUF }. Prof. Dr. Dietmar Seipel 234 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Expansion) Für die folgende Formel F in Skolemform F = ∀X (f ∧ r), f = married (a, b), r = student(X ) → person(X ), ist HUF = { a, b }, und die Herbrand–Expansion E(F ) = { married (a, b) ∧ (student(a) → person(a)), married (a, b) ∧ (student(b) → person(b)) } hat 2 Elemente, da man das Variablensymbol X mit den zwei Konstanten aus HUF belegen kann. Prof. Dr. Dietmar Seipel 235 Logik für Informatiker Wintersemester 2015/16 Beispiel (Herbrand–Expansion) Für die Formel F = ∀X1 ∀X2 ∀X3 G, mit G = F1 ∧ F2 ∧ F3 ∧ F4 ∧ F5 und F1 = ancestor(X1 , X2 ) ← parent(X1 , X2 ), F1 = ancestor(X1 , X2 ) ← parent(X1 , X3 ) ∧ ancestor(X3 , X2 ), F3 = parent(a, b), F4 = parent(b, c), F5 = parent(c, d), git HUF = { a, b, c, d }, und E(F ) hat 43 = 64 Elemente. Eines davon ist z.B. Gθ = F1 θ ∧ F2 θ ∧ F3 ∧ F4 ∧ F5 , für θ = [X1 |a] [X2 |c] [X3 |b]: F1 θ = ancestor(a, c) ← parent(a, c), F2 θ = ancestor(a, c) ← parent(a, b) ∧ ancestor(b, c). Prof. Dr. Dietmar Seipel 236 Logik für Informatiker Wintersemester 2015/16 Falls F Variablensymbole und Funktionssymbole der Stelligkeit n ≥ 1 enthält, so sind HUF und E(F ) unendlich groß. Beispiel (Herbrand–Expansion) Für die Formel F = ∀X1 ∀X2 p(X1 , f (X2 ), g(X1 , X2 )) in Skolemform erhalten wir die folgende Herbrand–Expansion: HUF = { a, f (a), g(a, a), f (f (a)), f (g(a, a)), g(a, f (a)), g(a, g(a, a)), g(f (a), a), g(f (a), f (a)), g(f (a), g(a, a)), g(g(a, a), a), g(g(a, a), f (a)), g(g(a, a), g(a, a)), . . . }, E(F ) = { p(t1 , f (t2 ), g(t1 , t2 )) | t1 , t2 ∈ HUF }. Da F keine Konstante enthält, wurde a zu HUF hinzugenommen. Prof. Dr. Dietmar Seipel 237 Logik für Informatiker Wintersemester 2015/16 Im Grunde genommen kann E(F ) als eine – meist unendliche – aussagenlogische Formelmenge angesehen werden, wenn man die in E(F ) vorkommenden Grundatome als atomare Formeln der Aussagenlogik auffaßt. Satz (Gödel, Herbrand und Skolem) Eine Aussage F in Skolemform ist genau dann unerfüllbar, wenn es eine endliche Teilmenge von E(F ) gibt, die (im aussagenlogischen Sinne) unerfüllbar ist. Beweis: Mittels des Satzes von Gödel, Herbrand und Skolem und des Endlichkeitssatzes der Aussagenlogik. Prof. Dr. Dietmar Seipel 238 Logik für Informatiker Wintersemester 2015/16 Semi–Entscheidungsverfahren für die Prädikatenlogik Gilmore: Für jede prädikatenlogische Formel F ist die Herbrand–Expansion E(G) = { G1 , G2 , . . . } der Skolemform G von F abzählbar, da auch das Herbrand–Universum HUF abzählbar ist. F ist genau dann erfüllbar, wenn alle Konjunktionen G1 ∧ G2 ∧ . . . ∧ Gn , mit n ∈ IN+ = { 1, 2, . . . }, erfüllbar sind. Durch sukzessives Testen dieser Konjunktionen auf Unerfüllbarkeit erhält man also ein Verfahren, welches für unerfüllbare Formeln F nach endlicher Zeit stoppt. Prof. Dr. Dietmar Seipel 239 Logik für Informatiker Wintersemester 2015/16 Für erfüllbare Formeln F terminiert das Verfahren offensichtlich nicht immer. → Semi–Entscheidbarkeit des Unerfüllbarkeitsproblems. Durch Anwendung des Testverfahrens auf ¬F kann man auf Gültigkeit testen. → Semi–Entscheidbarkeit des Gültigkeitsproblems. Prof. Dr. Dietmar Seipel 240 Logik für Informatiker 2.5 Wintersemester 2015/16 Resolution Wir betrachten eine prädikatenlogische Formel F = ∀X1 ∀X2 . . . ∀Xm G in Skolemform ohne freie Variablen und mit der Matrix G in KNF. • Die Matrix G ist quantorenfrei und von der Form G = ∧ki=1 βi . • Wir untersuchen nun die zugehörige Klauselmenge M = { β1 , . . . , βk }. Eine Struktur A heißt Modell für M , falls A ein Modell für F ist. Wir betrachten eine Klauselmenge M also wie eine KNF zusammen mit Allquantoren für alle vorkommenden Variablen. Eine Klausel β = L1 ∨ . . . ∨ Ln wird auch oft als Menge { L1 , . . . , Ln } von Literalen repräsentiert. Prof. Dr. Dietmar Seipel 241 Logik für Informatiker Wintersemester 2015/16 Definition (Resolutionsableitung) Sei M eine Klauselmenge. Eine Folge K1 , K2 , . . . , Kn von Klauseln nennt man Resolutionsableitung, falls für alle 1 ≤ i ≤ n gilt: 1. Ki ist eine Grundinstanz einer Klausel K ∈ M , d.h. Ki = K[X1 |t1 ] . . . [Xk |tk ], mit t1 , . . . , tk ∈ HUF , oder 2. Ki ist eine (aussagenlogische) Resolvente zweier Klauseln Ka und Kb mit 1 ≤ a, b ≤ i − 1. M ist genau dann unerfüllbar, wenn es eine Resolutionsableitung der leeren Klausel Kn = 2 gibt. Dasselbe gilt für die entsprechende prädikatenlogische Formel F . Prof. Dr. Dietmar Seipel 242 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolution) Wir betrachten die Klauselmenge M = { F1 , F2 , F3 } mit F1 = ¬p(X) ∨ ¬p(f (a)) ∨ q(Y ), F2 = p(Y ), F3 = ¬p(g(b, X)) ∨ ¬q(b). Dann kann man • F1 [X|f (a)] [Y |b] und F2 [Y |f (a)] zu K = { q(b) } resolvieren, und • F2 [Y |g(b, a)] und F3 [X|a] zu K 0 = { ¬q(b) }. Aus K und K 0 erhält man schließlich die leere Klausel 2. Also sind die Klauselmenge M und die zugehörige Formel F unerfüllbar: F = ∀X ∀ Y (F1 ∧ F2 ∧ F3 ). Prof. Dr. Dietmar Seipel 243 Logik für Informatiker Wintersemester 2015/16 Baumdarstellung: { ¬p(X), ¬p(f (a)), q(Y ) } [X|f (a)] [Y |b] { p(Y ) } [Y |f (a)] ? { ¬p(f (a)), q(b) } { ¬p(g(b, X)), ¬q(b) } [Y |g(b, a)] R { p(f (a)) } { p(g(b, a)) } U  [X|a] ? { ¬p(g(b, a)), ¬q(b) } U  { q(b) } { ¬q(b) } s 2 + Die Klausel { p(Y ) } wurde in der Resolutionsableitung zweimal benutzt. Prof. Dr. Dietmar Seipel 244 Logik für Informatiker Wintersemester 2015/16 { ¬p(X), ¬p(f (a)), q(Y ) } [X|f (a)] [Y |b] { p(Y ) } { ¬p(g(b, X)), ¬q(b) } [Y |f (a)] ? [Y |g(b, a)] K1 = { ¬A, B } R K2 = { A } K3 = { C } U  [X|a] ? K4 = { ¬C, ¬B } U  K5 = { B } K6 = { ¬B } s + K7 = 2 Durch die vollständige Grundinstanziierung auf A = p(f (a)), B = q(b), C = p(g(b, a)), wird das Problem auf die Aussagenlogik reduziert. Prof. Dr. Dietmar Seipel 245 Logik für Informatiker Wintersemester 2015/16 Aus Effizienzgründen versucht man Substitutionen aber nur auszuführen, wenn es für den direkt nachfolgenden Resolutionsschritt erforderlich ist. { ¬p(X), ¬p(f (a)), q(Y ) } [Y |f (a)] [X|f (a)] ? { p(Y ) } { ¬p(f (a)), q(Y ) } [Y |g(b, X)] R { p(f (a)) } ? { p(g(b, X)) } { ¬p(g(b, X)), ¬q(b) } U  U  { q(Y ) } { ¬q(b) } [Y |b] ? ? { q(b) } { ¬q(b) } s Prof. Dr. Dietmar Seipel { ¬p(g(b, X)), ¬q(b) } 2 + 246 Logik für Informatiker Wintersemester 2015/16 Definition (Unifikator, allgemeinster Unifikator) Sei θ = [X1 |t1 ] . . . [Xn |tn ] eine Substitution. 1. Für eine endliche Literalmenge L = { L1 , . . . , Lk } setzen wir Lθ = { L1 θ, . . . , Lk θ }. 2. θ ist ein Unifikator von L, falls L1 θ = L2 θ = . . . = Lk θ. θ R θ0 ? γ 3. Ein Unifikator θ von L heißt allgemeinster Unifikator von L, falls für jeden Unifikator θ0 von L eine Substitution γ existiert mit θ0 = θγ, d.h. F θ0 = (F θ)γ für alle Formeln F . Prof. Dr. Dietmar Seipel 247 Logik für Informatiker Wintersemester 2015/16 Beispiel (Allgemeinster Unifikator) 1. θ ist ein allgemeinster Unifikator für die Literalmenge L = { p(X), p(f (a)) }. θ0 ist ein weiterer Unifikator, und es gilt θ0 = θγ. θ = [X|f (a)] R θ0 = [X|f (a)] [Y |b] γ = [Y |b] ? Prof. Dr. Dietmar Seipel 248 Logik für Informatiker Wintersemester 2015/16 2. θ ist ein allgemeinster Unifikator für die Literalmenge L = { p(Y ), p(g(b, X)) }. θ0 ist ein weiterer Unifikator, und es gilt θ0 = θγ. θ = [Y |g(b, X)] R θ0 = [Y |g(b, a)] [X|a] γ = [X|a] ? Prof. Dr. Dietmar Seipel 249 Logik für Informatiker Wintersemester 2015/16 Allgemeinste Unifikatoren sind i.a. nicht eindeutig: L = { p(X), p(Y ) } hat z.B. die beiden folgenden allgemeinsten Unifikatoren: θ1 = [X|Y ], θ2 = [Y |X]. Es gilt θ1 θ2 = θ2 und θ2 θ1 = θ1 . Der folgende weitere Unifikator θ3 = [X|Z][Y |Z] ist allerdings kein allgemeinster Unifikator. Es gilt θ1 [Y |Z] = θ3 und θ2 [X|Z] = θ3 . Prof. Dr. Dietmar Seipel 250 Logik für Informatiker Wintersemester 2015/16 Die Substitutionen bilden keine Gruppe. Es gibt ein neutrales Element [ ]. Aber für θ3 = [X|Z][Y |Z] gibt es z.B. kein Rechts–Inverses γ3 mit θ3 γ3 = [ ]. Man kann die Anwendung von θ3 nicht rückgängig machen, da man für ein Z nicht weiß, ob es von einem X oder einem Y herrührt. Ebenso gibt es für θ4 = [X|a] kein Rechts–Inverses, da man die Konstante a nicht auf eine Variable X abbilden kann. Auch für θ1 und θ2 gibt es keine Rechts–Inverse. Deswegen sind θ1 θ2 = θ2 und θ2 θ1 = θ1 möglich. Interessanterweise gilt hier außerdem θ1 θ1 = θ1 und θ2 θ2 = θ2 (Idempotenz). Prof. Dr. Dietmar Seipel 251 Logik für Informatiker Wintersemester 2015/16 Unifikationssatz (J.A. Robinson) Jede unifizierbare Menge von Literalen besitzt auch einen allgemeinsten Unifikator. Wir interessieren uns hauptsächlich für denjenigen allgemeinsten Unifikator, der durch den folgenden Algorithmus bestimmt wird. Unifikationsalgorithmus Eingabe: eine endliche, nicht–leere Literalmenge (Literalfolge) L θ = [ ]; ([ ] ist die leere Substitution, d.h. die identische Abbildung) while |Lθ| > 1 do begin durchsuche die Literale in Lθ von links nach rechts, bis die erste Position gefunden ist, wo sich mindestens zwei Literale L1 und L2 unterscheiden (Prädikaten– oder Argument–Position); Prof. Dr. Dietmar Seipel 252 Logik für Informatiker Wintersemester 2015/16 if keines der beiden Zeichen an den gefundenen Positionen ist eine Variable then stoppe mit der Ausgabe “nicht unifizierbar” else begin sei X die an der einen Position gefundene Variable und t der Term an der anderen Position; if X kommt in t vor (“Occurs Check”) then stoppe mit der Ausgabe “nicht unifizierbar” else θ = θ [X|t]; end; end; Ausgabe: θ ist ein allgemeinster Unifikator von L Prof. Dr. Dietmar Seipel 253 Logik für Informatiker Wintersemester 2015/16 Beispiel (Unifikationsalgorithmus) 1. Für die Literalmenge L = { p(X), p(f (a)), p(Y ) } sind die Prädikatenpositionen alle gleich p. ? ? ? L = { p(|{z} X ), p(f (a)), p(|{z} Y )} |{z} 6 6 6 Die ersten Unterschiede liegen in den Argumenten. Also setzen wir θ1 = [X|f (a)] und erhalten Lθ1 = { p(f (a)), p(Y ) }, da die ersten beiden Atome zusammenfallen. Mittels θ2 = [Y |f (a)] erhalten wir θ = θ1 θ2 = [X|f (a)][Y |f (a)] und Lθ = { p(f (a)) }. Wegen |Lθ| = 1 ist θ ein allgemeinster Unifikator. Prof. Dr. Dietmar Seipel 254 Logik für Informatiker Wintersemester 2015/16 2. Für die Literalmenge L = { L1 , L2 }, mit L1 = p(f (Z, g(a, Y )), h(Z)), L2 = p(f (f (U, V ), W ), h(f (a, b))), sind die ersten unterschiedlichen Positionen X = Z und t = f (U, V ). Somit erhalten wir θ1 = [Z|f (U, V )]. Für Lθ1 = { L1 θ1 , L2 θ1 }, mit L1 θ1 = p(f (f (U, V ), g(a, Y )), h(f (U, V ))), L2 θ1 = L2 , sind die ersten unterschiedlichen Positionen X = W und t = g(a, Y ). Somit erhalten wir θ2 = [W |g(a, Y )]. Prof. Dr. Dietmar Seipel 255 Logik für Informatiker Wintersemester 2015/16 Für Lθ1 θ2 = { L1 θ1 θ2 , L2 θ1 θ2 }, mit L1 θ1 θ2 = p(f (f (U, V ), g(a, Y )), h(f (U, V ))) und L2 θ1 θ2 = p(f (f (U, V ), g(a, Y )), h(f (a, b))), sind die ersten unterschiedlichen Positionen X = U und t = a. Somit erhalten wir θ3 = [U |a]. Abschließend erhalten wir noch θ4 = [V |b]. Insgesamt erhalten wir die Substitution θ = θ1 θ2 θ3 θ4 = [Z|f (U, V )][W |g(a, Y )][U |a][V |b] = [Z|f (a, b)][W |g(a, Y )][U |a][V |b], und L1 θ = p(f (f (a, b), g(a, Y )), h(f (a, b))) = L2 θ. Prof. Dr. Dietmar Seipel 256 Logik für Informatiker Wintersemester 2015/16 3. Die Literalmenge L = { p, q } ist nicht unifizierbar, da die Prädikatensymbole nicht übereinstimmen. 4. Die Literalmenge L = { p(a), p(b) } ist nicht unifizierbar, da die Argumente unterschiedliche Konstanten sind. 5. Die Literalmenge L = { p(f (X)), p(g(X)) } ist nicht unifizierbar, da die Funktionssymbole f und g nicht übereinstimmen. 6. Die Literalmenge L = { p(X), p(f (X)) } ist ebenfalls nicht unifizierbar, denn der Occurs Check stellt fest, daß der Term t = f (X) die Variable X enthält. Wenn man X mittels θ = [X|t0 ] durch einen Term t0 ersetzt, etwa durch t0 = t = f (X), dann enthält p(X)θ = p(t0 ) immer ein Auftreten des Funktionssymbols f weniger als p(f (X))θ = p(f (t0 )). Prof. Dr. Dietmar Seipel 257 Logik für Informatiker Wintersemester 2015/16 Occurs Check In P ROLOG wird der Occurs Check aus Effizienzgründen meist weggelassen, da der auf X zu testende Term t sehr groß sein kann. ?- X = f(X). X = f(**). • Das Ergebnis der Unifikation von X und f (X) ist in S WI–P ROLOG die Substitution [X|f (**)]. • Wie bei Dauerschleifen in herkömmlichen Programmiersprachen wie JAVA, geht man aber davon aus, daß ein Programmierer in der Praxis diese fehlerhaften Unifikationen vermeidet. • Aus rein theoretischer Sicht könnte man über unendlichen Termstrukturen als Ergebnis die Substitution [X|f (f (f (...)))] angeben, die X durch einen unendlich tief verschachtelten Term ersetzt. Prof. Dr. Dietmar Seipel 258 Logik für Informatiker Wintersemester 2015/16 Definition (Prädikatenlogische Resolution) Seien K1 und K2 prädikatenlogische Klauseln. 1. Seien θ1 und θ2 Substitutionen, welche die Variablen von K1 und K2 so umbenennen, daß K1 θ1 und K2 θ2 keine gemeinsamen Variablen mehr enthalten – wir nennen sie dann variablendisjunkt. 2. Für ein Atom A setzen wir A = ¬A und ¬A = A. 3. Es gebe nun Literale L1 , . . . , Lm ∈ K1 θ1 und L01 , . . . , L0n ∈ K2 θ2 , mit m ≥ 1 und n ≥ 1, so daß K1 K2 L = { L , . . . , L , L0 , . . . , L0 } 1 m 1 n unifizierbar ist mit einem allgemeinsten Unifikator θ. 4. Dann ist die folgende prädikatenlogische Klausel K eine prädikatenlogische Resolvente von K1 und K2 : U  K K = ((K1 θ1 \{ L1 , . . . , Lm }) ∪ (K2 θ2 \{ L01 , . . . , L0m }))θ. Prof. Dr. Dietmar Seipel 259 Logik für Informatiker Wintersemester 2015/16 Alternative, abstraktere Formulierung • 1. und 2. wie oben. • Für eine Literalmenge L setzen wird L = { L | L ∈ L }. • Es gebe nun nicht–leere Literalmengen L1 ⊆ K1 θ1 , L2 ⊆ K2 θ2 , so daß L1 ∪ L2 unifizierbar ist mit einem allgemeinsten Unifikator θ. • Dann ist die prädikatenlogische Klausel K1 K2 K = ((K1 θ1 \ L1 ) ∪ (K2 θ2 \ L2 ))θ eine prädikatenlogische Resolvente von K1 und K2 . Prof. Dr. Dietmar Seipel U  K 260 Logik für Informatiker Wintersemester 2015/16 Beispiel (Prädikatenlogische Resolution) Da die Klauselmenge { K1 , K2 } für die Formel ∀X (p(X) ∧ ¬p(f (X))) ≡ (∀X p(X)) ∧ (∀X ¬p(f (X))) steht, können wir K1 und K2 variablendisjunkt machen. K1 = { p(X) } K2 = { ¬p(f (X)) } ? K10 = { p(X) } ? K20 = { ¬p(f (U )) } j  K=2 Wir setzen K10 = K1 , d.h. θ1 = [ ], und K20 = K2 θ2 , mit θ2 = [X|U ]. Dann ist θ = [X|f (U )] ein allgemeinster Unifikator für L = { p(X), p(f (U )) }, und wir erhalten die Resolvente K = 2 = ∅. Prof. Dr. Dietmar Seipel 261 Logik für Informatiker Wintersemester 2015/16 Beispiel (Prädikatenlogische Resolution) K1 = { p(f (X)), ¬q(Z), p(Z) } K2 = { ¬p(X), r(g(X), a) } ^  K = { ¬q(f (X)), r(g(f (X)), a) } Wir setzen θ1 = [ ], θ2 = [X|U ], θ = [U |f (X)] [Z|f (X)]. θ ist ein allgemeinster Unifikator für L = { p(f (X)), p(Z), p(U ) }. Prof. Dr. Dietmar Seipel 262 Logik für Informatiker Wintersemester 2015/16 Die Resolutionsmengen werden analog zur Aussagenlogik definiert. Definition (Resolutionsmengen) Sei M eine prädikatenlogische Klauselmenge. Res(M ) = M ∪ { K | K ist eine prädikatenlogische Resolvente zweier Klauseln K1 , K2 ∈ M }. Ferner definieren wir: Res 0 (M ) = M, Res n+1 (M ) = Res(Res n (M )), für n ≥ 0, ∪ ∗ Res (M ) = n≥0 Res n (M ). Es gibt meist sehr viele Resolventen, die wir nicht alle aufzählen können. Außerdem ist das Variablendisjunkt–Machen nicht eindeutig. Prof. Dr. Dietmar Seipel 263 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolutionsmengen) Für die Klauselmenge M = { F1 , F2 , F3 } mit F1 = ¬p(X) ∨ ¬p(f (a)) ∨ q(Y ), F2 = p(Y ), F3 = ¬p(g(b, X)) ∨ ¬q(b), zur Formel F = ∀X ∀ Y (F1 ∧ F2 ∧ F3 ) erhalten wir folgendes: • Je nachdem ob wir bei der Resolution von F1 und F2 beide p–Literale aus F1 gegen F2 = p(Y ) resolvieren oder jeweils nur eines, erhalten wir drei unterschiedliche Resolventen: q(Y ), ¬p(f (a)) ∨ q(Y ), ¬p(X) ∨ q(Y ). • Die Resolution von F2 und F3 über die p–Literale ergibt ¬q(b). Prof. Dr. Dietmar Seipel 264 Logik für Informatiker Wintersemester 2015/16 • Die Resolution von F1 und F3 über die q–Literale ergibt ¬p(X) ∨ ¬p(f (a)) ∨ ¬p(g(b, X 0 )). Um die Klauseln variablendisjunkt zu machen, haben X in F3 durch X 0 ersetzt. Diese Substitution ist natürlich nicht eindeutig. Wir erhalten also die folgenden Resolutionsmengen: Res 0 (M ) = M, Res 1 (M ) = M ∪ { ¬p(f (a)) ∨ q(Y ), ¬p(X) ∨ q(Y ), q(Y ), ¬q(b), ¬p(X) ∨ ¬p(f (a)) ∨ ¬p(g(b, X 0 )) }, Res 2 (M ) = Res 1 (M ) ∪ { 2, . . . }. Res 2 (M ) enthält hier – neben der leeren Klausel 2 – weitere Resolventen, die wir nicht alle aufzählen wollen. Prof. Dr. Dietmar Seipel 265 Logik für Informatiker Wintersemester 2015/16 Resolutionssatz der Prädikatenlogik Sei F eine prädikatenlogische Formel in Skolemform ohne freie Variablen und mit (quantorenfreier) Matrix in KNF, und sei M die zugehörige Klauselmenge. F ist genau dann unerfüllbar, wenn 2 ∈ Res ∗ (M ). Eine Resolutionsableitung verwendet immer nur endlich viele Klauseln. Deswegen ist der Kompaktheitssatz entscheident, der besagt, daß eine unerfüllbare Formelmenge bereits eine endliche unerfüllbare Teilmenge haben muß. Der Beweis des Resolutionssatzes erfolgt durch Lifting des aussagenlogischen Satzes. Prof. Dr. Dietmar Seipel 266 Logik für Informatiker Wintersemester 2015/16 Lifting–Lemma Seien K1 und K2 zwei prädikatenlogische Klauseln, und seien K10 und K20 beliebige Grundinstanzen von K1 bzw. K2 . • Sei K 0 eine Resolvente von K10 und K20 im aussagenlogischen Sinn. • Dann gibt es eine prädikatenlogische Resolvente K von K1 und K2 , so daß K 0 eine Grundinstanz von K ist. K1 K2 j K  ? K10 ? K20 j ?  K0 Prof. Dr. Dietmar Seipel 267 Logik für Informatiker Wintersemester 2015/16 Beispiel (Lifting–Lemma) { p(f (X)), ¬q(Z), p(Z) } { ¬p(X), r(g(X), a) } j θ1 = [X|b] [Z|f (b)]  θ2 = [X|f (b)] { ¬q(f (X)), r(g(f (X)), a) ? ? { p(f (b)), ¬q(f (b)), p(f (b)) } { ¬p(f (b)), r(g(f (b)), a) } j ?  { ¬q(f (b)), r(g(f (b)), a) Prof. Dr. Dietmar Seipel 268 Logik für Informatiker Wintersemester 2015/16 Beispiel (Resolution mit Gruppenaxiomen) Wir schreiben p(X, Y, Z) anstelle von X ◦ Y = Z (Produkt). (1) Abgeschlossenheit: ∀X∀Y ∃Z p(X, Y, Z). (2) Assoziativität: ∀U ∀V ∀W ∀X∀Y ∀Z ( p(X, Y, U ) ∧ p(Y, Z, V ) → (p(X, V, W ) ↔ p(U, Z, W ) ). äquivalent: ∀ . . . ( X ◦ (Y ◦ Z) = W ↔ (X ◦ Y ) ◦ Z = W ). (3) Existenz eines links–neutralen Elements (X) und Existenz von Links–Inversen (Z): ∃X ∀Y (p(X, Y, Y ) ∧ ∃Z p(Z, Y, X)). äquivalent: ∃X ∀Y ((X ◦ Y = Y ) ∧ ∃Z (Z ◦ Y = X)). Prof. Dr. Dietmar Seipel 269 Logik für Informatiker Wintersemester 2015/16 (4) Existenz von Rechts–Inversen: ∃X ∀Y (p(X, Y, Y ) ∧ ∃Z p(Y, Z, X)). äquivalent: ∃X ∀Y ((X ◦ Y = Y ) ∧ ∃Z (Y ◦ Z = X)). Es stellt sich heraus, daß man die Existenz von Rechts–Inversen nicht separat in einem Axiom fordern muß, da sie bereits aus den anderen Gruppenaxiomen (1), (2) und (3) folgt. Um dies zu zeigen, betrachten wir die Negation von (4). Diese ist äquivalent zur BPF ∀X ∃Y ∀Z (¬p(X, Y, Y ) ∨ ¬p(Y, Z, X)). • Da Z nicht in der Teilformel p(X, Y, Y ) vorkommt, kann man in (4) den Existenzquantor ∃Z nach vorne ziehen. • Die Negation vertauscht All– und Existenzquantoren, und sie verwandelt nach De Morgan eine Konjunktion in eine Disjunktion. Prof. Dr. Dietmar Seipel 270 Logik für Informatiker Wintersemester 2015/16 Die Formel zur Assoziativität wird z.B. schematisch wie folgt umgeformt: ∀... ∀... ∀... ∀... ( α → (A ↔ B) ) ≡ ( α → ((A ∧ B) ∨ (¬A ∧ ¬B)) ) ≡ ( α → ((A ∨ ¬B) ∧ (¬A ∨ B)) ) ≡ ( (α ∧ B → A) ∧ (α ∧ A → B) ). Es wurde zweimal verwendet, daß ein negiertes Literal ¬B im Kopf einer Regel als B in den Rumpf verschoben werden kann: ∀ . . . ( α → (A ∨ ¬B) ) ≡ ∀ . . . ( ¬ α ∨ A ∨ ¬B ) ≡ ∀ . . . ( α ∧ B → A ). Wir erhalten also aus (2) zwei Implikationen. Die Folgerung { (1), (2), (3) } |= (4) gilt genau dann, wenn { (1), (2), (3), ¬(4) } unerfüllbar ist. Prof. Dr. Dietmar Seipel 271 Logik für Informatiker Wintersemester 2015/16 Klauselform von (1) ∧ (2) ∧ (3) ∧ ¬(4) mit Skolemfunktionen m, e, i, j: (1) Abgeschlossenheit: (a) { p(X, Y, m(X, Y )) }. (2) Assoziativität: (b) { ¬p(X, Y, U ), ¬p(Y, Z, V ), ¬p(X, V, W ), p(U, Z, W ) }, (c) { ¬p(X, Y, U ), ¬p(Y, Z, V ), ¬p(U, Z, W ), p(X, V, W ) }. (3) Existenz eines links–neutralen Elements e und Existenz von Links–Inversen i(Y ) für Gruppenelemente Y : (d) { p(e, Y, Y ) }, (e) { p(i(Y ), Y, e) }. (4) Negation der Existenz von Rechts–Inversen: (f) { ¬p(X, j(X), j(X)), ¬p(j(X), Z, X) }. Prof. Dr. Dietmar Seipel 272 Logik für Informatiker Wintersemester 2015/16 Resolutionsherleitung der leeren Klausel (f ) { ¬p(X, j(X), j(X)), ¬p(j(X), Z, X) } | (d) { p(e, Y, Y ) } ↓ . { ¬p(j(e), Z, e) } | (b) { ¬p(X, Y, U ), ¬p(Y, Z, V ), ¬p(X, V, W ), p(U, Z, W ) } ↓ . { ¬p(X, Y, j(e)), ¬p(Y, Z, V ), ¬p(X, V, e) } | (e) { p(i(Y ), Y, e) } ↓ . { ¬p(i(V ), W, j(e)), ¬p(W, Z, V ) } | (d) { p(e, Y, Y ) } ↓ . { ¬p(i(V ), e, j(e)) } Prof. Dr. Dietmar Seipel 273 Logik für Informatiker Wintersemester 2015/16 | (c) { ¬p(X, Y, U ), ¬p(Y, Z, V ), ¬p(U, Z, W ), p(X, V, W ) } ↓ . { ¬p(i(V ), Y, U ), ¬p(Y, Z, e), ¬p(U, Z, j(e)) } | (d) { p(e, Y, Y ) } ↓ . { ¬p(i(V ), Y, e), ¬p(Y, j(e), e) } | (e) { p(i(Y ), Y, e) } ↓ . { ¬p(i(V ), i(j(e)), e) } | (e) { p(i(Y ), Y, e) } ↓ . 2 Also folgt das vierte Gruppenaxiom aus den ersten dreien: (1) ∧ (2) ∧ (3) |= (4). Prof. Dr. Dietmar Seipel 274 Logik für Informatiker Wintersemester 2015/16 Da wir in diesem Beispiel ausschließlich Horn–Klauseln vorliegen haben, können wir die Resolutionsherleitung auch in Implikationsnotation schreiben: (f ) ← p(X, j(X), j(X)) ∧ p(j(X), Z, X) | (d) p(e, Y, Y ) ↓ . ← p(j(e), Z, e) | (b) p(U, Z, W ) ← p(X, Y, U ) ∧ p(Y, Z, V ) ∧ p(X, V, W ) ↓ . ← p(X, Y, j(e)) ∧ p(Y, Z, V ) ∧ p(X, V, e) | (e) p(i(Y ), Y, e) ↓ . ← p(i(V ), W, j(e)) ∧ p(W, Z, V ) | (d) p(e, Y, Y ) ↓ . ← p(i(V ), e, j(e)) Prof. Dr. Dietmar Seipel 275 Logik für Informatiker Wintersemester 2015/16 | (c) p(X, V, W ) ← p(X, Y, U ) ∧ p(Y, Z, V ) ∧ p(U, Z, W ) ↓ . ← p(i(V ), Y, U ) ∧ p(Y, Z, e) ∧ p(U, Z, j(e)) | (d) p(e, Y, Y ) ↓ . ← p(i(V ), Y, e) ∧ p(Y, j(e), e) | (e) p(i(Y ), Y, e) ↓ . ← p(i(V ), i(j(e)), e) | (e) p(i(Y ), Y, e) ↓ . 2 Es handelt sich um eine lineare Herleitung von Goals. Bis auf den ersten Schritt wird immer zuerst das rechteste Atom des Goal–Rumpfes resolviert. Wenn man zuerst mit (b) und dann mit (d) resolvieren würde, dann wäre dies – wie bei der SLD–Resolution – immer der Fall. Prof. Dr. Dietmar Seipel 276 Logik für Informatiker Wintersemester 2015/16 Prädikatenlogik der zweiten Stufe (PL2) Die Prädikatenlogik ist zwar ausdrucksstärker als die Aussagenlogik. Aber trotzdem kann auch im Rahmen der Prädikatenlogik nicht jede mathematische Aussage formuliert werden. Wir erhalten eine noch größere Ausdrucksstärke, wenn wir zusätzlich Quantifizierungen über • Prädikaten– und • Funktionssymbolen erlauben. Beispiel (PL2) F = ∀p ∃f ∀X p(f (X)). Prof. Dr. Dietmar Seipel 277 Logik für Informatiker Wintersemester 2015/16 Exkurs: Induktionsaxiom der natürlichen Zahlen in PL2 Das Induktionsaxiom wurde ursprünglich in der PL2 formuliert: ∀p ( p(0) ∧ ∀N (N ∈ IN0 ∧ p(N ) → p(s(N ))) → ∀N (N ∈ IN0 → p(N )) ). Es verwendet ein 1–stelliges Funktionssymbol s zur Bezeichnung des Nachfolgers einer natürlichen Zahl, und es quantifiziert über ein 1–stelliges Prädikatensymbol p. Das Axiom besagt, daß jede induktive Teilmenge von IN0 – beschrieben durch das Prädikat p – gleich IN0 sein muß: • Falls p für die Zahl 0 gilt, und • falls für alle N ∈ IN0 aus p(N ) auch p(s(N )) folgt, d.h., wenn p für N gilt, dann gilt p auch für N + 1, • dann gilt p für alle N ∈ IN0 . Prof. Dr. Dietmar Seipel 278 Logik für Informatiker Wintersemester 2015/16 Peano–Axiome der natürlichen Zahlen (P1) ∀N ¬ (s(N ) ≡ 0), (P2) ∀N ∀M (s(N ) ≡ s(M ) → N ≡ M ), (P3) ∀p ( p(0) ∧ ∀N (p(N ) → p(s(N ))) → ∀N p(N ) ). (P3) ist eine verkürzte Version des Induktionsaxioms in der PL2. Zusätzlich muß das Gleichheitsprädikat ≡ geeignet axiomatisiert werden. Dann sind alle Modelle A der Gesamtformelmenge F isomorph. Z.B. gibt es das (eindeutige) Herbrand–Modell mit der Grundmenge HUF = { 0, s(0), s(s(0)), . . . } = { sn (0) | n ∈ IN0 }. Das Herbrand–Modell repräsentiert eine natürliche Zahl n ∈ IN als einen Term sn (0) mit n Auftreten des Funktionssymbols s. Wir setzen dazu s0 (0) = 0 und sn+1 (0) = s(sn (0)), für n ∈ IN0 . Prof. Dr. Dietmar Seipel 279 Logik für Informatiker Wintersemester 2015/16 Ein anderes Modell A, das von John von Neumann vorgeschlagen wurde, repräsentiert eine natürliche Zahl n ∈ IN als eine Menge. Dazu werden die Terme sn (0) aus HUF folgendermaßen interpretiert: 0A = ∅, s(t)A = tA ∪ {tA }. Wenn wir (sn (0))A = sn schreiben, dann erhalten wir: s0 = ∅, s1 = s0 ∪ { s0 } = ∅ ∪ { ∅ } = { ∅ } = { s0 }, s2 = s1 ∪ { s1 } = { ∅, { ∅ } } = { s0 , s1 }, sn+1 = sn ∪ { sn } = { s0 , s1 , . . . , sn }. Man kann dagegen zeigen, daß jede Axiomatisierung der natürlichen Zahlen als Peano–Struktur im Rahmen der PL1 Nicht–Standardmodelle aller unendlichen Kardinalitäten zuläßt. Prof. Dr. Dietmar Seipel 280 Logik für Informatiker Wintersemester 2015/16 Mathematische Theorien Eine Theorie ist eine Menge T von Formeln (möglicherweise beschränkt auf solche Formeln, die nur aus bestimmten vorgegebenen Bestandteilen – z.B. bestimmten Prädikaten– und Funktionssymbolen – aufgebaut ist), die gegenüber Folgerbarkeit abgeschlossen ist. D.h., falls { F1 , . . . , Fn } ⊆ T gilt und F eine Folgerung aus { F1 , . . . , Fn } ist, dann gilt auch F ∈T Die Formeln F ∈ T heißen auch Sätze der Theorie. Prof. Dr. Dietmar Seipel 281 Logik für Informatiker Prof. Dr. Dietmar Seipel Wintersemester 2015/16 282 Logik für Informatiker 2.6 Wintersemester 2015/16 Hyperresolution für Hornformeln Eine prädikatenlogische Klausel K = L1 ∨ . . . ∨ Ln ist eine Hornklausel, falls maximal ein Literal Li positiv ist – wie in der Aussagenlogik. Es gibt auch wieder drei interessante Spezialfälle; im folgenden seien A und B1 , . . . , Bm prädikatenlogische Atome: • Eine (definite) Regel ist eine Hornklausel K = A ∨ ¬B1 ∨ . . . ∨ ¬Bm mit genau einem positiven Literal. • Ein (definites) Fakt ist eine Regel K = A ohne negative Literale (m = 0). • Eine Goal (Ziel, Anfrage) ist eine Hornklausel K = ¬B1 ∨ . . . ∨ ¬Bm ohne positives Literal. Ein definites Logikprogramm ist eine Menge von definiten Regeln (bzw. Fakten) in Implikations–Notation. Prof. Dr. Dietmar Seipel 283 Logik für Informatiker Wintersemester 2015/16 In der Logikprogrammierung verwendet man – aufgrund der Regeln von De Morgan – für Hornklauseln folgende Implikations–Notation: Fakt: A, Regel: A ← B1 ∧ . . . ∧ Bm , m ≥ 0, Goal: ← B1 ∧ . . . ∧ Bm , m ≥ 0. Regeln und Fakten: • Das Atom A heißt Kopf einer Regel r = A ← β. • Die Konjunktion β = B1 ∧ . . . ∧ Bm ist der Rumpf der Regel r. Die Atome Bi , mit 1 ≤ i ≤ m, heißen Rumpfatome. • Falls m = 0 ist, so wird die Regel mit dem Fakt A gleichgesetzt. Goals werden bei der SLD–Resolution für Anfragen benutzt; in diesem Abschnitt zur Hyperresolution verwenden wir keine Goals. Prof. Dr. Dietmar Seipel 284 Logik für Informatiker Wintersemester 2015/16 DATALOG–Programme: verwendet in Deduktiven Datenbanken In der Aussagenlogik enthalten Hornformeln keine Variablensymbole. Als Erweiterung betrachten wir nun in der Prädikatenlogik Hornformeln, bei denen jedes Variablensymbol in mindestens einem Rumpfatom vorkommt. Solche Hornformeln nennen wir bereichsbeschränkt. Eine Menge von bereichsbeschränkten Hornformeln in Implikationsnotation nennen wir DATALOG–Programm. • Im strengen Sinne können DATALOG–Programme P auch keine Funktionssymbole enthalten. Dann ist das Herbrand–Universum HUP endlich, und es können nur endlich viele Atome abgeleitet werden. • In praktischen Anwendungen verwendet man aber oft die Erweiterung um Funktionssymbole namens DATALOGfun . Dann liegt es am Programmierer, Dauerschleifen bei der Ableitung zu vermeiden. Prof. Dr. Dietmar Seipel 285 Logik für Informatiker Wintersemester 2015/16 Beispiel (DATALOG–Programm) Die folgenden Regeln bilden ein DATALOG–Programm P zur Berechnung der Vorfahren (ancestor ) aufgrund der Eltern–Relation (parent): ancestor(X, Y ) ← parent(X, Y ), ancestor(X, Y ) ← parent(X, Z) ∧ ancestor(Z, Y ). Zugehörige Eltern–Fakten: parent(a, b), parent(b, c), parent(c, d). Jeder Elternteil ist ein Vorfahre (Regel 1), und jeder Vorfahre der Eltern ist ebenfalls ein Vorfahre (Regel 2). In P ROLOG sind auch Regeln sinnvoll, bei denen Variablensymbole nur im Kopf vorkommen – wie z.B. das Fakt zu hres_iteration/3 am Ende dieses Abschnittes. Prof. Dr. Dietmar Seipel 286 Logik für Informatiker Wintersemester 2015/16 Hyperresolution Die sukzessive, n–fache Anwendung der binären Resolution auf eine Regel A ← B1 ∧ . . . ∧ Bn und geeignete Fakten Ai nennt man Hyperresolution. Die Rumpfatome Bi werden sukzessive mit den Fakten Ai resolviert. A ∨ ¬B1 ∨ ¬B2 ∨ . . . ∨ ¬Bn θ1 (A ∨ (A ∨ ?9 ¬B2 ∨ . . . ∨ ¬Bn ) θ1 θ2 ..?9 . ?9 ¬Bn ) θ1 . . . θn−1 θn A1 A2 .. . An ?9 A θ1 . . . θ n Wir nennen das berechnete Fakt A θ1 . . . θn eine Hyperresolvente. Prof. Dr. Dietmar Seipel 287 Logik für Informatiker Wintersemester 2015/16 DATALOG–Fakten enthalten keine Variablensymbole. Deswegen muß man die Fakten Ai und die zwischendurch erhaltenen Regeln nicht variablendisjunkt machen. Es genügt Substitutionen θi zu finden, so daß (Bi θ1 . . . θi−1 ) θi = Ai . Wir bezeichen θ = θ1 . . . θn als die berechnete Substitution. Die berechnete Hyperresolvente Aθ ist dann automatisch auch ein Fakt ohne Variablensymbole, da ja alle Variablensymbole aus dem Regelkopf A in den Rumpfatomen Bi enthalten sind und somit von θ grundinstanziiert werden. Prof. Dr. Dietmar Seipel 288 Logik für Informatiker Wintersemester 2015/16 Beispiel (Hyperresolution) Für das DATALOG–Programm P mit den Regeln anc(X, Y ) ← par(X, Y ), anc(X, Y ) ← par(X, Z) ∧ anc(Z, Y ), und den Eltern–Fakten par(a, b), par(b, c), par(c, d), erhalten wir folgendes: 1. Die Fakten aus P werden mittels einer Hyperresolution durch n = 0 Anwendungen der binären Resolution abgeleitet. Prof. Dr. Dietmar Seipel 289 Logik für Informatiker Wintersemester 2015/16 2. Dann kann aus dem Fakt par (b, c) und der ersten Regel ein Fakt anc(b, c) abgeleitet werden: anc(X, Y ) ← par (X, Y ) θ1 = [X|b] [Y |c] par (b, c) ?) anc(b, c) Die berechnete Substitution ist θ = θ1 = [X|b] [Y |c], und es wird anc(X, Y )θ = anc(b, c) abgeleitet. Ebenso werden die Fakten anc(a, b) und anc(c, d) abgeleitet. Prof. Dr. Dietmar Seipel 290 Logik für Informatiker Wintersemester 2015/16 3. Danach kann aus den Fakten par (a, b) und anc(b, c) und der zweiten Regel das Fakt anc(a, c) abgeleitet werden: anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ) θ1 = [X|a] [Z|b] ?9 anc(a, Y ) ← anc(b, Y ) θ2 = [Y |c] par (a, b) anc(b, c) ?9 anc(a, c) Die berechnete Substitution ist θ = θ1 θ2 = [X|a] [Z|b] [Y |c], und es wird anc(X, Y )θ = anc(a, c) abgeleitet. Prof. Dr. Dietmar Seipel 291 Logik für Informatiker Wintersemester 2015/16 Ebenso kann das Fakt anc(b, d) abgeleitet werden. 4. Zuletzt kann aus dem Fakt anc(b, d) das Fakt anc(a, d) abgeleitet werden: anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ) θ1 = [X|a] [Z|b] ?9 anc(a, Y ) ← anc(b, Y ) θ2 = [Y |d] par (a, b) anc(b, d) ?9 anc(a, d) Insgesamt haben wir also die folgenden anc–Fakten abgeleitet: anc(a, b), anc(b, c), anc(c, d), anc(a, c), anc(b, d), anc(a, d). Prof. Dr. Dietmar Seipel 292 Logik für Informatiker Wintersemester 2015/16 In Iteration n ≥ 2 werden also die anc–Fakten zu den Pfaden der Länge n − 1 in der Vorfahrenhierarchie abgeleitet: dY  6 c I 6 b 6 a Die durchgezogenen Linien zeigen die par –Fakten und die entsprechenden anc–Fakten zu den Pfaden der Länge 1. Die gestrichelten Linien zeigen die anc–Fakten zu den Pfaden der Länge 2 und 3. Das Fakt anc(a, d ) zur Länge 3 wird in Iteration 4 aus par (a, b) und anc(b, d ) abgeleitet. Prof. Dr. Dietmar Seipel 293 Logik für Informatiker Wintersemester 2015/16 Hyperresolutionsmengen Sei P ein DATALOG–Programm und I eine Herbrand–Interpretation. 1. Hres(P, I) ist die Menge aller Hyperresolventen, die man aus den Regeln aus P und den Fakten aus I herleiten kann: 2. Also besteht Hres(P, I) aus allen Grundatomen Aθ, so daß es eine Regel A ← B1 ∧ . . . ∧ Bn ∈ P gibt, mit Bi θ ∈ I, für alle 1 ≤ i ≤ n. 3. Man könnte auch sagen: Hres(P, I) besteht aus allen Grundatomen A, so daß es eine Grundinstanz A ← B1 ∧ . . . ∧ Bn einer Regel aus P gibt, mit Bi ∈ I, für alle 1 ≤ i ≤ n. 4. Wenn gnd (P ) die Menge dieser Grundinstanzen ist, dann gilt: Hres(P, I) = { A | A ← β ∈ gnd (P ) ∧ I |= β }. Für ein festes P , schreibt man anstelle von Hres(P, I) oft auch Hres P (I). Prof. Dr. Dietmar Seipel 294 Logik für Informatiker Wintersemester 2015/16 Man kann auch wieder Potenzen Hres n (P ) bilden: Hres 0 (P ) = ∅, Hres n+1 (P ) = Hres(P, Hres n (P )), ∪ ∗ Hres (P ) = n∈IN+ Hres n (P ). Offensichtlich gilt auch hier die Monotonie–Eigenschaft: P ⊆ P 0 ∧ I ⊆ I 0 ⇒ Hres(P, I) ⊆ Hres(P 0 , I 0 ). Also kann man wieder durch vollständige Induktion folgendes zeigen: Hres n (P ) ⊆ Hres n+1 (P ). Wir schreiben Fakten in den Hyperresolutionsmengen als Atome. Prof. Dr. Dietmar Seipel 295 Logik für Informatiker Wintersemester 2015/16 Beispiel (Hyperresolutionsmengen) Für das DATALOG–Programm P mit den Regeln anc(X, Y ) ← par(X, Y ), anc(X, Y ) ← par(X, Z) ∧ anc(Z, Y ), und den Eltern–Fakten par(a, b), par(b, c), par(c, d), erhalten wir folgendes: Hres 0 (P ) = ∅, Hres 1 (P ) = { par (a, b), par (b, c), par (c, d) }, Hres 2 (P ) = Hres 1 (P ) ∪ { anc(a, b), anc(b, c), anc(c, d) }, Hres 3 (P ) = Hres 2 (P ) ∪ { anc(a, c), anc(b, d) }, Hres 4 (P ) = Hres 3 (P ) ∪ { anc(a, d) }. Prof. Dr. Dietmar Seipel 296 Logik für Informatiker Wintersemester 2015/16 Man kann die Definition der Hyperresolutionsmenge Hres(P, I) auf ein beliebiges definites Logikprogramm P anwenden, Hres(P, I) = { A | A ← β ∈ gnd (P ) ∧ I |= β }, selbst wenn P nicht bereichsbeschränkt ist und Funktionssymbole enthält. • Wenn ein Regelkopf Variablensymbole enthält, die nicht im Regelrumpf vorkommen, dann kann man diese in den zur Ableitung benutzten Grundinstanzen A ← β ∈ gnd (P ) mit I |= β unabhängig von I mit allen Termen des Herbranduniversums HUP instanziieren. • Dann kann man manchmal unabhängig von I sehr viele Atome A ableiten. • Wenn HUP unendlich ist, dann kann das nicht mehr berechnet werden. In diesem Fall müßte man alternativ Nicht–Grundatome ableiten. Prof. Dr. Dietmar Seipel 297 Logik für Informatiker Wintersemester 2015/16 Für das definite Logikprogramm P mit den Regeln anc(X, X), anc(X, Y ) ← par(X, Z) ∧ anc(Z, Y ), und den Eltern–Fakten par(a, b), par(b, c), par(c, d), gibt es sehr viele Grundinstanzen des Faktes anc(X, X), die man zur Ableitung benutzen kann, nämlich eines für jedes Element des Herbranduniversums HUP = { a, b, c, d } : anc(a, a), anc(b, b), anc(c, c), anc(d, d). Diese sind unabhängig von I, da ihr leerer Rumpf β immer gilt. Wenn das Herbranduniversum HUP noch größer wäre, dann wären das entsprechend mehr. Prof. Dr. Dietmar Seipel 298 Logik für Informatiker Wintersemester 2015/16 Dagegen kann man für I = { par (a, b), par (b, c), par (c, d), anc(a, b), anc(b, c), anc(c, d) } nur die folgenden Grundinstanzen der zweiten Regel zur Ableitung benutzen: anc(a, c) ← par(a, b) ∧ anc(b, c), anc(b, d) ← par(b, c) ∧ anc(c, d). Diese hängen von I ab. Prof. Dr. Dietmar Seipel 299 Logik für Informatiker Wintersemester 2015/16 Theorem 2.1 (Charakterisierung von Herbrand–Modellen) Sei P ein definites Logikprogramm. Eine Herbrand–Interpretation I von P ist ein Herbrand–Modell von P , g.d.w. gilt Hres(P, I) ⊆ I. Beweis: “⇐” Sei I eine Herbrand–Interpretation von P mit Hres(P, I) ⊆ I. Sei A ← β eine Grundinstanz einer Regel aus P mit I |= β. Dann gilt A ∈ Hres(P, I), und wegen Hres(P, I) ⊆ I folgt A ∈ I. Also ist I ein Herbrand–Modell von P . “⇒” Sei I ein Herbrand–Modell von P . Für jedes A ∈ Hres(P, I) gibt es eine Grundinstanz einer Regel A ← β aus P mit I |= β. Da I ein Herbrand–Modell von P ist, folgt sofort A ∈ I. Also gilt Hres(P, I) ⊆ I. Prof. Dr. Dietmar Seipel 300 Logik für Informatiker Wintersemester 2015/16 Minimales Herbrand–Modell MP Für ein definites Logikprogramm P kann man folgendes zeigen: 1. Jedes Herbrand–Modell muß MP = Hres ∗ (P ) enthalten. 2. MP ist ein Herbrand–Modell, denn Hres(P, MP ) ⊆ MP . Also ist MP das eindeutige minimale Herbrand–Modell von P . Für DATALOG–Programme ist MP endlich, und es kann effizient berechnet werden. Im allgemeinen kann MP unendlich sein. Prof. Dr. Dietmar Seipel 301 Logik für Informatiker Wintersemester 2015/16 2.7 SLD–Resolution Die SLD–Resolution (Linear Resolution with Selection Function for Definite Clauses) wurde ursprünglich zum automatischen Theorembeweisen für allgemeine Klauseln verwendet, vgl. J.A. Robinson (1965). • Sei s eine Selektionsfunktion, die aus jedem Goal ein Atom auswählt. • Sei G ein Goal und r = A ← β eine definite Regel: G = ← β1 ∧ B ∧ β2 . Dabei seien β1 und β2 Konjunktionen von Atomen und s(G) = B das von s selektierte Atom. Falls M GU(A, B) = θ existiert, dann heißt G0 = ← ( β1 ∧ β ∧ β2 ) θ eine Resolvente von G und r bezüglich s. Falls r ein Fakt ist (d.h. β ist leer), dann ist G0 um ein Atom kürzer als G. Prof. Dr. Dietmar Seipel 302 Logik für Informatiker Wintersemester 2015/16 Die SLD–Resolution ergibt sich aus der binären Resolution der PL1. Bekanntlich ist ein Goal G = ← β1 ∧ B ∧ β2 äquivalent zu einer Disjunktion α1 = ¬β1 ∨ ¬B ∨ ¬β2 , und eine Regel r = A ← β ist äquivalent zu einer Disjunktion α2 = A ∨ ¬β. Durch die bekannte binäre Resolution der PL1 erhält man mittels eines allgemeinsten Unifikators θ von A und B eine neue Disjunktion α = (¬β1 ∨ ¬β ∨ ¬β2 )θ, die wieder einem Goal G0 = ← ( β1 ∧ β ∧ β2 ) θ entspricht. Prof. Dr. Dietmar Seipel 303 Logik für Informatiker Wintersemester 2015/16 SLD–Widerlegung Sei P ein definites Logikprogramm und Q eine Anfrage. • Eine SLD–Widerlegung von h P, Q i ist eine endliche Folge h Gi i0≤i≤n , wobei G0 = Q und Gn = 2, von Goals zusammen mit einer Folge h ri i1≤i≤n von Regeln und einer Folge h θi i1≤i≤n von Substitutionen, wobei für alle 1 ≤ i ≤ n gilt: – ri ist eine Variante einer Regel aus P , – Gi ist eine Resolvente aus Gi−1 und ri bezüglich s, und – θi ist der benutzte allgemeinste Unifikator. θ = θ1 · θ2 · . . . · θn heißt Antwortsubstitution. • Die SLD–Widerlegung einer atomaren Anfrage Q = ← A ist äquivalent zu dem Beweis, daß die Instanz Aθ, welche man Antwort nennt, aus P abgeleitet werden kann. Prof. Dr. Dietmar Seipel 304 Logik für Informatiker Wintersemester 2015/16 • Ein SLD–Widerlegungsbaum veranschaulicht eine SLD–Widerlegung: G0 r1 ? r2 ? r3 G1 G2 ? G3 .. . .. . rn ? Gn = 2 Man kann eine SLD–Widerlegung natürlich auch einfach als eine r1 r2 r3 rn lineare Kette G0 −→ G1 −→ G2 −→ . . . −→ Gn = 2 repräsentieren, wenn man die Kanten mit den verwendeten Regeln markiert. Prof. Dr. Dietmar Seipel 305 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Resolution) Für das DATALOG–Programm P = { r, f1 , f2 }, mit r = p ← a ∧ b, f1 = a, f2 = b, erhalten wir mit der Selektionsfunktion sl , welche stets das linkeste (erste) Atom eines Goals selektiert, eine SLD–Widerlegung zum Goal Q = ← p. ←p ? ←a∧b ? ←b ? 2 Prof. Dr. Dietmar Seipel r f1 f2 306 Logik für Informatiker Wintersemester 2015/16 In Klauselschreibweise r = p ∨ ¬a ∨ ¬b, f1 = a, f2 = b, erhalten wir folgende Folge von binären Resolutionen zum Goal Q = ¬p : ¬p r ? ¬a ∨ ¬b f1 ? ¬b f2 ? 2 Prof. Dr. Dietmar Seipel 307 Logik für Informatiker Wintersemester 2015/16 Nicht–Lineare Resolution Für die inkonsistente Klauselmenge F = { p ∨ q, p ∨ ¬q, ¬p ∨ q, ¬p ∨ ¬q } gibt es keine lineare Widerlegung, aber folgende Resolutionsableitung: p∨q p ∨ ¬q ¬p ∨ q Rp ¬p ∨ ¬q R¬p s 2 + Diese Klauselmenge ist keine Hornklauselmenge. Für eine inkonsistente Hornklauselmenge gibt es immer eine lineare Ableitung der leeren Klausel, die mit einer Integritätsbedingung startet. Prof. Dr. Dietmar Seipel 308 Logik für Informatiker Wintersemester 2015/16 Neue Notation für Substitutionen Wir schreiben eine Substitution [X1 |t1 , . . . Xn |tn ], bei der alle Ersetzungen parallel angewendet werden, als Menge θ = { X1 7→ t1 , . . . , Xn 7→ tn }. θ definiert eine Abbildung von einer Struktur t auf eine neue Struktur tθ: • Für eine Konstante t gilt tθ = t. • Für eine Variable t = X gilt: falls es eine Ersetzung Xi 7→ ti ∈ θ gibt, mit X = Xi , so erhalten wir tθ = ti , und ansonsten tθ = t. • Für eine komplexe Struktur gilt f (t1 , . . . , tn )θ = f (t1 θ, . . . , tn θ). Dann entspricht die Substitution θ1 = [X|Z][Z|Y ] der Substitution [X|Y, Z|Y ], da X zuerst durch Y und dieses dann durch Z ersetzt wird. Sie ist damit verschieden von θ2 = [X|Z, Z|Y ]. Für t = f (X, Y, Z) gilt z.B. tθ1 = f (Y, Y, Y ) und tθ2 = f (Z, Y, Y ). Prof. Dr. Dietmar Seipel 309 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Resolution) Wir betrachten das nicht–rekursive, definite Logikprogramm P = { r, f1 , f2 , f3 , f4 } und die Anfrage Q = ← grandparent(X, Z): r = grandparent(X, Z) ← parent(X, Y ) ∧ parent(Y, Z), f1 = parent(’Elizabeth’, ’Queen Mum’), f2 = parent(’Elizabeth’, ’George’), f3 = parent(’Charles’, ’Elizabeth’), f4 = parent(’William’, ’Charles’). ’Queen Mum’ ’George’ f1 f2 ’Elizabeth’ f3 ’Charles’ Aus G0 = Q erhält man mittels r und θ1 = ∅ die Resolvente G1 = ← parent(X, Y ) ∧ parent(Y, Z). f4 ’William’ Daraus kann man mit der Selektionsfunktion sl , welche stets das linkeste Literal eines Goals auswählt, z.B. folgende SLD–Widerlegungen erhalten: Prof. Dr. Dietmar Seipel 310 Logik für Informatiker Wintersemester 2015/16 • Mittels f3 und θ2 = { X 7→ ’Charles’, Y 7→ ’Elizabeth’ } erhalten wir G2 = ← parent(’Elizabeth’, Z). – Mittels f1 und θ3 = { Z 7→ ’Queen Mum’ } erhalten wir G3 = 2 und die Antwortsubstitution θ = { X 7→ ’Charles’, Y 7→ ’Elizabeth’, Z 7→ ’Queen Mum’ }. – Mittels f2 und θ3 = { Z 7→ ’George’ } erhalten wir ebenfalls G3 = 2; nun ist die Antwortsubstitution θ0 = { X 7→ ’Charles’, Y 7→ ’Elizabeth’, Z 7→ ’George’ }. • Mittels f4 und f3 erhalten wir aus G1 die Antwortsubstitution θ00 = { X 7→ ’William’, Y 7→ ’Charles’, Z 7→ ’Elizabeth’ }. Später werden wir alle SLD–Widerlegungen in einem SLD–Baum zusammenfassen. Prof. Dr. Dietmar Seipel 311 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Resolution) Betrachten wir das rekursive, definite Logikprogramm P = { r, e, f } mit den folgenden Regeln (bzw. Fakten): r = anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ), e = anc(X, X), f = par (a, b). Zur Vereinfachung benutzen wir anstelle der üblichen bereichsbeschränkten Regel e0 = anc(X, Y ) ← par (X, Y ) das Fakt e = anc(X, X) mit Variablen zusammen mit der rekursiven Regel r. Dadurch wird im folgenden anc als die reflexive, transitive Hülle von par berechnet. Prof. Dr. Dietmar Seipel 312 Logik für Informatiker Wintersemester 2015/16 Hier kann das Goal G0 = ← anc(X, b) von allen Selektionsfunktionen mittels der Regel r zu G1 = ← A1 ∧ A2 , mit A1 = par (X, Z1 ) und A2 = anc(Z1 , b), resolviert werden. Sei sl (sr ) die Selektionsfunktion, welche stets das linkeste (rechteste) Literal eines Goals auswählt. 1. sl wählt das erste (linkeste) Atom A1 = par (X, Z1 ) in G1 . Dieses kann nur mit dem Fakt f = A = par (a, b) resolviert werden. Mit M GU(A1 , A) = { X 7→ a, Z1 7→ b } erhält man das verkürzte Goal G2 = ← anc(b, b). Eine weitere Resolution mit dem Fakt e würde die leere Klausel G3 = 2 liefern, und somit die Antwort anc(a, b). Prof. Dr. Dietmar Seipel 313 Logik für Informatiker Wintersemester 2015/16 2. Die Selektionsfunktion sr wählt das zweite (rechteste) Atom eines Goals; in G1 ist das A2 = anc(Z1 , b). Die folgende Baumdarstellung zeigt das weitere Vorgehen: G0 = ← anc(X , b) r ? G1 = ← par (X , Z1 ) ∧ anc(Z1 , b) r2 e2 s G02 = ← par (X, Z1 ) ∧ par (Z1 , Z2 ) ∧ anc(Z2 , b) G002 = ← par (X, b) f ? G003 = 2 Prof. Dr. Dietmar Seipel 314 Logik für Informatiker Wintersemester 2015/16 A2 = anc(Z1 , b) kann mit Varianten r2 = anc(X2 , Y2 ) ← par (X2 , Z2 ) ∧ anc(Z2 , Y2 ), e2 = anc(X2 , X2 ), der Regeln r bzw. e resolviert werden. Sei A jeweils deren Regelkopf. • Mit r2 , A = anc(X2 , Y2 ) und M GU(A2 , A) = { X2 7→ Z1 , Y2 7→ b } erhält man das verlängerte Goal G02 = ← par (X, Z1 ) ∧ par (Z1 , Z2 ) ∧ anc(Z2 , b). • Mit e2 , A = anc(X2 , X2 ) und M GU(A2 , A) = { X2 7→ b, Z1 7→ b } erhält man das verkürzte Goal G002 = ← par (X, b). Prof. Dr. Dietmar Seipel 315 Logik für Informatiker Wintersemester 2015/16 Eine weitere Resolution mit dem Fakt f würde M GU(par (X, b), f ) = { X 7→ a } und die leere Klausel G003 = 2 liefern, und somit die Antwort anc(a, b). Mittels des Faktes e kann das Goal G0 = ← anc(X, Y ) von allen Selektionsfunktionen zur leeren Klausel G01 = 2 resolviert werden. Dabei wird M GU(anc(X, Y ), anc(X, X)) = { Y 7→ X } berechnet, und somit die Antwort anc(X, X). Diese Antwort enthält noch das Variablensymbol X. Also kann die SLD–Resolution Nicht–Grundatome als Antworten ableiten. Prof. Dr. Dietmar Seipel 316 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Widerlegungsbäume) Wir betrachten weiterhin das definite Logikprogramm P = { r, e, f }, jetzt aber mit den Anfragen Q1 = ← anc(X, b), Q2 = ← anc(X, Y ). Die Regeln (bzw. Fakten) sind folgende: r = anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ), e = anc(X, X), f = par (a, b). Anders als in Q1 , ist in Q2 auch die zweite Argumentposition mit einem Variablensysmbol – hier Y – belegt. Deswegen kann eine Antwort berechnet werden, die noch Variablensymbole enthält. Prof. Dr. Dietmar Seipel 317 Logik für Informatiker Wintersemester 2015/16 Im folgenden wird ein SLD–Widerlegungsbaum T1 für Q1 angegeben: T1 : ← anc(X, b) ?9 ← par (X, Z1 ) ∧ anc(Z1 , b) ?9 ← anc(b, b) r1 = anc(X1 , Y1 ) ← par (X1 , Z1 ) ∧ anc(Z1 , Y1 ) θ1 = { X1 7→ X, Y1 7→ b } f = par (a, b) θ2 = { X 7→ a, Z1 7→ b } e2 = anc(X2 , X2 ) ?9 2 θ3 = { X2 7→ b } Die Antwortsubstitution ist θ = θ1 · θ2 · θ3 = { X 7→ a, X1 7→ a, X2 7→ b, Y1 7→ b, Z1 7→ b }, und die berechnete Antwort ist anc(a, b). Prof. Dr. Dietmar Seipel 318 Logik für Informatiker Wintersemester 2015/16 Die SLD–Resolution kann auch nicht–bereichsbeschränkte definite Logikprogramme mit Funktionssymbolen behandeln. Sie hat keine Probleme mit Fakten, die Variablen enthalten, wie etwa e = anc(X, X). T2 : ← anc(X, Y ) ?) 2 e = anc(X, X) θ = { Y 7→ X } Allerdings ist die erzeugte Antwortsubstitution θ dann unter Umständen keine Grundsubstitution. Im obigem Beispiel für Q2 = ← anc(X, Y ) ist die berechnete Antwort anc(X, X) dann ein Fakt mit Variablen, das zeigt, daß die beiden Grundinstanzen anc(a, a) und anc(b, b) aus P ableitbar sind. Prof. Dr. Dietmar Seipel 319 Logik für Informatiker Wintersemester 2015/16 Listenkonkatenation In der Logik dienen Terme als Datenstruktur. Eine Liste [1, 2, 3] wird als Term list(1 , list(2 , list(3 , nil ))) repräsentiert. Dabei ist list ein 2–stelliges Funktionssymbol, und nil ist ein 0–stelliges Funktionssymbol, welches das Listenende markiert. Die folgenden Regeln können zwei Listen Xs und Ys mittels des Aufrufs ← append (Xs, Ys, Zs) zu einer Liste Zs konkatenieren: append (list(X , Xs), Ys, list(X , Zs)) ← append (Xs, Ys, Zs), append (nil , Ys, Ys). X Xs Ys Zs Prof. Dr. Dietmar Seipel 320 Logik für Informatiker Wintersemester 2015/16 In der gezeigten kompakten Fassung der ersten Regel erfolgt die Listenzerlegung und der Listenaufbau in der Kopfzeile: append (list(X , Xs), Ys, list(X , Zs)) ← append (Xs, Ys, Zs). Die folgende ausführlichere Fassung hat dafür separate Zeilen. Außerdem verdeutlicht die funktionale Notation Zs := append (Xs, Ys), daß Zs durch die Konkatenation von Xs und Ys berechnet wird: append (Xs 0 , Ys, Zs 0 ) ← Xs 0 = list(X , Xs) ∧ Zs := append (Xs, Ys) ∧ Zs 0 = list(X , Zs). % Listenzerlegung % Listenaufbau In der relationalen Notation append (Xs, Ys, Zs) war die Ausgabe Zs dagegen lediglich das letzte Argument – und ansonsten gleichberechtigt mit der Eingabe Xs und Ys. Prof. Dr. Dietmar Seipel 321 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Widerlegungsbaum) ← append(list(1 , list(2 , nil )), list(3 , nil ), Zs) ? 9 θ1 ← append(list(2 , nil ), list(3 , nil ), Zs1 ) ? 9 2 9 r2 θ2 ← append(nil , list(3 , nil), Zs2 ) ? r1 f3 θ3 r1 = append(list(X1 , Xs1 ), Ys1 , list(X1 , Zs1 )) ← append(Xs1 , Ys1 , Zs1 ), r2 = append(list(X2 , Xs2 ), Ys2 , list(X2 , Zs2 )) ← append(Xs2 , Ys2 , Zs2 ), f3 = append(nil, Ys3 , Ys3 ). θ1 = { X1 7→ 1, Xs1 7→ list(2 , nil), Ys1 7→ list(3 , nil), Zs 7→ list(1 , Zs1 ) }, θ2 = { X2 7→ 2, Xs2 7→ nil, Ys2 7→ list(3 , nil), Zs1 7→ list(2 , Zs2 ) }, θ3 = { Ys3 7→ list(3 , nil), Zs2 7→ Ys3 = list(3 , nil) }. Prof. Dr. Dietmar Seipel 322 Logik für Informatiker Wintersemester 2015/16 Im Endergebnis θ = θ1 · θ2 · θ3 gilt Zs 7→ list(1 , Zs1 ) 7→ list(1 , list(2 , Zs2 )) 7→ list(1 , list(2 , list(3 , nil ))). Die berechnete Antwort ist also append (list(1 , list(2 , nil )), list(3 , nil ), Zs)θ = append (list(1 , list(2 , nil )), list(3 , nil ), list(1 , list(2 , list(3 , nil )))), denn die Konkatenation der Listen [1, 2] und [3] liefert die Liste [1, 2, 3]. Prof. Dr. Dietmar Seipel 323 Logik für Informatiker Wintersemester 2015/16 Vollständigkeit und Korrektheit der SLD–Resolution Sei P ein definites Logikprogramm und Q = ← A eine atomare Anfrage. 1. Es gibt genau dann eine SLD–Widerlegung mit der Antwort Aθ, wenn Aθ im minimalen Modell MP von P liegt. 2. Dieses Resultat ist unabhängig von der verwendeten Selektionsfunktion s. P ROLOG verwendet immer die Selektionsfunktion sl , welche stets das linkeste (erste) Literal eines Goals auswählt. Durch Umstellung der Atome in den Regelrümpfen kann der Programmierer de facto eine andere Selektionsfunktion simulieren. Prof. Dr. Dietmar Seipel 324 Logik für Informatiker Wintersemester 2015/16 SLD–Bäume Sei P ein definites Logikprogramm, Q eine Anfrage und s eine Selektionsfunktion. s Der SLD–Baum TP,Q faßt alle möglichen SLD–Ableitungen zusammen: s 1. Die Knoten von TP,Q sind mit Goals markiert, s und die Kanten von TP,Q sind mit Regeln r ∈ P markiert. s 2. Die Wurzel von TP,Q ist mit Q markiert. 3. Ein Knoten v, der mit einem Goal G markiert ist, hat für jede SLD–Resolvente G0 , die man aus G und einer Regel r ∈ P bezüglich s bilden kann, einen Nachfolgerknoten v 0 . 4. Dieser ist mit G0 markiert, und die Kante h v, v 0 i ist mit r markiert. Prof. Dr. Dietmar Seipel 325 Logik für Informatiker Wintersemester 2015/16 Jeder mit dem Goal G = 2 endende Ast eines SLD–Baumes entspricht einer SLD–Widerlegung bzw. einem SLD–Widerlegungsbaum: • Die Blätter dieser Äste werden als erfolgreich (success) markiert. • Alle anderen Blätter werden als erfolglos (failure) markiert. • Daneben kann es noch unendliche Äste im Baum geben. s2 s1 und TP,Q zu unterschiedlichen Zwei SLD–Bäume TP,Q Selektionsfunktionen s1 , s2 haben immer dieselben Antworten (success–Äste). Sie unterscheiden sich aber in der Regel hinsichtlich ihrer failure–Äste bzw. ihrer unendlichen Äste. Prof. Dr. Dietmar Seipel 326 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Bäume) Wir betrachten das nicht–rekursive, definite Logikprogramm P = { r, f1 , f2 , f3 , f4 } und die Anfrage Q = ← grandparent(X, Z): r = grandparent(X, Z) ← parent(X, Y ) ∧ parent(Y, Z), f1 = parent(’Elizabeth’, ’Queen Mum’), f2 = parent(’Elizabeth’, ’George’), f3 = parent(’Charles’, ’Elizabeth’), f4 = parent(’William’, ’Charles’). In diesem Falle sind alle SLD–Bäume – unabhängig von der Selektionsfunktion – endlich. sl Wir zeigen unten den SLD–Baum TP,Q zur Selektionsfunktion sl . Prof. Dr. Dietmar Seipel 327 Logik für Informatiker Wintersemester 2015/16 ← grandparent(X, Z) r ? ← parent(X, Y ) ∧ parent(Y, Z) f1 9  f2 ← parent(’Queen Mum’, Z ) ← parent(’George’, Z ) failure failure 2 ) { X 7→ ’Charles’, Y 7→ ’Elizabeth’, Z 7→ ’Queen Mum’ } success Prof. Dr. Dietmar Seipel f3 f4 j ← parent(’Elizabeth’, Z ) f1 f2 ? 2 {X → 7 ’Charles’, Y 7→ ’Elizabeth’, Z→ 7 ’George’ } success z ← parent(’Charles’, Z ) f3 ? 2 {X → 7 ’William’, Y → 7 ’Charles’, Z 7→ ’Elizabeth’ } success 328 Logik für Informatiker Wintersemester 2015/16 Beispiel (SLD–Bäume) Wir betrachten wieder das rekursive, definite Logikprogramm P = { r, e, f } und die Anfrage Q = ← anc(X, b): r = anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ), e = anc(X, X), f = par (a, b). Die SLD–Bäume zu den Selektionsfunktionen sl bzw. sr haben dieselben Antworten (success–Äste). • Allerdings ist in diesem Falle Tl endlich, • wohingegen Tr unendliche Äste hat. Für sr könnte man in obigem Beispiel die unendlichen Äste vermeiden, indem man die Reihenfolge der Rumpfatome invertiert. Prof. Dr. Dietmar Seipel 329 Logik für Informatiker Wintersemester 2015/16 Der SLD–Baum Tl zur Selektionsfunktion sl ist endlich: ← anc(X, b) Tl : r ← par (X, Z1 ) ∧ anc(Z1 , b) f ? ← anc(b, b) r ← par (b, Z2 ) ∧ anc(Z2 , b) failure Prof. Dr. Dietmar Seipel e R 2 { X 7→ b } success e R 2 { X 7→ a } success 330 Logik für Informatiker Wintersemester 2015/16 Der SLD–Baum Tr zur Selektionsfunktion sr ist unendlich, hat aber die gleichen Antwortsubstitutionen in den success–Blättern wie Tl : ← anc(X, b) Tr : r e ← par (X, Z1 ) ∧ anc(Z1 , b) r e  ← par (X, Z1 ) ∧ par (Z1 , Z2 ) ∧ anc(Z2 , b) r ) ← par (X, Z1 ) ∧ par (Z1 , Z2 ) ∧ par (Z2 , Z3 ) ∧ anc(Z3 , b) r e R R R 2 { X 7→ b } success ← par (X, b) e f s ← par (X, Z1 ) ∧ par (Z1 , b) f ? R 2 { X 7→ a } success ← par (X, a) failure (unendlicher Ast) Prof. Dr. Dietmar Seipel 331 Logik für Informatiker Wintersemester 2015/16 Steuerung der SLD–Resolution Der Logikprogrammierer kann bei gegebener Selektionsfunktion durch • die Reihenfolge der Regeln und • die Reihenfolge der Rumpfatome in den Regeln die Abarbeitung steuern: • Wenn wir in unserem letzten Beispiel die Regel e vor die Regel r stellen, dann wandern im neuen SLD–Baum Tr0 zur Selektionsfunktion sr die mit e markierten Kanten vor die mit r markierten. • Bei Backtracking findet der LWR–Durchlauf von Tr0 nun die beiden Antworten, bevor der unendliche Ast zu einer Dauerschleife führt. • Wenn wir dagegen die Reihenfolge der Rumpfatome von r vertauschen, dann hat der neue SLD–Baum Tr00 zu sr dieselbe Struktur wie der alte SLD–Baum Tl zu sl : r00 = anc(X, Y ) ← anc(Z, Y ) ∧ par (X, Z). Prof. Dr. Dietmar Seipel 332 Logik für Informatiker Wintersemester 2015/16 • Generell ist es am besten die nicht–rekursive Regel e vor die rekursive Regel r zu stellen: e = anc(X, X), r = anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ). • Für die Standard–Selektionsfunktion sl sollte in der rekursiven Regel r der nicht–rekursive Aufruf par (X, Z) vor dem rekursiven Aufruf anc(Z, Y ) stehen. Dies garantiert die Terminierung für azyklische par –Relationen. • Bei zyklischer par –Relation enthält der SLD–Baum Tl aber leider trotzdem unendliche Äste. Für die Fakten f1 = par (a, b), f2 = par (b, a), und die Anfrage Q = ← anc(a, Y ) generiert die alternierende Verwendung von f1 und f2 abwechselnd die Antworten Y 7→ a und Y 7→ b. Prof. Dr. Dietmar Seipel 333 Logik für Informatiker Wintersemester 2015/16 ← anc(a, Y ) Tl : e r R ← par (a, Z1 ) ∧ anc(Z1 , Y ) 2 {Y → 7 a} success f1 ? ← anc(b, Y ) e r R ← par (b, Z2 ) ∧ anc(Z2 , Y ) 2 { Y 7→ b } f2 success ? ← anc(a, Y ) (unendlicher Ast) Prof. Dr. Dietmar Seipel 334 Logik für Informatiker Wintersemester 2015/16 Beispiel (Redundanz in SLD–Bäumen) Wir betrachten nun das etwas erweiterte rekursive, definite Logikprogramm P = { r, e, f1 , f2 } und die Anfrage Q = ← anc(X, Y ): r = anc(X, Y ) ← par (X, Z) ∧ anc(Z, Y ), e = anc(X, X), f1 = par (a, b), f2 = par (b, c). Der SLD–Baum Tl zur Selektionsfunktion sl ist endlich. Die success–Äste leiten der Reihe nach die folgenden Grundinstanzen ab: • success–Äste 1 bis 3: tc(a, c), tc(a, b), tc(b, c); • success–Ast 4: tc(a, a), tc(b, b), tc(c, c). Die Unteranfrage ← anc(c, Y ) wurde redundant in zwei success–Ästen (1 und 3) mit Y 7→ c beantwortet. Derartige Redundanz tritt bei Graphen mit längeren Ketten (hier: a → b → c) noch verstärkt auf. Prof. Dr. Dietmar Seipel 335 Logik für Informatiker Wintersemester 2015/16 ← anc(X, Y ) Tl : r e R ← par (X, Z1 ) ∧ anc(Z1 , Y ) 2 { X 7→ Y } success f1 f2 ← anc(b, Y ) r e R R ← anc(c, Y ) r R e z ← par (b, Z2 ) ∧ anc(Z2 , Y ) ← par (c, Z2 ) ∧ anc(Z2 , Y ) 2 2 { X 7→ a, Y 7→ b } { X 7→ b, Y 7→ c } f2 failure success success ? ← anc(c, Y ) r e R ← par (c, Z3 ) ∧ anc(Z3 , Y ) 2 { X 7→ a, Y 7→ c } failure success Prof. Dr. Dietmar Seipel 336 Logik für Informatiker 3 Wintersemester 2015/16 Logikprogrammierung P ROLOG ermöglicht • deklarative Programmierung • kompakte Programme • agile Softwareentwicklung, rapid Prototyping Die Auswertungsstrategie der SLDNF–Resolution benutzt • Tiefensuche • Backtracking • Unifikation Prof. Dr. Dietmar Seipel 337 Logik für Informatiker 3.1 Wintersemester 2015/16 Grundlagen von P ROLOG Datentypen und Datenstrukturen • Die Beschränkung auf wenige Basisdatentypen und einen einzigen komplexen Datentyp, nämlich die Strukturen (Atome, Terme), der generisch ist und alle anderen Datentypen subsumiert, standardisiert die Datenstrukturen ganz entscheident. • Es gibt keine expliziten Typdeklarationen. Man kann aber rein syntaktisch zwischen P ROLOG–Atomen (Strings), Zahlen und Variablensymbolen unterscheiden; aus diesen kann man komplexere Strukturen bilden. • Es gibt eine große Kollektion von generischen Operationen, die auf alle Strukturen anwendbar sind – und somit auf alle Datentypen. Prof. Dr. Dietmar Seipel 338 Logik für Informatiker Wintersemester 2015/16 Methoden und Kontrollstrukturen • Prädikate realisieren Methoden. Alle Parameter – auch die Rückgabewerte – werden als Argumente eines Prädikats übergeben. Kommentare helfen zu erkennen, welche Argumente die Eingabe bzw. die Ausgabe bilden. • Manche Prädikate kann man mit unterschiedlichen Bindungsmustern aufrufen, und für dieselbe Eingabe kann es unterschiedliche Ausgaben geben (relationales Programmieren). Die meisten Prädikate sind aber funktional. • Häufig werden Meta–Prädikate verwendet. Auch Kontrollstrukturen basieren auf Meta–Prädikaten. Zusätzlich zu den Standardkontrollstrukturen, wie Verzweigungen (if–then–else), Schleifen (for, while), und Rekursion, können benutzerdefinierte Kontrollstrukturen in Form von Meta–Prädikaten gebildet werden. Prof. Dr. Dietmar Seipel 339 Logik für Informatiker Wintersemester 2015/16 Strukturen in P ROLOG P ROLOG–Atom: z.B. a, books, ’Books’, kt_321_xy Konstante: P ROLOG–Atom | Number: z.B. books, 0, 123 Variable: beginnend mit Großbuchstaben oder mit “_” z.B. X, Y, Books, _, _A, _a Funktor (Funktions– bzw. Prädikatensymbol): Operator | P ROLOG–Atom: z.B. +, -, ≤, ancestor Struktur: Konstante | Variable | Funktor(Struktur, . . . , Struktur) z.B. +(1,7), ancestor(’William’,’Elizabeth’); Listen sind spezielle Strukturen zum Funktor “.” Prof. Dr. Dietmar Seipel 340 Logik für Informatiker Wintersemester 2015/16 P ROLOG–Klauseln Eine P ROLOG–Klausel (Regel, Fakt) ist eine Infix–Struktur der Form Kopf :– Rumpf. “:-” spricht man dabei als “falls” aus. Falls der Rumpf leer ist (Fakt), so kann man “:-” weglassen und kurz “Kopf” schreiben. Der Regelrumpf kann folgende Junktoren enthalten: • Konjunktion “,”, • Disjunktion “;”, und • Negation “\+”, “not”. Eine negierte Formel kann man als “\+ F” oder als “not(F)” schreiben. Prof. Dr. Dietmar Seipel 341 Logik für Informatiker Wintersemester 2015/16 Prädikatensymbole: ancestor, parent Regel: ancestor(X, Z) :ancestor(X, Y), parent(Y, Z). Ein Elternteil Z eines Vorfahren Y von X ist ebenfalls ein Vorfahre. Fakten: parent(a, b). parent(b, c). parent(c, d). Goal: ?- ancestor(a, Z). Prof. Dr. Dietmar Seipel 342 Logik für Informatiker Wintersemester 2015/16 Prädikatensymbole: likes, woman, nice, loves Regeln: likes(george, Y) :woman(Y), likes(Y, books). likes(mary, Y) :( nice(Y) ; loves(Y, cats) ) Fakten: woman(mary). likes(mary, books). loves(george, cats). Goal: ?- likes(george, Y). Prof. Dr. Dietmar Seipel 343 Logik für Informatiker Wintersemester 2015/16 Das Prädikat likes besteht aus 2 Regeln und einem Fakt. Diese decken unterschiedliche Fälle ab: • Die erste Regel besagt, daß George alle Frauen mag, die Bücher mögen. • Die zweite Regel besagt, daß Mary alles, was schön (nice) ist, und alle Lebewesen, die Katzen lieben, mag. Ein Fakt besagt außerdem, daß Mary Bücher mag. In der prozeduralen Programmierung könnte man eine Fallunterscheidung in einem case–Statement ausdrücken. Die likes–Regel zu Mary mit dem disjunktiven Rumpf könnte man in zwei separate Regeln zerlegen. Die Bündelung der Information zu Mary – zu der man eventuell auch noch das Fakt hinzunehmen könnte – erscheint aber softwaretechnisch auch sehr sinnvoll. Da uns momentan keine Information zu nice vorliegt, ist der erste Teil der Regel inaktiv. Prof. Dr. Dietmar Seipel 344 Logik für Informatiker Wintersemester 2015/16 Die Bündelung liefert folgende Regel mit einem disjunktiven Regelrumpf: likes(mary, Y) :( nice(Y) ; loves(Y, cats) ; Y = books ). Diese ist äquivalent zu drei einzelnen Regeln: likes(mary, nice(Y). likes(mary, loves(Y, likes(mary, Y) :Y) :cats). books). Die Reihenfolge der Regeln und Fakten zum selben Prädikatensymbol ist – wie in klassischen Programmiersprachen auch – wichtig. Prof. Dr. Dietmar Seipel 345 Logik für Informatiker Wintersemester 2015/16 Infix–Notation, Domain Specific Language (DSL) Wenn man geeignete Operatoren (Infix, Präfix, Postfix) definiert, dann kann man die P ROLOG–Klauseln etwas natürlicher notieren: X has_ancestor Z :X has_ancestor Y and Y has_parent Z. george likes Y :Y is_a_woman and Y likes books. mary likes Y :Y is_nice or Y loves cats. mary is_a_woman. mary likes books. george loves cats. Man könnte H :- B sogar als B implies H schreiben. Prof. Dr. Dietmar Seipel 346 Logik für Informatiker Wintersemester 2015/16 Anfragen in P ROLOG Ein P ROLOG–Interpreter versucht ein Goal durch Inferenz zu beweisen. Dies erfolgt Top–Down vom Goal ausgehend durch DFS–Durchlauf (Tiefensuche, Depth–First–Search) des SLD–Baumes. Beispiel (Anfragen) ?- likes(george, Y). Y = mary ?- likes(X, X = george, X = mary, Y X = mary, Y Prof. Dr. Dietmar Seipel Y). Y = mary ; = george ; = books . 347 Logik für Informatiker Wintersemester 2015/16 P ROLOG gibt eine Antwort auf eine Anfrage zurück: • Falls die Anfrage erfolgreich beantwortet wurde, so gibt P ROLOG die erzeugte Variablenbelegung als Antwort zurück; falls keine Variablen belegt wurden, so ist die Antwort true. • Falls die Anfrage erfolglos beantwortet wurde, so ist die Antwort false. Bei erfolgreicher Beantwortung der Anfrage kann man hinter der Antwort einen Strichpunkt gefolgt von Return eingeben. Dieser stößt Backtracking an, so daß P ROLOG versucht eine weitere Antwort zu finden. Wenn man nur Return eingibt, so ist die Anfrageauswertung beendet. Ebenso ist die Anfrageauswertung nach der Antwort false automatisch sofort beendet. Prof. Dr. Dietmar Seipel 348 Logik für Informatiker Wintersemester 2015/16 Auswertung von Anfragen in P ROLOG • Die Auswertung von P ROLOG–Regeln erfolgt Top–Down mittels der Methode der SLDNF–Resolution: aus einer Anfrage an das Kopfatom einer Regel werden Unteranfragen an die Rumpfatome erzeugt. • Dies entspricht dem Vorgehen bei der Abarbeitung von prozeduralen Programmiersprachen. • Falls ein Rumpfatom mehrere Antworten liefert, so wird zuerst mit einer solchen Antwort weitergerechnet (Tiefensuche); falls die Berechnung später fehlschlägt, so kann mit der nächsten Antwort fortgefahren werden (Backtracking). • In der Praxis sind viele P ROLOG–Prädikate aber funktional: aus einer Eingabe wird genau eine Ausgabe erzeugt. Prof. Dr. Dietmar Seipel 349 Logik für Informatiker Wintersemester 2015/16 Aus der Anfrage ← likes(X, Y ) wird mittels der Ersetzung X 7→ george und der Regel r1 = likes(george, Y ) ← woman(Y ) ∧ likes(Y , books) eine Folge von Unteranfragen erzeugt: ← woman(Y ) ∧ likes(Y , books) Aufgrund des Fakts f1 wird die erste Unteranfrage mit Y 7→ mary beantwortet. Der neue Wert für Y wird in der zweiten Unteranfrage sofort berücksichtigt, so daß wir also ← likes(mary, books) zu beantworten haben. Aufgrund des Fakts f2 ist die Antwort dafür ja. Prof. Dr. Dietmar Seipel 350 Logik für Informatiker Wintersemester 2015/16 SLD–Baum ← likes(X, Y ) r1 9 ← woman(Y ) ∧ likes(Y, books) f1 ? ← likes(mary, books) r2  ← nice(books) ∨ loves(books, cats) failure r2 ? f2 q ← nice(Y ) ∨ loves(Y, cats) 2 {X 7→ mary, Y 7→ books} f3 success ? 2 {X → 7 mary, Y 7→ george} f2 j success 2 {X 7→ george, Y 7→ mary} success Der SLD–Baum faßt alle SLD–Ableitungen zusammen. Jeder success–Ast gibt eine Antwort. Prof. Dr. Dietmar Seipel 351 Logik für Informatiker Wintersemester 2015/16 Kontrollprimitive, welche über die PL1 hinausgehen • Eingabe und Ausgabe: read und write. • Meta–Prädikate wir findall und maplist realisieren komplexe Kontrollstrukturen. • assert und retract verändern die interne Datenbank von P ROLOG; clause sucht in dieser. • call und apply rufen Goals auf, die vorher zusammengebaut werden können. • Der Cut “!” friert die bisherige Variablenbelegung in der aktuellen Regel ein. • ... Prof. Dr. Dietmar Seipel 352 Logik für Informatiker Wintersemester 2015/16 Start von P ROLOG und Konsultieren in die Datenbasis P ROLOG kann mittels pl von der Kommandozeile eines Betriebssystems oder von einer GUI aus gestartet werden: % pl Welcome to SWI-Prolog ... Danach kann man mittels consult/1 bzw. [...] eine P ROLOG–Datei in die Datenbasis von P ROLOG einlesen: ?- [’sources/projects/teaching/likes.pl’]. % sources/.../likes.pl compiled 0.00 sec, 0 bytes Prof. Dr. Dietmar Seipel 353 Logik für Informatiker Wintersemester 2015/16 Eingabe und Ausgabe Die Eingabe und Ausgabe von erfolgt mittels read/1,2 und write/1,2: ?- read(X). |: likes(mary, cats). X = likes(mary, cats). ?- write(’Hello World’). Hello World true. Die zweistelligen Prädikate read/2 und write/2 greifen auf Dateien zu. Prof. Dr. Dietmar Seipel 354 Logik für Informatiker Wintersemester 2015/16 Das Meta–Prädikat findall/3 Finden aller Lösungen für ein Goal: findall( X, goal(X), Xs ) Das D DK erlaubt sogar die äquivalente Mengenschreibweise Xs <= { X | goal(X) }. Weitere wichtige Meta–Prädikate sind checklist/2 und maplist/3 für Listen sowie die Prädikate für Schleifen (Kontrollstrukturen) aus der Loops–Bibliothek (z.B. foreach-do). Prof. Dr. Dietmar Seipel 355 Logik für Informatiker Wintersemester 2015/16 Mit dem Meta–Prädikat findall/3 kann man alle Antworten auf eine Anfrage bestimmen: ?- findall( [X, Y], likes(X, Y), Pairs ). Pairs = [[george,mary], [mary,george], [mary,books]]. Pairs wird als die Liste aller Paare [X, Y] bestimmt, für die likes(X, Y) gilt. Die äquivalente Mengenschreibweise des D DK ist ?- Pairs <= { [X, Y] | likes(X, Y) }. Prof. Dr. Dietmar Seipel 356 Logik für Informatiker Wintersemester 2015/16 Verändern der Datenbasis: assert und retract Man kann mittels assert/1 auch dynamisch die Datenbasis von P ROLOG erweitern: ?- read(X), assert(X). |: likes(mary, cats). X = likes(mary, cats) . Nachfolgende Aufrufe können die erweiterte Datenbasis benutzen: ?- likes(mary, cats). true . Mittels retract/1 kann man in der Datenbasis von P ROLOG löschen. Prof. Dr. Dietmar Seipel 357 Logik für Informatiker Wintersemester 2015/16 Arbeiten mit Strukturen Eine Struktur kann in eine Liste bestehend aus dem Funktor und den Argumenten zerlegt werden: ?- likes(mary, books) =.. Xs. Xs = [likes, mary, books] . Eine Liste hat den Funktor ’.’ mit zwei Argumenten, dem ersten Listenelement und der Restliste: ?- [likes, mary, books] =.. Ys. Ys = [’.’, likes, [mary, books]] . Prof. Dr. Dietmar Seipel 358 Logik für Informatiker Wintersemester 2015/16 Eine Liste ist eine zweistellige Stuktur mit dem Funktor ’.’: ?- functor([a,b,c,d], F, N). F = ’.’, N = 2 . Mittels arg/3 kann man auf die Argumente einer Stuktur zugreifen; über Backtracking erhält man der Reihe nach alle Argumente: ?- arg(N, [a,b,c,d], A). N = 1, A = a ; N = 2, A = [b,c,d] . Prof. Dr. Dietmar Seipel 359 Logik für Informatiker Wintersemester 2015/16 Man kann zur Laufzeit mittels =../2 dynamische Strukturen zusammenbauen und mittels call/1 aufrufen: ?- read(P), S =.. [P, X, Y], call(S). |: likes. P = likes, S = likes(X, Y), X = george, Y = mary . Dies geht noch eleganter, wenn man stattdessen apply/2 verwendet, denn S =.. [P,X1,...,Xn], call(S) ist äquivalent zu apply(P, [X1,...,Xn]). Der Aufruf read(P), P(X,Y) ist in P ROLOG nicht erlaubt, da eine Variable – hier P – nicht an der Stelle eines Prädikatensymbols stehen kann. Prof. Dr. Dietmar Seipel 360 Logik für Informatiker Wintersemester 2015/16 Listen sind spezielle P ROLOG–Strukturen mit dem binären Funktor “.”. Beispiel: [a,b,c,d] = .(a,.(b,.(c,.(d,[])))) leere Liste: [] Listenkonstruktion: Falls X und Xs bereits gebunden (mit Werten belegt) sind, so ist [X|Xs] die Liste, die man erhält, wenn man das Element X an die Liste Xs vorne anhängt. Für X = a und Xs = [b,c,d] ist [X|Xs] = [a,b,c,d]. Listenzerlegung: Falls X und Xs ungebunden sind, so liefert der Aufruf [X|Xs] = [a,b,c,d] die Belegungen X = a und Xs = [b,c,d]; man kann eine Liste also in ihren Kopf X und den Rest Xs zerlegen. Früher hatten wir das Funktionssymbol list anstelle von ”.” und die Konstante nil anstelle von [] verwendet. Prof. Dr. Dietmar Seipel 361 Logik für Informatiker Wintersemester 2015/16 Listenkonstruktion und Listenzerlegung erfolgen also mittels desselben Aufrufs Xs = [Head|Tail]. Die folgenden beiden Prädikate bestimmen das erste Listenelement Head und den Rest Tail der Liste. list_to_head(Xs, Head) :Xs = [Head|_]. list_to_tail(Xs, Tail) :Xs = [_|Tail]. Um eine “singleton variable warning” zu vermeiden, wird der jeweils nicht benötigte Listenteil mittels einer anonymen Variable “_” (Wildcard) bezeichnet. Prof. Dr. Dietmar Seipel 362 Logik für Informatiker Wintersemester 2015/16 Die Listenschreibweise [X1 , . . . ,Xn ] nennt man Syntactic Sugar. Eine Liste ist eigentlich eine stark verschachtelte binäre Struktur: .( X1 , .(X2 , .( . . . ,.(Xn ,[])))). |{z} | {z } Head Tail Somit ist [Head|Tail] = .(Head, Tail). Der Aufruf .(a,.(b,.(c,.(d,[])))) = .(Head, Tail), bestimmt mittels Unifikation Head = a und Tail = .(b,.(c,.(d,[]))). Prof. Dr. Dietmar Seipel 363 Logik für Informatiker Wintersemester 2015/16 Die Listenkonstruktion aus einem gegebenen Kopf und einem Rest erfolgt – wie bereits gezeigt – auch mittels des Aufrufs Xs = [Head|Tail]: head_and_tail_to_list(Head, Tail, Xs) :Xs = [Head|Tail]. Dasselbe Prädikat kann man auch benutzen, um eine gegebene Liste in Kopf und Rest zu zerlegen: ?- head_and_tail_to_list(a, [b,c,d], Xs). Xs = [a,b,c,d] . ?- head_and_tail_to_list(Head, Tail, [a,b,c,d]). Head = a, Tail = [b,c,d] . Prof. Dr. Dietmar Seipel 364 Logik für Informatiker Wintersemester 2015/16 Listenrekursion: das Prädikat member /* member(?X, +Xs) 0, M is N - 1. diff(sin(X), X, cos(X)). diff(e^X, X, e^X). diff(F+G, X, DF+DG) :diff(F, X, DF), diff(G, X, DG). diff(C*F, X, C*DF) :atomic(C), !, diff(F, X, DF). Der Cut in der letzten Regel ist hier eigentlich nicht erforderlich. Er wird erst dann wichtig, wenn man das Regelsystem noch erweitert. Prof. Dr. Dietmar Seipel 378 Logik für Informatiker Wintersemester 2015/16 Hyperresolution in P ROLOG Wir kodieren eine DATALOG–Regel A ← B1 ∧ . . . ∧ Bn als eine Paar–Struktur [A]-[B1 ,...,Bn ]. Die Liste [A] enthält das Kopfatom, die Liste [B1 ,...,Bn ] die Rumpfatome. Ein Fakt, d.h., eine Regel ohne Rumpfatome (n = 0), kann auch kurz als [A] kodiert werden. Um auch Regeln A1 ∨ . . . ∨ Ak ← B1 ∧ . . . ∧ Bn mit disjunktiven Regelköpfen kodieren zu können, wird der Regelkopf als Liste repräsentiert: [A1 ,...,Ak ]-[B1 ,...,Bn ], was bei DATALOG zunächst eigentlich nicht erforderlich wäre. Prof. Dr. Dietmar Seipel 379 Logik für Informatiker Wintersemester 2015/16 parse_rule/2 zerlegt eine DATALOG–Regel in Kopf und Rumpf. Dann wird aus einem Fakt [A] eine Paar–Struktur [A]-[] mit einem leeren Rumpf. parse_rule(Head-Body, Head-Body) :!. parse_rule(Head, Head-[]). Im D DK wird diese Repräsentation noch um Default Negation erweitert. Prof. Dr. Dietmar Seipel 380 Logik für Informatiker Wintersemester 2015/16 Das Prädikat hres/3 generiert zu einem DATALOG–Programm Program und einer Herbrand–Interpretation Int_1 eine neue Herbrand–Interpretation Int_2 bestehend aus den Hyperresolventen. % hres(+Program, +Int_1, -Int_2) X. 2. Conquer: Sortiere F1 und F2 rekursiv mit Quicksort • Quicksort(F1 ) → F10 sortiert • Quicksort(F2 ) → F20 sortiert 3. Merge: Bilde die Ergebnisfolge F 0 duch Hintereinanderhängen von F10 , X, F20 in dieser Reihenfolge. Prof. Dr. Dietmar Seipel 401 Logik für Informatiker Wintersemester 2015/16 Quicksort in P ROLOG % quicksort(+List, ?Sorted_List) X ), Xs2 ). append([], Ys, Ys). append([X|Xs], Ys, [X|Zs]) :append(Xs, Ys, Zs). Prof. Dr. Dietmar Seipel 404 Logik für Informatiker Wintersemester 2015/16 Mittels des Meta–Prädikats sublist/3 kann man die Listenaufteilung noch etwas kompakter formulieren: quicksort_divide(X, Xs, Xs1, Xs2) :sublist(>(X), Xs, Xs1), sublist(<(X), Xs, Xs2). Ein Element X1 von Xs kommt nach Xs1, falls >(X, X1) gilt; in Infix–Notation bedeutet dies X > X1. Analog kommen die Elemente X2 von Xs mit <(X, X2) nach Xs2; in Infix–Notation bedeutet dies X < X2. Falls ein Element mehrfach in der zu sortierenden Liste vorkommt, so ist es trotzdem nur einmal in der Resultatsliste enthalten, denn das Pivot–Element X wird nicht in Xs1 oder Xs2 aufgenommen. Dies könnte man ändern, indem man > durch >= ersetzt, oder < durch =<. Prof. Dr. Dietmar Seipel 405 Logik für Informatiker Wintersemester 2015/16 Mergesort Mergesort („Sortieren durch Mischen“) ist eines der ältesten und bestuntersuchtesten Verfahren zum Sortieren mit Hilfe von Computern. John von Neumann hat es bereits 1945 vorgeschlagen. Mergesort eignet sich auch besonders für das Sortieren von Daten auf Sekundärspeichern, das externe Sortieren. Mergesort sortiert eine Folge F durch rekursives Teilen nach aufsteigenden Werten. Prof. Dr. Dietmar Seipel 406 Logik für Informatiker Wintersemester 2015/16 Mergesort in Pseudo–Code Falls F die Länge N = 0 oder N = 1 hat, so ist F bereits sortiert und bleibt unverändert. Sonst: 1. Divide: Teile F in zwei etwa gleich große Teilfolgen F1 und F2 . 2. Conquer: Sortiere F1 und F2 rekursiv mit Mergesort • Mergesort(F1 ) → F10 sortiert • Mergesort(F2 ) → F20 sortiert 3. Merge: Bilde die Resultatfolge durch Verschmelzen von F10 und F20 . Lasse dazu je einen Positionszeiger (Index) durch die Teilfolgen F10 , F20 so wandern: Bewege jeweils in einem Schritt denjenigen der beiden Zeiger um eine Position weiter, der auf den kleineren Schlüssel zeigt. Prof. Dr. Dietmar Seipel 407 Logik für Informatiker Wintersemester 2015/16 Mergesort in Java public static void mergesort(int[] a, int l, int r) { int i, j, k, m; int[] b = new int[a.length]; if (r > l) { /* Divide */ m = (l + r) / 2; /* Conquer */ mergesort(a, l, m); mergesort(a, m+1, r); Prof. Dr. Dietmar Seipel 408 Logik für Informatiker Wintersemester 2015/16 /* Merge */ // zuerst alle Werte ins Feld b kopieren: // b = a[l],...,a[m],a[r],...a[m+1] for (i=m; i >= l; i--) b[i] = a[i]; for (j=m+1; j <= r; j++) b[r+m+1-j] = a[j]; // dann die Werte der Groesse nach // zurueckschreiben i=l; j=r; for (k=l; k <= r; k++) { if (b[i] < b[j]) { a[k] = b[i++]; } else { a[k] = b[j--]; } } } } Prof. Dr. Dietmar Seipel 409 Logik für Informatiker Wintersemester 2015/16 Beispiel (Mergesort) F = (2, 1, 3, 9, 5, 6, 7, 4, 8, 10) wird aufgespalten in F1 = (2, 1, 3, 9, 5), F2 = (6, 7, 4, 8, 10). Sortieren von F1 , F2 ergibt F10 = (1, 2, 3, 5, 9), F20 = (4, 6, 7, 8, 10). Verschmelzen von F10 und F20 : 1 2 3 5 9 4 6 7 8 10 ↓ 1 2 3 4 5 6 7 8 9 10 Prof. Dr. Dietmar Seipel 410 Logik für Informatiker Wintersemester 2015/16 Mergesort in P ROLOG % mergesort(+List, ?Sorted_List) X = X1, mergesort_merge(Xs1, [X2|Xs2], Xs) ; X = X2, mergesort_merge([X1|Xs1], Xs2, Xs) ). middle_split(Xs,Xs1,Xs2) splittet eine Liste Xs in zwei etwa gleich große Teile Xs1 und Xs2. Hier wird die Kontrollstruktur If -> Then ; Else verwendet. Prof. Dr. Dietmar Seipel 412 Logik für Informatiker Wintersemester 2015/16 Binäre Suchbäume in P ROLOG Zur binären Suche versuchen wir zuerst der Suchbaum Tree in seine Wurzel Root sowie seinen linken und rechten Teilbaum Lson und Rson zu zerlegen. Dann gibt es 3 Fälle: 1. Ist der Schlüssel Key die Wurzel Root, so wird er gefunden, und die Suche war erfolgreich. 2. Ist der Schlüssel Key kleiner als Root, so wird er rekursiv im linken Teilbaum Lson weiter gesucht. 3. Ist der Schlüssel Key größer als Root, so wird er rekursiv im rechten Teilbaum Rson weiter gesucht. Falls der Suchbaum Tree leer ist, so schlägt der anfängliche Zerlegungsversuch fehlt. Dann wird der Schlüssel Key also nicht gefunden. Prof. Dr. Dietmar Seipel 413 Logik für Informatiker Wintersemester 2015/16 % search_in_binary_tree(+Key, +Tree) search_in_binary_tree(Key, Lson) ; Key > Root -> search_in_binary_tree(Key, Rson) ). Die Suchbäume liegen dabei in einer Termnotation in P ROLOG vor. Prof. Dr. Dietmar Seipel 414 Logik für Informatiker Wintersemester 2015/16 Suchbaum in P ROLOG tree(8, tree(4, tree(2, tree(1, nil, nil), tree(3, nil, nil)), tree(6, tree(5, nil, nil), tree(7, nil, nil)) ), tree(12, tree(10, tree(9, nil, nil), tree(11, nil, nil)), tree(13, nil, nil) ) ) Prof. Dr. Dietmar Seipel Visualisierung in P ROLOG mittels binary_tree_to_picture(Picture, Tree) 415 Logik für Informatiker Wintersemester 2015/16 Der leere Baum wird in P ROLOG als die Konstante nil dargestellt. Falls ein Knoten eines Suchbaumes nur genau einen Sohn hat, so wird als anderer Sohn der leere Baum eingetragen: 2 tree(2, tree(1, nil, nil), nil) Eine entsprechende JAVA–Klasse wäre folgende: 1  Class node { int key ; node lson, rson; ... } Prof. Dr. Dietmar Seipel 416 Logik für Informatiker Wintersemester 2015/16 Einzelne Einfügeoperation Die erste Einfügeregel ist rekursiv. Zuerst wird der alte Suchbaum Tree in seine Wurzel Root sowie seinen linken und rechten Teilbaum Lson und Rson zerlegt. Dann gibt es 3 Fälle: 1. Ist der einzufügende Schlüssel Key die Wurzel Root, so ist der neue Suchbaum New_Tree gleich dem alten Suchbaum Tree. 2. Ist Key kleiner als Root, so ergibt sich der neue Suchbaum New_Tree durch das Einfügen in Lson. 3. Ist Key größer als Root, so ergibt sich New_Tree durch das Einfügen in Rson. Die zweite Regel fügt in einen leeren Suchbaum nil ein. Dann enthält New_Tree nur den einen Wert Key; der linke und rechte Teilbaum sind leer. Prof. Dr. Dietmar Seipel 417 Logik für Informatiker Wintersemester 2015/16 % insert_into_binary_tree(+Key, +Tree, ?New_Tree) New_Tree = Tree ; Key < Root -> insert_into_binary_tree(Key, Lson, L), New_Tree = tree(Root, L, Rson) ; Key > Root, insert_into_binary_tree(Key, Rson, R), New_Tree = tree(Root, Lson, R) ). insert_into_binary_tree(Key, nil, New_Tree) :New_Tree = tree(Key, nil, nil). Prof. Dr. Dietmar Seipel 418 Logik für Informatiker Wintersemester 2015/16 Aufbau eines Suchbaums Man kann aus einer Liste Keys von Schlüsseln durch sukzessives Einfügen in den anfangs leeren Suchbaum nil einen entsprechenden Suchbaum Tree aufbauen: % keys_to_binary_tree(+Keys, ?Tree) ’), write(user, Y), graph_search(Y, [Y|Visited], Path). Prof. Dr. Dietmar Seipel . . . ,Yn =Z] -Z 429 Logik für Informatiker Wintersemester 2015/16 Der initiale Aufruf graph_search(X, [X], Path) berechnet einen einfachen Pfad von X zu einer Senke des Graphen. • Falls X bereits eine Senke ist, so bestimmt die erste Regel für graph_search/3 den Pfad Path als die leere Liste. • Ansonsten wählt die rekursive zweite Regel mittels graph_edge (X, Y) einen Nachfolgerknoten Y und sucht von dort aus weiter. Bei Backtracking können weitere einfache Pfade berechnet werden. • Dazu können in der zweiten Regel alternative Nachfolgerknoten Y betrachtet werden. • In der obigen Implementierung kann über eine Senke hinaus zu anderen Senken weitergesucht werden, indem man die zweite Regel anstelle der ersten verwendet. Prof. Dr. Dietmar Seipel 430 Logik für Informatiker Wintersemester 2015/16 Beispiel (Berechnung in P ROLOG) Das Prädikat graph_search/2 benutzt Tiefensuche, und es berechnet einfache Pfade (ohne doppelte Knoten). Labyrinth: a b c d e f g h i - 6 Prof. Dr. Dietmar Seipel 431 Logik für Informatiker Wintersemester 2015/16 Beim Aufruf graph_search(+Node, ?Path) können alle einfachen Pfade von Node zu einer Senke (graph_sink) über Backtracking berechnet werden: ?- graph_search(i, Path). ->f->h->g->d->e->a->b->c Path = [i, h, g, d, a, b, c] ?- graph_search(e, Path). ->d->a->b->c Path = [e, d, a, b, c] ; ->g->h->i->f false. Prof. Dr. Dietmar Seipel 432 Logik für Informatiker Wintersemester 2015/16 Würde man eine weitere Kante graph_arc(e, b) in den Graphen einfügen (die Wand zwischen e und b einreisen), so gäbe es einen weiteren einfachen Pfad [e, b, c] von e zur Senke c. Man kann alle Antworten mittels Backtracking und findall/3 bestimmen: ?- findall( Path, graph_search(e, Path), Paths ). ... Paths = [ [e, d, a, b, c], [e, b, c] ] Prof. Dr. Dietmar Seipel 433 Logik für Informatiker Wintersemester 2015/16 Implizites und explizites Backtracking In P ROLOG wird automatisch (implizit) Backtracking verwendet. In einer prozeduralen Sprache muß man das Backtracking explizit implementieren. Falls man obigen Code eins–zu–eins in einer prozeduralen Umgebung umsetzen würde, so könnte ein Aufruf graph_edge(X, Y) nur einen einzigen Nachfolgerknoten Y von X produzieren – falls es dann keinen Pfad von Y zu einer Senke gibt, so würde die Berechnung fehlschlagen. Außerdem könnte nur maximal eine Lösung ermittelt werden. Wenn man die Graph–Suche prozedural mit explizitem Backtracking realisiert, so ergibt sich mehr Code als bei der P ROLOG–Implementierung. Prof. Dr. Dietmar Seipel 434 Logik für Informatiker Wintersemester 2015/16 Man kann in P ROLOG (im Gegensatz zur reinen Logikprogrammierung) auch • prozedural • mit Seiteneffekten und • mit globalen Variablen (realisiert mit Hilfe von assert und retract) programmieren. Es gibt umfangreiche Programmbibliotheken und Erweiterungen: • Datenstrukturen und Algorithmen, Kombinatorik, • Datenbank– und Web–Programmierung, • GUI–Programmierung, etc. Prof. Dr. Dietmar Seipel 435 Logik für Informatiker Wintersemester 2015/16 Anwendungsbereiche • regelbasierte Diagnosesysteme (Medizin, Technik) • symbolische Informationsverarbeitung, Parsing • Datenbanken mit komplexen Strukturen (Hierarchien, X ML) • Datenintegration • Semantic Web • Default Reasoning • kombinatorische Suchprobleme (Graphenprobleme, Spiele wie Sudoku oder Minesweeper, etc.) Prof. Dr. Dietmar Seipel 436 Logik für Informatiker Wintersemester 2015/16 Weitere Veranstaltungen Sommersemester: Master • Deduktive Datenbanken: P ROLOG, DATALOG, SLD–Resolution, Auswertungsmethoden, . . . • Datenbanken 2 / Advanced Databases: Data Warehousing, Data Mining, X ML, Semantic Web, Ontologien, . . . Wintersemester: Bachelor • Datenbanken Prof. Dr. Dietmar Seipel 437 Logik für Informatiker Wintersemester 2015/16 Literatur 1. U. Schöningh: Logik für Informatiker. Spektrum Verlag, 5. Auflage, 2000. 2. H.–D. Ebbinghaus, J. Flum, W. Thomas: Mathematical Logic. Springer, 2nd Edition, 1994. 3. J.W. Lloyd: Foundations of Logic Programming. Springer, 1987. 4. W.F. Clocksin, C.S. Mellish: Programming in P ROLOG, Springer, 5th Edition, 2003. 5. I. Bratko: P ROLOG – Programming for Artificial Intelligence. Addison–Wesley, 4th Edition, 2011. Prof. Dr. Dietmar Seipel 438