Schoening - Logik Für Informatiker
Schoening - Logik Für Informatiker
Schoening - Logik Für Informatiker
5. Auflage
WoIfram Schwabkausep.
( 1931 - 1985)
in dankbarer Erinnenrng
SchBning, Uwe:
Logik für Informatiker I von Uwe Schlining. - 5 . Aufl.
- Hcidclbeg ; Berlin :Spektrum, Akad Verl., 2000
(Spektrum-HochschuItaschenbuch)
ISBN 3-8274- 1005-3
Der Vcrlag und der Autor haben alle Sorgfall walten lassen, um vollstindige und akkuratc Infor-
mationcn in diesem Buch zu publizieren. Der Verlag obernimmt weder Garantic noch dicjuri~ti-
schl: Verantwortung oder igendeinc Haftung für die Nutzung dieser Informationen, flir deren
Wirtschaftlichkeit uder fehlerfreie Funktion für einen besrimrnien Zweck. Der Verlag Uber-
nimint kcinc Gewahr dafür, d a s die bcschricbcncn Verlahren, Programme usw frei von Schuiz-
rechten Dntter sind.
Allc Rechte, insbesondere die der Uhcrsctzung in fremde Sprachen, sind vorbehalten. Kein Teil
des Buches darf ohnc schriftliche Genehmigung des Verlages photokopiert odcr in irgendcincr
anderen Form reproduziert oder in eine von Maschinen i~erwentlbarcForm uhcrtragcn ndcr
ubcrsetn werden.
Der dritte Teil Ieitet in die spezielle Art der Resolution über, wie d c im Zusa-
menhang mit Hornfonneln und Logik-Programmiersysternen, 2.B. reaIisiert
in der Programmiersprache PROLOG (Programming in Logic), angewendet
wird. Dieses Buch will jedoch kein Prograrnmierhandbuch fiir PROLOG er-
setzen; Ziel ist es vielmehr, die logischen Grundlagen für das Verständnis der
Logik-Programmierung zu legen. Kapitel 1
Übung 1: "Worin besteht das Geheimnis Ihres Iangen Lebens?" wurde ein
100-jähriger gefragt. "Ich halte mich streng an die Diätregeln: Wenn ich kein
Bier zu einer Mahlzeit trinke, dann habe ich immer Fisch. Immer wenn ich Aussagenlogik
Fisch und Bier zur selben Mahlzeit habe, verzichte ich auf Eiscreme. Wenn
ich Eiscreme habe oder Bier meide, dann rühre ich Fisch nicht an." Der Fra-
gesteller fand diesen Ratschlag ziemlich verwirrend. Können Sie ihn verein-
fachen? 1.1 Grundbegriffe
Überlegen Sie sich, welche formalen Schritte des Vorgehens (Diagramme, Ta-
bellen, Graphen, etc.) Sie für sich selbst eingesetzt haben, um diese Aufgabe In der AussagenIogik werden einfache Verknüpfungen - wie "und", "oder",
zu lösen. Hiermit haben Sie bereits ihre ersten eigenen Versuche unternom- "nicht" - zwischen atomaren sprachlichen Gebilden untersucht. Solche ato-
men, eine formale Logik zu entwickeln! maren Gebilde sind etwa:
14= "Paris ist die Hauptstadt von Frankreich"
D = "Mäuse jagen Elefanten"
Diese atomaren Bestandteile können wahr oder falsch sein (von der inhaltli-
chen Interpretation wissen wir, dass A wahr und B falsch ist). Der Gegenstand
der Aussagenlogik ist es nun festzulegen, wie sich solche "Wahrhei tswerte"
der atomaren Bestandteile zu Wahrheitswerten von komplizierteren sprachli-
chen Gebilden fortsetzen lassen, wie 2.B.
A und B
(Wir wissen, dass im obigen Beispiel A lind B eine fdsche Aussage ist, da
bereits B falsch ist.)
Wir interessieren uns hier also nur dafür, wie sich Wahrheitswerte in kompli-
zierten Gebilden aus den Wahrheitswerten der einfacheren Gebilde ergeben.
In diesen Untersuchungen wird letztlich ignoriert, was die zugrundeliegenden
inhaltlichen Bedeutungen der atomaren Gebilde sind; unser ganzes Interesse
wird auf ihre Wahrheitswerte reduzierz.
Falls 2.B.
A = "Otto wird krank"
B = "Der Arzt verschreibt Otto eine Medizin",
14 KAPITEL 1. A USSAGENLOGTK
so ist es in der Umgangssprache durchaus ein Unterschied, ob wir " A und Man beachte, dass zu diesem Zeitpunkt Formeln lediglich Zeichenreihen
B" oder "B und A" sagen. Von solchen "Feinheiten" befreien wir uns in des (syntaktische Objekte) sind. Sie haben keinen "Inhalt", keine Interpretation.
folgenden Definition, in der Ale denkbaren atomaren Gebilde (jetzt atomare Im Moment ist es nicht zulässig bzw. verfrüht, "A" als " u n d bzw. "V" als
Formeln genannt) ohne eine inhaitliche Interpretation durchnummeriert sind, "oder" zu lesen. Besser wäre etwa "Dach" bzw. "umgekehrtes Dach".
und mit Ar, A2,A3, usw. bezeichnet werden. Eine zugeordnete "Bedeutung" erhalten die Bestandteile von Formeln erst
durch die folgende Definition.
Definition (Syntax der AussagenIogik)
Eine atomare Formel hat die Form Ai (wobei 1: = 1,2,3,. . . ). Definition (Semantik der Aussagenlogik)
Formeln werden durch folgenden induktiven Prozess definiert: Die Elemente der Menge {O,l } heißen Wahrheitswe~e.Eine Relegung ist eine
Funktion A : D -+ (0, I}, wobei D eine Teilmenge der atomaren Formeln
1. Alle atomaren Formeln sind Formeln. ist. Wir erweitern A zu einer Funktion d : E + {0,1), wobei E 2 D die
2. Für alle Formeln F und G sind (F A G) und (F V G) Formeln. Menge aller Fomeln ist, die nur aus den atomaren Formeln in D aufgebaut
sind.
3. Für jede Formel F ist 1 F eine Formel.
1. Für jede atomare Formel il E D ist 4-41
= A(,4).
Eine Formel der Bauart F heißt Negation von F, (FA G) heißt Konjunktion
1
1, falls A ( F ) = o
4 . d ( 1 ~=)
F, ( ( - 4 5 h A s )V y A 3 ) r (-45AAs), A51 A6, 7A31 Aa 0, sonst
Hierbei können Fl,F2,. . . beliebige Formeln sein. Das heißt also, falls wir 0, falls A ( ( AA B)) = 1 oder A(C) = 1
irn Folgenden 2.B. ( A tt E) schreiben, so ist dies eine Abkürzung fiir die
Formel :
= { 1, sonst
0, falls A ( ( AA B)) = 1 (da A(C) = 0)
((AI A As) V ('AI 4 5 ) ) 1, sonst
U, falls J(A) = 1 und A ( B ) = 1 Den Wahrheitswert von F erhalten wir, indem wir zunächst dre Blätter mit
= I, sonst den durch die Belegung gegebenen Wahrheitswerten markieren und dann al-
= 0 le Knoten anhand obiger Verknüpfungstafeln markieren. Die Markierung der
Wurzel ergibt dann den Wahrheitswert der Formel unter der gegebenen Bele-
Wir können die Wirkung der Operationen A, V, 7 durch Verknüpfungstafeln gung.
darstellen.
Übung 2: Man finde eine F o m l F, die die drei atomaren Formeln A, B und
G enthält mit folgender Eigenschaft: Für jede Belegung A : { A ,B , C) 4
( 0 , l ) gilt, dass das Ändern irgendeiner der Werte A(A),A ( B ) ,A(C) auch
A(F) ändert.
Unter Zuhilfenahme dieser Verknüpfungstafeln lässt sich der Wahrheitswert
jeder Formel F leicht bestimmen, wenn eine Belegung derjenigen atoma- Aus der Definition von A(F) lässt sich nun erkennen, dass das Symbol
ren Formeln gegeben ist, die in F enthalten sind. Wir betrachten wieder "A" das umgangssprachliche Wort "und, "V" das "oder" und das Wort
"7"
F = - ( ( A /\ B) V C},und stellen die Art und Weise, wie F aus ernfacheren "nicht" modelliert. Wenn wir noch die Symbole "+" und "H" hinzuneh-
Teilfonneln aufgebaut ist, durch eine Baumstruktur dar: men, die wir als syntaktische Abkurzungen eingeführt haben, so steht "-+"
für "impliziert", "daraus folgt" bzw. "wenn dann", während "H" für "genau
dann wenn" steht.
Um das Ausrechnen von Wahrheitswerten einfacher zu gestalten, wenn die
Formel die (Abkürzungs-) Symbole "+"oder "++" enthalt, können wir hier
ebenfalls Verknüpfungstafeln verwenden.
20 KAPITEL I . AUSSAGENLOGTK I . I . GRUNDBEGRIFFE
2. ((AF~
Fi)+ G) ist eine Tautologie.
3. ((/$=, Fi)
/\ -G) ist unerfüllbar.
Die zu F gehörende Spalte enthäIt nur Einsen, also ist F eine Tautologie.
Übung4: Was ist falsch an folgendem Schluss :
"'Wenn ich lOOm unter 10,O Sekunden laufe, werde ich zur Olympiade zuge-
Bemerkung: Die Wahrheitstafelmethode gibt uns also ein algorithmisches
lassen. Da ich die lOOm nicht unter 10,0 Sekunden laufe, werde ich folgIich
Verfahren in die Hand, die Erfüllbarkeit einer Formel festzustellen. Jedoch
nicht zur Olympiade zugeIassen."
beachte man, dass der Aufwand hierzu gewaltig ist: Für eine Formel mit n
atomaren Fomeln müssen 2" Zeilen der Wahrheitstafel berechnet werden.
Der Wahrheitswert einer Formel F unter irgendeiner zu F passenden Bele- Für eine Formel mit 2.B. 100 atomaren Formeln wäre auch des schnellste exi-
gung A hängt offensichtlich nur von den in F vorkommenden atomaren For- stierende Rechner Tausende von Jahren beschäftigt. (Man rechne sich einmal
meln ab. Das heißt formaler ausgedrückt, dass A ( F ) = A1(F)für alle zu F aus, wie viel 210%Miosekunden sind - angenommen eine Zeile der Wahr-
passenden Belegungen A und At gilt, sofern A und A' auf den in F vorkorn- heitstafel kann in einer Mikrosekunde berechnet werden). Dieses sogenann-
menden atomaren Formeln übereinstimmen. (Ein formaler Beweis müsste Per te Exponentialverhalten der Rechenzeit scheint auch durch raffiniertere Al-
Induktion iiber den Formelaufbau von F geführt werden!). gorithmen nicht einzudämmen zu sein (höchstens in EinzeIfallen), denn das
Das Fazit, das wir ziehen können, ist, dass es zum Feststellen der Erfüllbarkeit Erfüllbarkeitsproblem für FormeIn der Aussagenlogik ist "NP-vollständig".
bzw. der Gültigkeit einer Formel F genügt, lediglich die endlich vielen Bele- (Dieser Begriff kann hier nicht erläutert werden, dies ist Thema der Kom-
gungen, die genau auf den in F vorkommenden atomaren Formeln definiert plexi tätstheorie).
sind, zu testen. Falls F TL verschiedene atomare Fomeln enthält, so sind dies
genau 2" viele zu testende Belegungen. Systematisch können wir dies mittels
Übung 5: Man zeige: Eine Formel F der Bauart
Wahrheitstafeln tun:
-
ist erfüllbar, genau dann wenn die Menge M = {G1,. . , G k ] erfüIlbar ist.
Gilt dies auch für Formeln der Bauart
k
F=(~G,)?
1=1
Ubung 6: Wie viele verschiedene Formeln mit den atomaren Formeln Al: A2,
Hierbei ist F offensichtlich etfüllbar, falls der Wahrheitwerteverlauf von F . . . , An und verschiedenen Wahrheitswerteverlänfen gibt es ?
(die Spalte unter F}mindestens eine 1enthält, und F ist eine Tautologie, fails
der Wahrheitswerteverlauf von F nur aus Einsen besteht.
Übung 7: Man gebe eine dreielementige Formelmenge M an, so dass jede
zweielementige Teilmenge von M erfüllbar ist, M selbst jedoch nicht.
BeispieI: Es sei F = (-A -+ { A + B)).
Es ist praktikabler, für jede in F vorkommende Teilforme1 den jeweiligen Übung 8: Ist folgende unendliche Formelrnenge M erfüllbar?
Wahrheitswerteverlauf in einer Extra-Spalte zu ermitteln.
22 KAPITEL 1 . AUSSAGENLOGIK
Übung 9: Man konstruiere Wahrheitstafeln für jede der folgenden Formeln: 1.2 Äquivalenz und Normalformen
( ( AA B) A (-7BV C ) )
l ( 7 A Y l(7B V TA))
Aus der Art und Weise, wie wir Formeln interpretieren, wissen wir, dass
IA * (B C)) (FA G) und (G A F) "dasselbe bedeuten" -obwohl sie syntaktisch gesehen
verschiedene Objekte sind. Diese semantische Gleichheit oder Äquivalenz er-
Übung 10: Man beweise oder gebe ein Gegenbeispiel: fassen wir mit folgender Definition.
(a} Falls (F-+ G) gültig ist und F gültig ist, so ist G gültig.
Definition
(b) Falls (F -+ G) erfüllbar ist und F erfüllbar ist, so ist G erfüllbar.
Zwei Formeln F und G heißen (semantisch) äquivalent, faIIs für alle Bele-
(C) Falls (F + G) gültig ist und F erfüllbar ist, so ist G erfüllbar. gungen A, die sowohl für F als auch für G passend sind, gilt A(FJ= ACG).
Hierfür schreiben wir F Y G.
Übung 11:
(a) Jeder, der ein gutes Gehör hat, kann richtig singen. Bemerkung: Auch Formeln mit verschiedenen Atomformeln können äquiva-
lent sein (2.B. Tautologien).
(b) Niemand ist ein wahrhafter Musiker, wenn er nicht seine
Zuhörerschaft begeistern kann. Satz (Ersetzbarkeitstheorem)
(C) Niemand, der kein gutes G e h ~ hat,
r kann seine Zuhörerschaft be- Seien F und G äquivalente Formeln. Sei H eine Formel mit (mindestens)
geistern. einem Vorkommen der Teilfomel F. Dann ist H äquivalent zu H', wobei H'
aus H hervorgeht, indem (irgend) ein Vorkommen von F in H durch G ersetzt
(d) Niemand, außer einem wahrhaften Musiker, kann eine Sinfonie wird.
schreiben.
Beweis (durch Induktion über den Formelaufbau von H):
Frage: Welche Eigenschaften muss jemand notwendigerweise besitzen, wenn
er eine Sinfonie geschrieben hat? Induktionsanfung: Falls H eine atomare Formel ist, dann kann nur H = F
Formalisieren Sie diese Sachverhalte und verwenden Sie Wahrheitstafeln! sein. Und damit ist Mar, dass H äquivaIent zu H' ist, denn H' = G.
Induiciionsschrirt: Falls F gerade H selbst ist, so tnfft dieselbe Argumentation
Übung 12: Sei (F t G) eine Tautologie, wobei F und G keine gemeinsamen wie im Induktionsanfang zu. Sei also angenommen, F ist eine Teilformel von
atomaren Formeln haben. Man zeige: dann ist entweder F unerfüllbar oder G H mit F # H. Dann müssen wir 3 Fälle unterscheiden.
eine Tautologie oder beides. Fall I : H hat die Bauart H = -Hl.
Nach Induktionsvoraussetzung ist H j äquivalent zu H:, wobei H ; aus Hl
Übung 13: (Craigscher Interpolationssatz) durch Ersetzung von F durch G hervorgeht. Nun ist aber H' = TH:. Aus der
+
Es gelte (F+ G) und es gibt mindestens eine atomare Formel, die sowohl (semantischen) Definition von
Fall 2: H hat die Bauart H = (Hl
"7" folgt dann, dass H und H' qrtquivrtlent sind.
V Hz).
in F als auch in G vorkommt. Man beweise, dass es eine Formet H gibt,
die nur aus atomaren Formeln aufgebaut ist, die sowohl in F als auch in G Dann kommt F entweder in ]II oder H? vor. Nehmen wir den ersteren Fall an
vorkommen, mit (F + H) und t= (H -+ G ) . (der zweite ist völlig analog). Dann ist nach Induktionsannahme Hl wieder
Hinweis: Induktion über die Anzahl der atomaren Formeln, die in F, aber äquivalent zu H:, wobei H: aus HI durch Ersetzung von F durch G hervor-
nicht in G vorkommen. Andere Möglichkeit: Konstruieren einer Wahrheitsta- =
geht. Mit der Definition von "V" ist dann klar, dass H ( H ; V H 2 ) = H'.
fel für H anhand der Wahrheitstafeln von F und G. Fall 3: H hat die Bauart H = ( H 1A Hz).
Diesen Fall beweist man völlig analog zu Fall 2.
1.2. Ä Q U I V R L E ~ UNDNORMALFORMEN 25
Übung 14: Es gelte F G. Man zeige: Beispiel: Mittels obiger Äquivalenzen und des Ersetzbarkeitstheorems (ET)
Wenn F' bzw. G' aus F bzw. G hervorgehen, indem alle Vorkommen von A können wir nachweisen, dass
durch V und umgekehrt ersetzt werden, so gilt: F' G'.
( ( AV ( B V C ) )A (C V Y A ) )E ((BATA) V C }
Satz
Übung 17: Man zeige sowohl durch Wahrheitstafeln als auch durch Anwen-
dung obiger Urnfomungsregeln, dass ( ( AV l ( B A A ) ) h (C V (D V C))) Fur jede Fonnel F gibt es eine Quivalente Formel in KNF und eine äquiva-
äquivalent ist zu (C V D). lente Formel in DNF.
(a) "Wenn das G n d fiebrig ist oder stark hustet und wir erreichen Induktionsschrits:Wir unterscheiden wieder 3 Fälle.
den Arzt, so rufen wir ihn." Fall I : F hat die Form F = -G
Dann gibt es nach Induktionsannahme zu G aquivalente Formeln GIin KNF
(b) "Wenn &s Kind fiebrig ist, so rufen wir den Arzt, falls wir ihn und Gq in DNF. Sei n m,
erreichen, und, wenn wir de~iArzt erreichen, so werden wir ihn, G1 = ( A ( V J;„)).
wenn das Kind stark hustet. rufen." 1=1 3=1
Definition (Normalfomen) F E (V ( A l L i , j ) l T
i=l 3=1
Ein Litera! ist eine atomare Formel oder die Negation einer atomaren For-
mel. (Tmersten Fall sprechen wir von einem posiriven, im zweiten von einem woraus wir mittels des Doppelnegationsgesetzes erhalten:
negativen Literal).
Eine Forme1 F ist in konjunktiver NomtaEfom (KNF), fails sie eine Konjunk-
tion von Disjunktionen von Literalen ist:
Ak falls LiJ = 7 A k
wobei ¿,j = 7Ak fallsLij=Ak.
Fall 2: F hat die Form F = (G Y H). 1. Ersetze in F jedes Vorkommen einer Tei lfomel der Bauart
Nach der Induktionsannahme gibt es zu G und H jeweils äquivalente Formeln
in KNF und in DNF. 1 1 G durch G,
Um eine zu F äquivalente Formel in DNF zu erhalten, verknüpfen wir die -$GA H) durch (1GV -.H) ,
DNF-Formeln zu G und H mittels V. Mehrfaches Anwenden des Assoziativ- T(G V H ) durch (-3 A T H ) ,
gesetzes liefert schließlich die gewünschte Linksklammerung.
Umeine zu F äquivalente KNF-Formel zu erhalten, wähle man zunächst nach bis keine derartige Teilformel mehr vorkommt.
Induktionsannahme zu G und H äquivalente Formeln in KNF.
2. Ersetze jedes Vorkommen einer Teilfomel der Bauart
( F V (GJ\ H ) ) durch ( ( FV G ) A ( F V H ) ) ,
((FA G) V H) durch ((FV H ) A (GV W)),
bis keine derartige Teilfom~elmehr vorkommt.
Hierbei sind die G, und H1 Disjunktionen von Literalen. Mittels (verallgemei- Die resultierende Formel ist nun in KNF (es kommen evtl. nwh übedlüsnge,
nerter) Drstributivität (vgl. Übung 16) und Assoziativität erhalten wir dann: aber zulässige Disjunktionen vor, die Tautologien sind).
Eine weitere Methode zur Herstellung von KNF bzw. DNF bietet sich an,
sofern von der Formel F eine Wahrheitstafel vorliegt.
In diesem Fall kann eine DNF- oder KNF-Formel sozusagen direkt abgelesen
Durch weitere Anwendung des Assoziativgesetzes erhält diese Formel die werden. Um eine zu F aquivalente DNF-Fomel zu erhalten, gehe man wie
gewünschte Bauart folgt vor: Jede Zeile der Wahrheitstafel mit Wahrheitswert 1 tragt zu einem
n-k
Konjunktionsglied bei. Die Literale dieser Konjunktion bestimmen sich wie
F (S\ F;) folgt: Falls die Belegung von A, in der betreffenden Zeile 2 ist, so wird Ai als
a=1 Uteral eingesetzt, sonst -A,.
wobei die F, Disjunktionen von LiteraIen sind. Evtl. vorkommende identische Um eine zu F aquivalente KNF-Formel zu erhalten, vertausche man in obiger
Disjunktionen, oder identische Ljterale innerhalb einer Disjunktion können Anleitung die Rollen von 0 und 1, sowie von Konjunktion und Disjunktion.
nun mittels der I&mpotenzgesetze eliminiert werden.
Falls einige Disjunktionen Tautologien darstellen (2.B. CA,v~A,)),so können Beispiel: Eine Formel F habe die Wahrheitstafel
diese noch mittels der Tautologieregel beseitigt werden. Damit erhalten wir
eine zu F kquivalence Formel in KNF.
Fall 3: F hat die Form F = (G A H).
Der Beweis verläuft sinngemäß zu Fall 2. m
( ( T A+ B ) A ( ( A A -C) +t B)).
1.3 Hornformeln
Einen in der Praxis wichtigen und haufig auftretenden Spezialfall stellen die
Man beachte, dass die DNF- oder W-Formeln, die mit obigen Methoden Hornfomeln dar (benannt nach dem Logiker Alfred Horn).
erzeugt werden, nicht notwendigerweise die kürzestmöglichen sind. Dieses
Problem, möglichst kurze konjunktive oder disjunktive Normalformen einer
gegebenen Fomel herzustellen, ist vor altem für die Digitaltechnik interessant Definition (Hornfarmeln)
und soll hier nicht behandelt werden. Eine Formel F ist eine Homfomel, falls F ~n KNF ist, und jedes Disjunkti-
Man beachte ferner, dass der Urnformungsprozess in eine KNF- oder DNF- onsglied in F höchstens ein positives Litera1 enthält.
Fomel diese exponentiell aufblahen kann. Aus einer Ausgangsfomel der
Länge n kann bei diesem Umforrnungsprozess eine Formel entstehen, deren Beispiel: Eine Hornfomel ist:
Länge in der Gr~ßenordnungvon 2" liegt. Der Grund liegt in der Anwendung
des Distributivgesetzes, welches die Formellänge in etwa verdoppelt. Eine F = ( A V T B )h (-CY T A v D ) A ( 1 . 4 ~ - B )A D A T B
Fonnel mit kurzer DNF-DarsteIlung hat i.a. eine lange KNF-Darstellung und
Keine Hornfomel ist:
umgekehrt.
G = (-4V T B )A ( C V - r l V D).
Übung 20: Man zeige, dass es zu jeder Formel F eine (effizient konstntierba-
re) Femel G in KNF gibt, so dass jedes Konjunktionsglied von G höchstens
3 Literale enthält, und es gilt: F ist erfüllbar genau dann, wenn G erfüllbar Hornformeln können anschaulicher als Konjunktionen von ImpIikationen ge-
ist. (Es ist also nicht die Äquivalenz von F und G behauptet!). Ferner ist die schrieben werden (prozedurale Deutung). Im obigen Beispiel ist
Länge von G linear in der Länge von F. (Es liegt hier aIso kein exponentielles
Aufblähen vor). F (B+ A) A ( C A A i D)A ( A A B i O ) A (1 i D ) A ( E -+ 0).
Hinweis: Die atomaren FormeIn von G bestehen aus denjenigen von E und Hierbei steht 0 für eine beliebige unerfüllbare Fomel und 1 für eine beliebige
zusätzlichen atomaren Formeln, die jeweils den inneren Knoten des Stmktur- Tautologie. Man mache sich anhand von &ung 3 und der Definition von "+"
baums von F zugeordnet sind. klar, dass die obige Formel tatsächlich äquivalent zu F ist.
32 KAPITEL 1 . AUSSAGErnOGIK
Ein Gmndthema dieses Buches ist die Frage nach einem algorithmischen Test eine Disjunktion, wie im Schritt 1, nur aus einem positiven Litera1 besteht, so
fLir die Gültigkeit oder Erfullbarkei t einer gegebenen Formel. Es genügt, sich muss dieses notwendigerweise mit 1 belegt werden. Damit ergibt sich auch
auf Unerfüllbarkeitstesis zu beschränken, da eine Formel F giiltig ist genau die Notwendigkeit, Ern Schritt 2 alle atomaren Formeln B mit 1 zu belegen,
dann, wenn 1F unerfüllbar ist. (Um die Gültigkeit von F festzustellen, gebe -
sofern (Al /\. . A A, -+ B) in F vorkommt, und A i , . . . , An bereits markiert
man einfach 1 F in einen Unerfüllbarkeitstest ein). sind. Diese Uberlegung zeigt auch, dass im Schritt 2 korrekterweise "unerfüll-
Die Erfüllbarkeit oder UnerfüIlbarkeit von aussagenlogischen Formeln likst bar" ausgegeben wird, sofern (Al A - . /\An t 0) vorkommt und Al, . .. , An
4
sich grundsätzlich immer, jedoch i.a. nur mit großem Aufwand, mittels Wahr- markiert sind.
heitstafeln durchführen. Falls der Markierungsprozess in Schritt 2 erfolgreich zu Ende kommt, so lie-
Für Hornfomleln gibt es jedoch einen sehr effizienten Erfüllbarkeitstest, der fert Schritt 3 korrekterweise die Ausgabe "erfüllbar" und die Markierung Iie-
wie folgt arbeitet: fert ein entsprechendes Modell .d für F.
Eingabe: eine Homfomel F, Dies sieht man wie folgt: Sei G ein beliebiges Disjunktionsglied in F. Falls G
eine atomare Formel ist, so wird bereits in Schritt 1 A(G) = 1 gesetzt. Falls
1. Versehe jedes Vorkommen einer atomaren Formel A in F mit einer G die Form (Al A . A An + B) hat, so sind entweder alle atomaren Formeln
+ +
Markiening, falls es in F eine Teilformel der Form (1 -+ -4) gibt; in G, insbesondere B, mit 1 belegt (wegen Schntt 2) und damit A(G) = 1,
oder für mindestens ein j mit 1 5 j 5 n giIt A(A,) = 0. Auch in diesem
-
2. whik es gibt in F eine Teilformel G der Form (AI ri . A An t B)
+ Fall folgt A(G) = 1.Falls G die Form (Al A . . . A An + 0) hat, so muss
--
oder (AI A . A -4, + 0 ) , n 2 1, wobei A l , . . . , An bereits für mindestens ein J' mit 1 5 j 5 TI, gelten A(A,) = O (da in Schritt 2 nicht
markiert sind (und B noch nicht markiert ist) do "unerfüllbar" ausgegeben wurde), und damit folgt gleichfalls A(G) = 1. i
if G hat die erste Form then
markiere jedes Vorkommen von B Man beachte, dass aus dem obigen Beweis hervorgeht, dass der Markierungs-
else gib "unerfullbar" aus und stoppe; algorithmus das kleinste Modell A für F konstniiert (falls existent).Das heißt,
3. Gib "erfidlbar" aus und stoppe. (Die erfullende Belegung wird hierbei dass für alle Modelle A' und alle atomaren Formeln B rn F gilt: A ( B ) <
durch die Markierung gegeben: A(Ae) = I gdw. A, hat eine Marke- d l ( B ) (Eherbei
. ist die Ordnung O < 1vorausgesetzt).
mngl. Weiterhin beobachten wir, dass jede H ~ r n f o m eerfüllbar
l ist, sofern sie keine
Teilforme1 der Bauart (Al h . . . A A , + 0) enthält. Es sind genau diese
Teilfomeln, die in Schritt 2 möglicherweise zu der Ausgabe "unerfüllbar"
Satz führen. (Wir werden diese Klauseln später Zielklausekn nennen).
Obiger Markierungsalgorithmus ist (für Hornfometn als Eingabe) korrekt Gleichfalls ist jede Bornformel erfüllbar, sofern sie keine Teilfomel der Form
und stoppt immer nach spätestens n Markierungsschritten (n = Anzahl der (1+ A) enthält. In diesem Fall würde die while-Schleife nicht betreten wer-
atomaren Formeln in F). den.
Beweis: Zunächst ist es klar,dass nicht mehr atomare Formeln markiert wer-
Übring 21: Man wende den Markierungsalgori thmus auf die Formel
den können als vorhanden sind, und deshalb nach spätestens n Markierungs-
schritten entweder die Ausgabe "erfiillbar" oder "unerfüllbar" erreicht wird.
Zur Korrektheit des Algorithmus' beobachten wir zunächst, dass für jedes
Modell A für die Eingabeformel F (sofern überhaupt ein Modell für F exI- an. (Man beachte, dass die Wahrheitstafel für diese Formel 2% 64 Zeilen
stiert) gilt, dass für die im Laufe des Verfahrens markierten atomaren Formeln hat!)
A, d ( A , ) = 1 gelten muss . Dies ist unmittelbar einleuchtend im Schritt I des
Algorithmus', da eine KNF-Formel nur dann den Wert 1 unter einer Belegung
ijbung 22: Man gebe eine Formel an, zu der es keim gqiquivalenteHornfomel
A erhalten kann, wenn alle ~ i s j u n k t k n e nden Wert 1 unter A erhalten. Falls
gibt und begninde, warum dies so ist.
34 KAPITEL I . AUSSAGENLOGIK
1.4 Endlichkeitssatz
Stufe n > 0:
Wir werden in diesem Abschnitt einen wichtigen Satz beweisen, dessen Be-
deutsamkeit vielleicht im Moment noch nicht einleuchten wird. Ern zweiten if es gibt unendlich viele Indizes i E I
Kapitel wird dieser Satz jedoch eine wichtige Rolle spielen. mit A;(A,) = 1 then
begin
Satz (Endlichkeitssatz, compactness theorem) d := A U {(A„ I)};
I := I - {i 1 &(An) # I}
Eine Menge M von Formeln ist erfüllbar genau dann, wenn jede der endlichen end
Teilmengen von M erfüllbar ist. else
begin
Beweis: Jedes Modell für M ist trivialesweise auch ein Modell für jede be-
d := A U {(Am 0));
liebige Teilmenge von M, insbesondere auch für jede endliche. Die Richtung
I := I - {?1 &(An) # (I}
von links nach rechts ist also klar. end.
Sei also umgekehrt angenommen, dass jede endliche TeiImenge von M erfüll-
bar ist, also ein Modell besitzt. Unsere Aufgabe besteht nun darin, aus dieser Da in jeder Stufe n die Belegung A entweder um (Am0) oder (An: 1) (aber
Vielzahl von Modellen für die endlichen Teilmengen ein einziges Modell für nie beides) erweitert wird, ist A eine wohldefinierte Funktion mit Definitions-
>
M zu konstruieren. Für jedes n 1 sei M, die Menge der Formeln in M, die bereich {.4,, A2,AB,. . .} und Wertebereich (0,l).
nur die atomaren Formeln A l , . .. , An enthalten. Obwohl M, im Allgemei-
nen eine unendliche Menge sein kann, gibt es höchstens k 5 22n verschie- Wir zeigen nun, dass A ein Modell für M ist. Sei also F eine beliebige Formel
dene Formeln Fl, . . . , Fk in M„ die paarweise zueinander nicht äquivalent in M. In F können nur endlich viele atomare Formeln vorkommen, sagen wir
sind, denn es gibt genau 22n verschiedene Wahrheitstafeln mit den atomaren bis zum Index I , also A l , A Z ,. . . , Ai. Das heißt also, F ist Element von MI C
Formeln A l , . . . , An. MI+, . . - und jede der Belegungen AI,A M I , . . ist Modell für F. Die
Mit anderen Worten, für jede Formel F E M, gibt es ein i 5 k mit F = F%. Konstruktion von A ist nun so angelegt, dass in jeder Stufe die Indexmenge
Jedes Modell fdr (fi, . . . , F k ) ist somit auch Modell für M,. Nach Voraus- I zwar "ausgedfinnt" wird, dass aber I nie endlich werden kann. Das heißt,
setzung besitzt { F l , . . . , Fk} ein Modell, denn diese Menge ist endlich. Wir auch nach Stufe L verbleiben unendlich viele Indizes i in I, natürlich auch
nennen dieses Modell &. Wir bemerken ferner, dass An gleichfalls Modell solche mit i 2 I. Für all diese i gilt: A,(Ai)= A(ill), - . . :A,(PII)= A(Al),
für MI, Mz, . . . , M,-1 ist, denn MI C . . - M,-, C M,. Das gesuchte und deshalb ist A Modell für F. m
36 KAPITEL 1 . AUSSAGENLOGIK 2.5. RESOLUTION 37
Man beachte eine Besonderheit im obigen Beweis: er ist nicht-konstruktiv. wobei für n = 1,2,3,. . . gilt: (Fwi+ F,) und F (F, + Man
Die Existenz des Modells A wird durch den Beweis zwar gezeigt, aber die zeige: M ist nicht endlich axiomatisierbar.
if-Bedingung in der "Konstruktion" ist nicht algofithmisch in endlicher Zeit
nachprüfbar. Das heißt, es gibt keinen Algorithmus, der A tatsächlich effektiv obmg 27: Sei L eine beliebige unendliche Menge von natürlichen Zahlen,
konsmiiert. Es ist lediglich eine gedankliche Konstruktion: entweder ist die dargestellt als Binärzahlen. (Zum Beispiel die Primzahlen: L = {10, 11, 101,
if-Bedingung erfüllt oder ihr Gegenteil, und dementsprechend soll die "Kon- I11, 10L1, . . .}). Man beweise, dass es eine unendIiche Folge W , wz7w3,. . .
struktion" fortfahren; "programmieren" können wir dies allerdings nicht. von paarweise verschiedenen Binärzahlen gibt, so dass ru, Anfangsstück von
Auf andere Weise formuliest besagt der EndIichkeltssatz, dass eine (evtl. un- w , + ~und von mindestens einem Element aus L ist (i = 1T 2 , 3 , . . .) .
endliche) Fomelmenge M unefilibar ist genau dann, wenn bereits eine end-
liche Teilmenge M' von M unerfüllbar ist. In dieser Form werden wir den
Endlichkeitssatz später anwenden (Kapitel 2.4).
Diese Anwendung des Endlichkeitssatzes geschieht in folgendem Zusammen- 1.5 Resolution
hang: Nehmen wir an, die Formelmenge M kann durch einen algorithmischen
Prozess aufgezählt werden (m.a.W., M ist rekursiv aufz'zrihlbar): Die Resolution ist eine einfach anzuwendende syntaktische Umformungs-
regel. Hierbei wird in einem Schritt aus zwei Formeln, sofern sie die Vor-
aussetzungen für die Anwendungen der Resolutionsregel erfüllen, eine dritte
Dann kann die Unerfüllbarkeit von M so getestet werden, dass immer größere
Formel generiert, die dann als Eingabe in weitere Resolutionsschntte dienen
endliche Anfangsabschnitte von M erzeugt werden und auf Unerfüllbarkeit
kann, usw.
getestet werden. Aufgmnd des Endlichkeitssatzes ist M unerfüllbar genau
dann, wenn dieser so beschriebene Algorithmus irgendwann Erfolg hat. Eine Kollektion solcher rein "mechanisch" anzuwendender syntaktischer
Umfomungsregeln nennen wir einen Kulkül. Kalkule bieten sich wegen ihrer
Man beachte, dass ein ähnlicher Test für die Erfii'llbarkeit nicht unbedingt einfachen mechanistischen Arbeitsweise direkt für die algorithmische Tmple-
existieren muss (und im Allgemeinen tatsächlich nicht existiert).
mentiemng per Computer an. Im Falle des Resolutionskalkiils gibt es sogar
nur eine einzige Umformungsregel, die wir weiter unten beschreiben werden.
Übung 24: Sei M eine unendliche Formelmenge, so dass jede endliche Teil- Die Definition eines Kalküls hat nur dann einen Sinn, wenn man dessen Kor-
menge von M erfüllbar ist. In keiner Formel F E M komme die atomare rektheit und Irollstir'ndigkeit (in Bezug auf die betrachtete Aufgabenstellung)
Formel A723 vor, und daher sei angenommen, dass keines der Modelle & in nachweisen kann.
der Konstruktion des Endlichkejtssatzes auf A723definiert ist. Man gebe an,
Die zupndeliegende Aufgabenstellung soll hier darin liegen, die Une@ll-
welchen Wert ATZ3dann unter der imEndlichkeitssatz konstruierten Belegung
barkeit einer gegebenen Fomelmenge nachzuwe~sen.Korrektheit bedeutet
A erhält.
dann, dass keine erfüllbare Formelmenge durch den Kalkül als vermeintlich
werfüllbar nachgewiesen werden kann, und VoIlstSndigkeit bedeutet umge-
Übung 25: Man beweise (unter Verwendung des Endlichkeitssatzes), dass kehrt, dass jede unerfüllbare Pomelmenge durch den Kalkül als solche nach-
M = { F17F*,F3,. . .} erfülIbar ist genau dann, wenn für unendlich viele n, gewf esen werden kann.
F,) erfülIbar ist. Wie schon enviihnt, können wir uns auf Unerfüllbarkeitstests beschränken,
denn viele andere Aufgabenstellungen können auf einen Unerfüllbarkeitstest
Übung 26: Eine Formelmenge Mo heißt ein Axiornensystem für eine Formel- zurückgeführt werden: Um z.B. zu testen, ob eine Formel F eine Tautologie
menge M, falls ist, genügt es T F auf Unerfüllbarkeit zu testen. Eine noch häufiger vorkom-
{AlA ist Modell für Mo} = {AlA ist Modell für M). mende Fragestellung ist: Folgt die Formel G aus einer gegebenen Formelmen-
ge {Fl,F2,. . .,Fk)?Wir wissen, dass dies gleichwertig ist O u n g 3) mit der
M heißt endlich axiomatisierbar, fdls es ein eridliches Axiomensystem für M Frage, ob Fl A F2 r\ . . - A FkA 1G unerfüllbar ist, und damit haben wir obige
F3,. . .} ein Axiomensystem für eine gewisse Menge M,
gibt. Es sei { F ! ,.FJ7 Frage wieder auf einen Unerfüllbarkeitstest zurückgeführt.
38 KAPITEL I . A USSAGENCOGlK 1.5. RESOLUTION
Voraussetzung für die Anwendung der Resolution ist, dass die Formel (oder Hierbei ist definiert als
Formelmenge) in KNF vorliegt, d.h. dje Formel muss gegebenenfalls erst in
KNF umgeformt werden (vgl. hierzu auch Ubung 20). Sei also i,4, falls L = Ai ,
Ai falls L = 7-4,
- -
wobei die L„ Literale sind, also L,, E {AI, A2, . U {T&, l A Z , . .).
+)
Wir stellen diesen Sachverhalt durch folgendes Diagramm dar (Sprechweise:
R wird aus K,, K2 nach L resolviert).
Für die Anwendung der Resolution ist es vorteilhaft, Formeln in KNF als
Mengen von sog. Klauseln darzustellen:
Jedes Element von F, welches wiederum eine Menge ist, heißt Klausel. Die
Klauseln (deren Elemente die Literaie sind) entsprechen nun also den Dis-
junktionsgliedern. Wir vereinbaren ferner, dass die leere Menge, die ebenfalls als Resolvent auf-
treten kann (falls K1 = ( L ) und K2 = {¿} für ein Litera1 L) mit dem spe-
Da die Elemente einer Menge keine Rangordnung haben, und mehrfach auf-
ziellen Symbol bezeichnet wird. Dieses Symbol wird verwendet, um eine
tretende Elemente zu einem einzigen Element verschmelzen, sind Vereinfa-
unerfüIlbare Formel zu bezeichnen. Eine Klauselmenge, die 17 als Element
chungen, die sich durch Assoziativität, Kornmntativität oder Idernpotenz er-
enthält, wird somit (per Definition) als unedüllbar erklärt.
geben, sozusagen "automatisch" bereitgesteiit durch die Mengennotation.
Es folgen einige Beispiele für Resolutionen.
Die folgenden, äquivalenten KNF-Formeln besitzen alle dieselbe Mengen-
darstellung, nämlich {{A3),{Al, lA2}}:
(A3, T A ,A i )
V
l A ~ )
4 1 -417
(443 A (742 V Ai))
(A3 A ((742 V 4 2 ) V Ai))
USW.
Es ist aus dem bisher Gesagten nun klar, dass eine KFauselmenge unerfüllbar
ist genau dann, wenn eine Deduktion der leeren Klausel aus F exrstiert. Um
zu beweisen, dass eine Mauselmenge F unerfüllbar ist, genagt es also, eine
und somit folgt E Resm(F). U Deduktion der leeren Klausel aus F anzugeben, es müssen nicht alle Klauseln
aus Res*{F)aufgeschrieben werden.
Aus dem Resolutionssatz leitet sich folgender Algoriihmus ab, der von ei-
ner Formel in KNF entscheidet, ob sie erfüllbar ist oder nicht (vgl. hierzu
Beispiel: Es sei F = { { A ,B , T C ) ,( T A } ,{ A ,B, C), { A , 133).F ist un-
Übung 3 1).
erfullbar, denn eine mögliche Deduktion der leeren Klausel aus F ist die Fol-
Eingabe: eine Fomel F in KNF ge K l , . . . ,I& mit
KAPITEL 1. AUSSAGENLOGrK 1.5. RESOLUTION 45
K1 = ( A , B ,-C) (Klausel aus F) Da bei solchen Resolutionen immer nur kürzere Klauseln entstehen können,
K2 = { A , B , C ) (Klausel aus F) lässt sich aus diesem Kalkul ein effizienter Algorithmus für die Klasse der
K3 = (Resolvent von K 1 ,K2) Hornfomeln ableiten - ähnlich effizient wie der Markieningsalgorithmus aus
K4 = { A , l B } (Klausel aus F ) Kapitel 1.3.
& = {Al (Resolveni von G, K4) Hinweis: Man zeige, dass der Ablauf des Markierungsalgorithmus' für Horn-
K6 = { T A ) [Klausel aus F) formeln in gewisser Weise nachvollzogen werden kann durch Anwendung
K7 = (Resolvent von K5, K6) entsprechender Einheitsresotutionen. (Auf eine andere Weise wird diese
Ubung in Kapitel 2.6 gelöst).
Diese Situation kann durch einen Resolutionsgraphe~tpenveranschaulicht wer-
den.
hjbung 36: Sei F eine Klauselmenge mit den atomaren Formeln
A l , .. . ,Am wobel für jede Klausel K E F gilt ( K ( 5 2. Wie groß ist
Res*(F)höchstens? (Für diese Klasse von Klauselmengen oder Formeln, sog.
Kromfomeln, liefert der Resolutionskalkül also wiedemm einen effizienten
Algorithmus).
ist.
venten brauchen nicht betrachtet werden. (Dies ist für die beiden Kanten zwi- echte Teilmenge von G ist erfüllbar), dann benötigt jede Resolutionsherlei-
schen der zweiten und dritten Klausel der Fall). tung der leeren Klausel aus F mindestens [GI - 1 Resolutionsschritte.
mung 38: Gegeben sei folgender Resoluiionsgraph, wobei K1, 16,. . . , K7 Bemerkung: Obwohl, wie wir gesehen haben, der Resolutionskalkül in vie-
Homklauseln sind. len Spezialfallen direkt zu einem effizienten algorithmischen Unerfüllbar-
keitskst führt, muss dies nicht fürjede Formel so sein. Man kann unerfüllbare
Formeln bzw. Klauselmengen angeben, wo jede Deduktion der leeren Klausel
exponentiell viele Klauseln enthält. Das heißt, für diese Klauseln Ist der Auf-
wand für den UnerfGllbarkeitstest per Resolutionskalkul mit dem der Wahr-
heitstafelmethode vergleichbar. Wegen der "NP-Vollständigkeit" des Erfull-
barkeitsproblems scheint hier auch keine prinzipielle Verbesserung möglich
zu sein.
Man beachte ferner die folgende interessante Besonderheit: Man kann sowohl
die Erfüllbarkeit als auch die Unerfiiilbarkeit einer Formel F durch eine &i-
Man zeige, dass dieser Resolutionsbaum "linearisiert" werden kann, und die stenmussuge ausdrücken: F ist (per Definition) erfüllbar, falls eine erfüllen-
Klausel K7auch auf folgende Ari aus Ki, K2, K3,K4 resolviert werden kann, de Belegung existieaiert, und F ist unerfüllbar, falls eine Deduktion der leeren
Klausel existiert. Eine "Asymmetrie" in dieser an sich symmetrisch aussehen-
den Situation besteht jedoch darin, dass das Aufschreiben einer Deduktion
evtl. mit wesentlich (d.h. exponentiell) mehr Aufwand verbunden sein kann
als das Aufschreiben einer Belegung. (Diese Asymmetie hängt eng mit dem
sog. N P =? CO-NPProblem zusamen.)
wobei {il, 22, i3, i d ) = { 1,2 , 3 , 4 ) und K', K" geeignete Klauseln sind.
Übung 39: Eine Klause! heißt positiv [negativ),falls sie nur positive (nega-
tive) Literale enthält. Man zeige, dass jede Klauselmenge erfüllbar ist, wenn
sie keine positive Klausel enthält. (Dasselbe gilt für eine Klauselmenge, die
keine negative Klausel enthalt).
Übung 41: Man zeige: Wenn F eine unerfüllbare Klauselrnenge ist und G
eine minimal unerfüllbare Tetlmenge von F (d.h. G ist unerfüllbar, aber jede
Kapitel 2
Prädikatenlogik
2.1 Grundbegriffe
Die Prädikatenlogik ist eine m e i t e r u n g der Aussagenlogik. Was hinzu
kommt sind Quantoren, Funktions- und Frädikatsymbole. Durch diese neuen
Konzepte sind nun Sachverhalte beschreibbar, die im Rahmen der Aussagen-
logik nicht formuliert werden konnten. Zn der Aussagenlogik war es z.B. nicht
möglich auszudrücken, dass gewisse "Objekte" in gewissen Beziehungen ste-
hen; dass eine Eigenschaftfiir alle Objekte gilt, oder dass ein Objekt mit einer
gewissen Eigenschaft existiert. Ein bekanntes BeispieI aus der Analysis:
Für alle E > 0 glbt es ein no, so dass für alle n. 2 no gilt, dass
abs(f (n) - a) < E .
Die wesentlichen Bestandteile hier sind die sprachlichen Konstmkte "für alle"
und "es gibt", sowie die Verwendung von Funktionen (abs, f , -) und Rela-
tionen (>, >, <).
Wir beginnen wieder wie in der Aussagenlogik damit, dass wir den syntakti-
schen Sprachrahmen abstecken, in dem wir uns in der Prädikatenlogik bewe-
gen wollen. Der Definition von (prädikatenlogischen) Formel~tmuss noch die
Definition von Ternen vorangestellt werden, da sie Bestandteile der Formeln
sind.
2. Falls f ein Funktionssyrnbol ist mit Stellenzahl k, und faIIs ti,. . . , tk fi(~2))
p52(x~~
Terme sind, so ist auch f (tl , . . . ,t k ) ein Term. -Q~2P,?(x2, f?2(f4ai f51(x3)))
V ~ z P , 2 ( ~fZf40,
2 , M.3)))
P42(52!f;(f;, f51(53)))
Hierbei sollen auch Funktionssymbole der Stellenzahl 0 eingeschlossen sein,
und in diesem Fall soilen die Klammem wegfallen. Nullstellige Funktions- AHe in F vorkommenden Terme sind:
symbole heißen auch Konssanten.
Nun können wir (wiederum induktiv) definieren, was Formeln (der Prädika-
tenlogik) sind.
1. Falls P ein Prädikatsyrnbol der Stelligkeit k ist, und falls tl, . . . , tk Ter-
me sind,dann ist P(t,, . . . , t k )eine Fomel.
2. Für jede Formel F ist auch 1 F eine Formel. Alle Vorkommen von slin F sind gebunden. Das erste Vorkommen von x2 ist
frei, alle weiteren sind gebunden. Ferner kommt in F frei vor. Die Formel
3. F& alle Formeln F und G sind auch (FA G) und (FV G) Formeln. ft
F ist also keine Aussage. Der Term stellt eine Konstante dar.
Die Matrix von F ist die Formel
4. FalIs X eine Variable ist und F eine Formel, so sind auch 3xF und V x F F* = (p$(xr, f i ( x 2 ) ) V 7~421x2,f;(f;, fl(x3))))
Formeln.
Übung 42: Sei Frei(F) die Menge der in F frei vorkommenden Variablen.
Atomare Fomela nennen wir genau die, die gemäß 1. aufgebaut sind.
Man definiere Frei(F) formal (per Induktion über den Term- und Eomelauf-
Falls F eine Formel ist und F als Teil einer Formel G auftritt, so heißt F bau von F).
Teilfomei von G .
Wir vereinbaren wieder &e vereinfachenden Schreibweisen wie in der Aus-
Alle Vorkommen von Variablen in einer Formel werden in freie und gebun- sagenlogik. Knzu kommen noch die folgenden:
dene Vorkommen unterteilt. Dabei heißt ein Vorkommen der Variablen X in
der Formel F gebunden, falls z in einer Teilformel von F der Form 3xG oder U , V , W, X, Y,z stehen für Variablen
QxG vorkommt. Andernfalls heißt dieses Vorkommen von z frei. (Dieselbe U , h, C stehen fur Konstanten
Variable kann also in einer Fomel an verschiedenen Stellen sowohl frei aIs f1 s, 11 stehen für Funktionssymbole, wobei die zugehön-
auch gebunden vorkommen). ge Stelligkeit immer aus dem Kontext hervorgeht.
Eine Formel ohne Vorkommen einer freien Variablen heißt geschlossen oder P?Q 1R stehen fLir PrädikatsyrnboIe. Die Stelligkeit geht
eine Aussage. Das Symbol 3 wird Existenzquantor und V Allquantorgenannt. aus dem Kontext hervor.
Die Matrix einer Formel F ist diejenige Formel, die man aus F erhält, in-
dem jedes Vorkommen von 3 bzw. V, samt der dahinterstehenden Variablen Übung 43: Man gebe swtliche TeilformeIn und Terme an, die in der Formel
gestrichen wird. Symbolisch bezeichnen wir die Matrix der Formel F mii F*.
enthalten sind. WeIche TeilformeIn sind Aussagen? Für jedes Vorkommen IA(Q) = Q~ = { n E UA I n ist Primzahl 1
einer Variablen bestimme man, ob es frei oder gebunden ist. Wie lautet die IA(f ) = f = die Nachfolgerfunktion auf UA,
Matrix von F ?
+
also f A ( n ) = n 1,
= g* = die Additionsfunktion auf UA,
Um Formeln der Prädikatenlogik zu interpretieren, müssen die Funktionssym-
bole als gewisse Funktionen, die Wdikatsymbole als gewisse Radikate (je- also gA(rn, n ) = m -n,
i
weih auf einer gewissen Grundmenge) gedeutet werden. Hinzu kommt, dass IA( a ) = aA = 2,
evtl. vorkommende freie Variablen als Elemente der Gnindmenge interpretiert IS1(z) = E* = 3.
werden müssen. All dies wird in der folgenden Definition formal getan.
Definition (Semantik der Prakatenlogik) In dieser Struktur "gilt" F offensichtlich (was wir gleich formal definieren
Eine Struktur ist ein Paar d = (U;, Ia) wobei UA eine beliebige aber nicht werden}, denn jede natürliche Zahl ist kleiner als ihr Nachfolger und die Sum-
leere Menge ist, die die Grundmenge von A (oder der Grundbe~ich,der In- me von 2 und 3 ist eine Primzahl.
dividuenhereicfi,das Univerxum) genannt wird. Ferner ist Ia eine Abbi I dung, Man kann sich natürlich auch für diese Beispielfomel F (zu F passende)
die Strukturen vorstellen, in denen F nicht gilt. F ist also nicht in jeder Struktur
gültig.
- jedem k-stelligen Prädikatsymbol P (das irn Definitionsbereich von TA
Um nicht den Eindruck aufkommen zu lassen, dass der Gmndbereich UAim-
liegt) ein k-stelliges Prädikat über UA zuordnet,
mer aus Zahlen bestehen muss, geben wir nun eine Struktur an, die auf den
- jedem k-stelligen Funktionssymbol f (das im Definitionsbereich von IA ersten Blick etwas künstlich wirken mag, aber im Kapitel 2.4 eine wichtige
Iiegt) eine k-steIlige Funktion auf Ud zuordnet, Rolle spielen wird. Sei A = (U*,I*), wobei UA die Menge der variablenfrei-
en Terme ist, die aus den Bestandteilen von F (also den Funktionssymbolen)
- jeder Variablen X (sofern I* auf X definiert ist) ein Element der Grundmen- aufgebaut werden können. Fiir obige Beispielfomel wäre
ge UA zuordnet.
Mit anderen Worten, der Definitionsbereich von IA ist eine Teilmenge von
k , X , 1 i = 1 , 2 , 3 , .. . u n d k = 0 , 1 , 2 , . . .),undder Wertebereich von
>E , fi
.,
{Pt Für jeden Term t E UA sei f A(t) definiert als der Term f ( t ) E Ua, und für
IA ist eine Teilmenge aller Prädikate und Funktionen auf UA,sowie der Ele- alle Terme t l lt 2sei gA(tl t S }definiert ais der Term g ( t l , ts) E VA.Ferner sei
mente von U*.Wir schreiben a b k h e n d statt Ia(P) einfach P", statt JA(f) U* =
*
einfach f und statt IA(x) einfach zA. Der Leser sollte sich unbedingt klarmachen, was für eine Wechselwirkung
Sei F eine Formel und A = (UAlI*) eine Struktur. A heißt zu F passend, zwischen syntaktischen Objekten (den Elementen von U*) und den semanti-
falls IA für alle in F vorkommenden Prädikatsyrnbole, FunktionssymboIe und schen Interpretationen (f A l gA und a*) hier stattfindet. Um A vollständig zu
freien Variablen definiert ist. definieren, muss noch pA,QA und zA angegeben werden. Wir überlassen es
dem Leser, diese Definition einmal so vorzunehmen, dass sZ Modell für F ist,
Beispiel: F = tlzP(xl f (X)) A Q(g(a, 2 ) ) ist eine Formel. Hierbei ist P ein und so, dass A kein Modell fiir F ist.
zweistelliges und Q ein einstelliges Pridikatsymbol und f ein einstelliges,
g ein zweistelliges und a ein nuIIsteIIiges Funktionssymbol. Die Variable z Definition (Semantik der Prädikatenlogik - Fortsetzung)
kommt in F frei vor. Eine zu F passende Struktur ist 2.B. A = (UA,IA) mit Sei F eine Formel und A eine zu F passende Struktur. Fiir jeden Term t, den
man aus den Bestandteilen von F bilden kann (also aus den Variablen und
Ud = {0,1,2, ...} = INl Funktionssy mbolen), definieren wir nun den Wert von t in der Stmktur A,
I A ( P ) = pA = { ( m ,n) ) m, n E IjA u n d m < n), den wir mit A(t)bezeichnen. Die Definition ist wieder induktiv.
1. Falls t eine Variable ist (also t = X), s o ist Alt} = sA. Kierbei bedeutet AIxJ4diejenige Struktur At,die überall mit A identisch ist,
bis auf die Definition von X*' : Es sei nämlich X*' = d, wobei d E UA = UAi
2. Falls t die Form hat t = f (tl, . . . ,t k )wobei t,, . . . ,tk Tenne und f ein - unabhängig davon, ob Id auf z definie~t isr oder nrcht.
k-stelliges Funkhonssymbol ist, so ist
4 t ) = fA(A(t,) , - . ,dltk)).
FaIIs für eine Formel F und eine zu F passende Struktur A gilt d(F) = 1,
Der Fall 2 schließt auch die Möglichkeit ein, dass f nullstellig ist, also i: die so schreikn wir wieder A F (Sprechweise: F gilt in A oder A ist Modell
Form hat t = a. In diesem Fall ist also A(t)= aA. fW F ) . FaIls jede zu F passende Struktur ein Modell für F ist, so schreiben
Auf analoge Weise definieren wir (induktiv) den (Wahrheits-) Wert der For- wir F (Sprechweise: F ist (allgemein-)gullig), andernfalls F. Falls es
meln F unter der Struktur A, wobei wir ebenfalls die Bezeichnung d(F) mindestens ein Modell für die Formel F gibt, so heih F efiilbar, andernfülls
verwenden. uae@EEbar.
1. Falls F die Form hat F = P(t,, .. . ,t k )mit den Termen t l ,. . . , tk und Übung 44: Gegeben sei folgende Formel:
k-stelligem Prädikatsymbol P, so ist
1, falls A(G) = 0 Einige Begnffe aus der Aussagenlogik wie "Folgerung" und "Äquivalenz"
A(F) = können nun in offensichtlicherWeise direkt in die PrädikatenIogik übertragen
0, sonst
werden. Wir verwenden diese Begriffe irn Folgenden, ohne sie noch einmal
3. Falls F die Form F = (G A H) hat, so ist explizit zu definieren.
eine Formel ohne Variablen (aber mit mehr als 0-steiligen Prädikazensym- Übung 46: In der Prüdihtenlogik mit Identifät ist auch dris Symbol = zuge-
bolen!). Indem wir die vorkommenden atomaren Formeln mit entsprechenden lassen, das Gleichheit zwischen Termen bedeuten soll. Wie muss die Syntm
atomaren Formeln der Aussagenlogik identifizieren (Definition von Formeln) und Semantik (Definition von A ( F ) )der Pradika-
tenlogik erweitert werden, um die Prädikatenlogik mit Identität zu erhalten?
Übung 47: Welche der folgenden Strukturen sind Modelle für die Formel
Offensichtlich ist (ein solcherart gewonnenes) F' erfüllbar (oder gültig) genau
dann, wenn F erfüIlbar (oder gültig) ist.
(C) UA = pIN(die Potenzmenge von IN),
3. Man beachte, dass prädikatenlogische Formeln, sofern sie keine Quanto- P A = ((Al B ) 1 A, B C IN,A C B }
sen enthalten (z.B. die Matrix einer gegebenen Formel), mit den Mineln der
Aussagenlogik in KNF bzw. DNF umgeformt werden können. Der einzige
Unterschied ist, dass die Rolle der aussagenlogischen atomaren Formeln (dies Übung 48: Sei F eine Formel und die in F frei vorkommenden Variablen
sind die A, j nun von den prädikatenlogischen atomaren Formeln übernommen seien 21, x2,. . . ,x,~.Man zeige:
wird (dies sind die Formeln der Form P(tl,. . . , t,)).
(a) F ist gültig genau dann, wenn QzlVxz. - . h , F giiltig ist,
4. Die Prädikatenlogik ist zwar "ausdnicksscärkeJ' als die Aussagenlogik, je-
doch kann nicht jede mathematische Aussage im Rahmen der Prädikatenlogik (b) F ist erfüllbar genau dann, wenn 32, 3x2 . 3x,F erfiillbar ist.
+ +
Um prädikatenlogische Formeln in gewisse Normalformen umzuformen, Übung 56: Man zeige, dass F = ( 3 x P ( 2 )t P(y)) äquivalent ist zu G =
benötigen wir jedoch auch Äquivalenzen, die Quantoren mit einbeziehen. Y x ( P ( x )+ P ( y ) ) .
Satz Übung 57: Man beweise, dass Vx3y P ( x ,y) eine Folgerung von 3yVx P ( z ,
Seien F und G beliebige Formeln. ist, aber nicht umgekehrt.
Ferner bemerken wir, dass das Erselzbarkitstheorem der Aussagenlogik in Definition
analoger Weise auch fUr Formeln der Pradikatenlogik gilt. Der im Kapitel Sei F eine Formel, X eine Variable und t ein Term. Dann bezeichnet F[x/t]
1.2 geführte Induktionsbeweis (iiber den Formelaufbau) muss Iediglich um diejenige Formel, die man aus F erhält, indem jedes freie Vorkommen der
die bei prädikatenlogischen Formeln zusätzlich vorkommenden Fälle ergiinzt Variablen X in F durch den Tenn t ersetzt wird. Durch [ x / t ]wird eine Substi-
werden. (Fd14: F hat die Form F = 3xG, Fall 5: F hat die Form F = VxG). tution beschrieben.
Dies führt gleich iiber zu der nächsten Bemerkung. Induktionsbeweise über Substitutionen (oder auch Folgen von Substitutionen} behandeln wir auch als
den Formelaufbau können - wie soeben bemerkt - auch bei prädikatenlo- selbständige Objekte. So soll z.B.
gischen Formeln geführt werden (mit entsprechend mehr Fallunterscheidun-
gen). Da jedoch der Definition von Formeln die Definition von Termen vor-
ausgeht, muss bei dem Beweis einer Behauptung B, die für alle prädikaten-
logischen Formel gelten soll, evtl. ein weiterer Induktionsbeweis über den diejenige Substitution bedeuten, die in einer Formel (oder auch in einem
Termaufbau vorausgehen. Hierzu muss die Behauptung B evtl. auf Terme an- Term) jedes freie Vorkommen von X durch f l und dann jedes freie Vorkom-
gepasst bzw. umgeformt werden. men von y durch tz ersetzt. (Man beachte hierbei, dass tl auch y enthalten
darf).
Man beachte, dass die Äquivalenzurnfomungen 1-3 des obigen Satzes - von
links nach rechts angewandt - die in einer Forme1 evtl. vorkommenden Quan-
toren '"nachaußen treiben". Bemerkung: Man unterscheide deutlich zwischen Ap14 und F[x/t]. Zum
einen erhaiten wir eine neue Struktur, bei der X den Wert d erhalt (Semantik)
und zum anderen erhalten wir eine neue Formel, bei der z durch t ersetzt ist
Beispiel: (Syntax).
( 7 ( 3 x P ( 2 Y)
, V Qz&lz)) A 3 w P ( f( U , W ) ) ) In der fotgenden Übung soll der Zusammenhang zwischen beiden Notationen
z ((-3xP(s, y} A +'.@(z}) A 3uiP(f( a ,W))) (deMorgan) hergestellt werden.
( ( Q x 7 P ( sy1) A 327Q(z))r\ 3wP(f (a, W ) ) (wegen 1.)
Übung 58: Man beweise (per Induktion über den Term- und Formetaufbau),
-
(3wP(f (a, W))A (VX-.IP(X, Y) h 3 z ~ Q t z ) ) )(Komrnutativität)
dass das folgende ~ b e ~ h m n g s l e m mfüra jede Forme1 F, jede Variable X,
= 3w(P(f (U, W))A V x ( l P ( s ,P) A 3 z l Q ( z ) ) )(wegen 2.) und jeden Term .t, der keine in F gebundene Variable enthält, gilt:
3w(Vx(3zlQ(z)r\ l P ( s ,3)) J\ P( f ( U , W ) ) ) (Kommutativität)
= 3 u i ( V x 3 x ( l Q ( z ) A + ( X , y)) /\ P(f ( a ,W ) ) ) (wegen 2.)
3wb'z32-(lQ(z) ri -iP(r:Y) i\ P( f (a, W ) ) ) (wegen 2.)
Definition äquivalent.
Eine Formel heißt pränex oder in Pränexfom, faIIs sie die Bauart hat
1. F hat die Form -F1 und GI = G)l ylQzyz . - - QnynG' sei die nach Definition (Skolemform)
Induktionsvoraussetzung existierende zu Fl äquivalente Formel. Dann Für jede Fomel F in BPF definieren wir i hre Skolernfom(-el) als das Resultat
gilt - der Anwendung folgenden Algorithmus' auf F :
F 5Q I Y I Q ~ Y ~ ~ . + Q & ~ Y ~ ~ G '
wobei = 3, falls Q, = V; und = V, falls Q, = 3. Diese Formel while F enthält einen Existenzqnantor do
hat die gewünschte Form. begin
2.2. NORMALFORMEN 65
F habe die Form F = Vy,Vyz + .+Vyn32Gf i r eine Formel G Wir nehmen zunächst an, dass F' erfüllbar ist. Dann gibt es eine Struktur d,
in BPF und TL 2 0 (der Allquantorblock kann auch leer sein); passend zu F', mit d ( F E )= 1.Dann passt A auch zu F und es gilt:
Sei f ein neues bisher in F nicht vorkommendes n-stelliges füralle U I , U ~ .~. ,U,
. E UA ist
FunktionssymboI;
F := V Y I V M ~- ..v ~ ~ n c (91
[ ~ /~ f2 .3. . ~ n ) ] ;
1
'A[Yl/?L1~[Y2/U2~-[Bm!Un] (G[z/f(yi ~ 2 ~' + . Y ~ 3 =I I .
(d-h. der Existenzquantor in F wird gestrichen und jedes Vor- Mit dem Uberf~hmngclemmafolgt:
end
-
kommen der Variablen x in G durch f (?lili,y2: . . . yn) ersetzt)
füralle U ~ , T I ,. ~. ., , U , E Ud ist
A[~l/~l][212/~2]~~~[YR/ZIn][Z/~] (G) = '
Beispiel: Betrachten wir die Forme1
für alle u l , u2,. . . , U, E UA gibt es ein v E U* mit
A[~l~llaia/~al~~~[~~~/~~lt~/~~
(G) = +
und damit 2. Seien y1, y2, . . . , pn die in F bzw. Fl vorkommenden freien Varia-
-a'(Vm - . - VynG[zJf ( u ~. ,. .,yn)]) = 1 blen. Ersetze F, durch F2 = 3y 13y2. . - 3y, Ft . Dann ist F2 erfullbar-
Also ist A' Modell für F'. keitsaquivalent zu Fl und F (vgl. Übung 48) und enthält keine freien
Variablen mehr.
an!
Umbenennen von y zu W im zweiten Disjunktionsglied liefert die bereinigte
Übung 64: Wenn man im Algorithmus zur Erzeugung der Skolernform die Form
Rollen von 3 und V vertauscht, so entsteht ein Algorithmus, der aus gegebe-
ner Formel F in BPF eine Formel F' erzeugt, die keine Allquantoren mehr
enthält. Man zeige: F ist genau dann giiltig, wenn F' gültig ist.
Die Variable x kommt in F1 frei vor. Wir bilden deshalb
Übung 65: Man gebe ein algorithmisches Verfahren an, das zu gegebener, be-
reinigter Formel F direkt (also ohne vorheriges Erstellen einer Prinexfcimel)
eine Skolemformel von F erzeugt. Hierzu überlege man sich, dass die Exi- Umformen in Pränexform liefert (z.B.)
stenzquantoren der Rinexformel genau von denjenigen Existenz- (bzw. All-
}quantoren der Ausgangsformel herstammen, die sich im "Wirkungsbereich"
einer geraden (bzw. ungeraden) Anzahl von Negatjonszeichen befinden.
Wir gehen nun zur Skolemform über, wobei ein neues 0-stelliges Funktions-
symbol a (eine Konstante) für z und h(x) für y substituiert wird.
Es soIlen noch einmal alle behandelten Umfomungsschritte zusammenge-
stellt werden, die eine Formel durchlaufen muss , um für die Anwendung der
später zu betrachtenden Algorithmen in adaquater Form vorzuliegen.
Umformen der Matrix von in KNF liefert
Gegeben: eine prädikatenlogi sche Formel F (mit eventuellen Vorkommen
von freien Variablen).
Um es noch einmal zu verdeutlichen, wir zeigen also irn Folgenden, dass u.a. den Resultaten der Berechenbarkeitstheorie. Aus einem fiktiven Entschei-
dieses Problem unentscheidbar ist: dungsverfahren fur das Gültigkeitsproblern der Prädikatenlogik müssen wir
ein fiktives Entscheidungsverfahren für das Postsche Korrespondenzproblem
gegeben: Eine prädikatenlogi sche Formel F. konstruieren. Viele Unentscheidbarkeitsresultatcin der Theorie der Formalen
gefragt: Ist F eine giiltige Formel? Sprachen werden mittels dieser Methode der Reduktion geführt - insbesonde-
re auch unter Verwendung der Unentscheidbarkeit des Postschen Korrespon-
Hierzu verwenden wir ein bekanntes Resultat aus der Berechenbarkeitstheo- denzproblems.
rie, das wir hier nicht beweisen wollen, nämIich dass das sog. Postsche Kor-
respondenzproblem unentscheidbar ist. Dies ist das folgende Problem:
Satz (Church)
gegeben: Eine endliche Folge von Wortpaaren (zl, yl):. . . , ( x k :yk), Das GuItigkeitsprobEem der Prädikatenlogik ist uncntscheidbar.
wobei X„ y, f { O l l ) + .
Beweis: Wie oben bereits ausgeführt, besteht die Aufgabe darin, eine dgo-
gefragt:Gibt es eine Folge von Indizes il ,iL, . . . , in f {1,2,. . . , k}, rithmische Vorschrift anzugeben, die jedes beliebige vorgelegte Postsche Kor-
n > l,mitxilx, ? . . . X,,, =?~„y„ ...Y,-? respondenzproblem K in endlicher Zeit in eine prädikatenlogische Formel
Wir nennen ir, iz3 . . . , in dann eine Lösung des Komspondenzproblems
F = FK überführt, so dass K eine Lösung besitzt, genau dann wenn FK
gültig ist. Daraus ergibt sich dann, dass die fiktive Existenz eines Entschei-
~ l )( ,~ 2 3~ 2 ) ;- .. I ( X ~ ~I k ) .
dungsverfahrens ffir die Prädikatenlogik che Existenz eines Entscheidungs-
verfahrens für das Postsche Korrespondenzproblem nach sich zieht. Sei also
Beispiel: Das Korrespondenzproblem
Ua = {0,1}* (dieMenge aller endlichen Wörter, die Mit anderen Werten,für u = p(xilx*, .. . yin) gilt ( ? J , 21) E
. . .xi,) = p(yZlziyap
sich mit dem Alphabet {O,l) bilden lassen), P*. D m u s folgt A +
3rP(z,z ) , und somit A F3. Damit ist A F
U* = E (das leere Wort), gezeigt.
ft(a) = CVO (die Konkatenatron von a mit 01,
Folgerung: Das Erfüllbarkeitsproblem der Prädikatenlogik (gegeben: eine
ft(a) = al (die Konkatenation von a mit l),
Formel F, gefragr: Ist F erfullbar?) ist unentscheidbar.
= {(cT, P) 1 0,ß 6 {0,1}+ und es gibt Indi-
. und ß =
zes i l , i 2 , . . .,it mit a = z „ ~ „. .X„ Beweis: Da eine Formel F giiltig ist genau dann, wenn i F unerfüllbar ist,
Yaizlia . . . ~ i t I . würde die Existenz eines fiktiven Entscheidungsverfahrens fiir das Erfüllbar-
keitsproblem zur Existenz eines Entscheidungsverfahrens für das Gültigkeits-
Ein Wortpaar (a,b') liegt also in PA,falls (II mittels derselben indexfolge problem führen. Da das Gültigkeitsproblem unentscheidbar ist, kann es ein
il , iz, . . . , it aus den X, aufgebaut ist, wie ß aus den pT aufgebaut ist. solches Verfahren also nicht geben. m
Man stellt nun Ieicht fest, dass A zu F passend ist. Somit gilt A F. Ferner
kann man nachprüfen, dass A + F, und A + F2 gelten. Da F die Bauafi Der Leser wird sofort bemerkt haben, dass dieses Argument wiederum nichts
einer Implikation ((Fi A F2)+ F3) hat, folgt A F3. anderes als die Methode der Reduktion ist.
Inhaltlich bedeutet A F3 aber nichts anderes, als dass ein Wort y E 10, I ) +
existiert, das mittels derselben Indexfolge aus den xi, wie auch aus den y„ Übung 67: Man zeige, dass das Gültigkeitsproblem (und damit auch das
aufgebaut werden kann. Mit anderen Worten, das Korrespondenzproblem K Erfüllbarkeitsprobfem) bereits für Formeln ohne Funktionssymbole unent-
besitzt eine Lösung. scheidbar ist.
Sei nun umgekehrt angenommen, dass K die Lösung il, 22, . . . ,in besitzt.
Es gilt also X„ X „ . . . X,= = y„ ?lf, .. . yT,. Ferner sei A eine beliebige zu F Übung68: Man zeige, dass folgende Variante des Postschen Korrespondenz-
passende Struktur. Wir müssen nun zeigen, dass A F gilt. FaIls A F, problems entscheidbar ist.
oder A Fz, so folgt wegen der Bauart von F sofort, dass A F. Nehmen
+
wir für das Folgende also an, dass A F, und A F„ also A (4 + P, fi), gegeben: Eine endliche Folge von Wortpaaren ( X , , yl), . . . , (xk,yk),
wobei X,,y, E {0, I}+.
gilt.
Wir definieren nun eine Abbildung (oder Einbettung) p : (0, I}* -+ I j A durch gefragr: Gibt es Folgen von Indizes il , iZ, . . . in, n 2 1, und
folgende induktive Definition: j 1 , j 2 ~ - . . ,13,~",
tm~ „>x „ . . . x t ~ = ~ ~ ~ ~ ~ ~7 . . . y j ~ .
2.4 Herbrand-Theorie
Beispiel: Gegeben seien die Formeln F und G:
Ein Problem beim Umgang mit prädi katenlogischeri Formeln ist, dass die De- F = VxVyQxP(x,f {Y), dz,T))
finition von Simkturen A = (UA,IA)zulässt, dass UA beliebige Mengen G = VxVyQ(c, f (X),h(91b ) )
sein können. Insbesondere scheint es zunächst keine Möglichkeit zu geben,
Aussagen uber deren Mächtigkeit, geschweige denn über den Aufbau von IA Für die Formel F liegt der Spezialfall vor (kein Vorkommen einer Konstan-
zu machen. Es scheint ein unmögliches Unterfangen zu sein, auf irgendeine ten). Deshalb ist
systematische Art und Weise alle potenziellen Strukturen für eine gegebene
2.4. HERBRAND-THEORIE 79
Iadukfionsanfmg (n = 0). Falls G keine Allquantoren (also überhaupt keine Beispiel: Für die oben behandelte Beispielformel
Quantoren) enthält, so ist aus der Definition von B unmittelbar klar, ddss sogar
gilt: A(G) = B(G).
Indukh'onsschritt (n > 0).Sei G eine Formel m i t n Allquantoren der Bau-
art G = V x H , wobei H nur n - 1 Allquantoren enthält. Auf H selbst ist sind die einfachsten Formeln in E ( F ) die folgenden:
die Jnduktionsvoraussetzung zunächst nicht anwendbar, da H keine Aussage
mehr ist (X kann in H frei vorkommen). Da nach Voraussetzung A G, gilt
fur alle U E UA, dass A[,J,I(H) = 1. Dann gilt erst recht für alle u E &
der speziellen Form U = A(t) mit t E D(G), dass dlTl,Ll
( H ) = 1. Anders
(H) = A ( H [ x / ~=] 1
ausgedrückt, für alle t E D(G) gilt Ai,lActjl ) (wegen
Uberfühmngslemma). Nach Induktionsvoraussetzung ist nun B ( H [ x / t ] =
) 1
für alle t E D(G). Wieder mit dem Uberfiührungslemma folgt, dass für alle
= B(H[x/t])= I.Also ist B(VxH) = B(G)= I,
t E D(G) gilt .tilrzlL7(tjl(H)
was zu zeigen war.
Man beachte, dass die Formeln in E ( F ) letztlich wie aussagenlogische Eor-
Der Leser möge nachvollziehen, dass für &esen Beweis wesentlich ist, dass meln behandelt werden können, da sie keine Variablen enthalten. Anstelle von
die Formel F eine Aussage ist, und dass keine Existenzquantoren in F vor- Al, A2,A?,. . . wird sozusagen ein anderes Bezeichnungssystern für die ato-
maren Formeln verwendet. Bei der Angabe einer Struktur für die Formeln in
kommen.
E ( F ) genügt es, die Wahrheitswerte der atomaren Formeln in E ( F ) anzu-
geben. Die Angabe eines Gnindbereichs und der Interpretation der Terme ist
Folgerung (Satz von Cöwenheim-Skolem) überflüssig.
Jede erfüllbare Formel der Prädikatenlogik besitzt bereits ein abzahl bares Mo-
dell (also eines mit abzählbarer Gmndmenge}.
Satz (Gödel-Herbrand-Skolem)
Beweis: Mit den Methoden aus Abschnitt 2.2 kann jede prähkatenlogische Für jede Aussage F in Skolemfom gilt: F ist erfüllbar genau dann, wenn die
Formel F in eine erfüllbarkeits~quivalente Aussage G in Skolemform Forrnelmenge E ( F ) (im aussagenlogischen Sinn) erfüllbar ist.
überführt werden. Diese Umformungen sind solcherart, dass jedes Modell
für G auch Modell für F ist. Da F erfü3Ibar ist, ist G erfüllbar und G besitzt Beweis:Es genügt zu zeigen, dass F ein Herbrand-Modell besitzt genau dann,
dann ein Herbrand-Modell (welches auch Modell für F ist). Dieses Herbrand- wenn E ( F ) erfüllbar ist.
Modell besitzt die Grundmenge D ( G ) ,welche abzählbar ist. Die Formel F habe die Form F = VylVy2. . . VyaF*. Nun gilt:
A(F"(YI / t l ][ ~ 2 / t z 1 .- - [ ~ n / t n ]=
) 1 (Uberf~hnrn~slernma) Gib "unerfüllbar" aus und stoppe;
gdw. für alle G E E ( F ) gilt A(G) = I
gdw. A ist ein Modell für E (F). Dieser Algorithmus hat die Eigenschaft, dass er auf unerfüllbaren Formeln
W
nach endlicher Zeit stoppt mjt der Ausgabe "unerfüllbar"; auf crfüllbaren For-
meln dagegen nicht stoppt.
Diese Situation entspricht der sog. Semi-Eatscheidhurkeit; auf den ja-
Der Satz von Gödel-Herbrand-SkoIem kann dahingehend interpretiert wer-
Instanzen des zugmndeliegenden Problems (hier: "Ist F unerfullb~?")stoppt
den, dass es möglich ist, prädikatenlogische Formeln durch i.a. unendlich vie-
das Verfahren, nicht jedoch auf den nein-Instanzen.
le aussagenlogische Formeln (dje Formeln in E ( F ) )zu approximieren. Indem
wir diesen Satz von Gödel-Herbrand-Skolemnoch mit dem Endlichkeitssatz Durch Eingabe von -F anstatt F in den Algorithmus wird aus dem Unerfüll-
der Aussagenlogik kombinieren, erhalten wir den barkeitstest ein Gultigkeirstest. Somit können wir zusammenfassen:
Wir sind nun in der Lage, ein Serni-E~t.scheidungme$ah~n für (die Unerfüll- a u n g 73: Milan zeige, dass der hier eingeführte Begriff der Semi-
barkeit von) Formeln der Priidikatenlogik zu formulieren. Hierbei verstehen Entscheidbarkeit identisch ist mit dem Begriff der rekursiven Aufzählbar-
wir unter einem Semi-Entscheidungsverfahrenfür ein Entscheidungsproblern keit. Hierbei heißt eine Menge M rekursiv aufzählbar, falls M = fl
einen Algorithmus, der genau auf denjenigen Eingaben nach endlicher Zeit oder falls es eine algorithmisch berechenbare Funktion f gibt mit M =
stoppt, für die die zugnindeliegende Fragestellung mit 'tja" zu beantworten {f (1),f (21, f (31,. . .}. Die Menge M wäre irn obigen Beispiel die Menge
ist. Die Korrektheit des Verfahrens ergibt sich unrnitteIbar aus dem Satz von aller unerfüllbaren pradi katenlogischen Formeln.
Herbrand. Im folgenden fixieren wir eine beliebige Aufiahlung von E ( F ) =
{F,: Fa F3.. . .J. Übung 74: Man zeige: Ein ProbIern ist entscheidbat genau dann, wenn es re-
kursiv aufiahlbrtr 1st (vgl. vorherige übung), wobei für die aufzählende Funk-
Algorithmus von Gilrnore <
tion f gilt: f (n) f (n-+ 1) für alle TL.
Eingabe: Eine prächkatenlogische Aussage: F in SkoIemform Übung 75: Man zeige, dass das Postsche Korrespondenzproblem (vgl. Ab-
(Jede prädikatenlogische Formel kann in eine erfüllbür- schnitt 2.3) semi-entscheidbx ist.
keitsäquivalente Formel dieser Art überführt werden, vgl.
Abschnitt 2.2).
Durch Kombination des Unerfüllbarkeitstests und des Gültigkeitstestskönnen
wir einen Algoithmus erhalten, der zumindest auf den unerfüllbaren und den
2.5. RESOLUTION 85
gültigen Formeln stoppt (mit der Ausgabe "unerfüllbar" bzw. "gültig"). Man entstehen, liegen dann auch alle Fomeln aus E ( F ) in KNF vor. Damit bie-
könnte noch ein dnttes Verfahren hinzunehmen, das Formeln auf ihre Erfüll- tet sich die nachfolgende Modifikrttion des Gilmore-Algorithmus' an, deren
barkeit in endlichen Modellen testet, indem es systematisch die Modelle der Korrektheit sich unmittelbar aus der Korrektheit des Gilmore- Algorithmus'
Mächtigkeit n = 1 , 2 , 3 ,. . . durchprobiert. ergibt.
Zusammengefasst ergibt dies ein Verfahren, das genau auf den Forrnein in den Wir nennen diesen Algorithmus Grundre.soiurionsalgorithmus. Diese Be-
schraffierten Zonen nach endlicher Zeit stoppt - mit entsprechender Ausgabe. zeichnung ergibt sich aus dem Verständnis, dass Substitutionen, die alle frei-
en Variablen durch variablenfreie Terme ersetzen, Grcmdsubstitufionen sind.
alle prädikatenlagischen Formeln Die Substitutionen, die in der Definition von E ( F ) vorkommen, sind also
Gnindsubszitutionen. Sofern alle Variablen in F" durch eine Grundsubstitu-
tion ersetzt sind, so ist das Resultat eine sogenannte Grundinsranz von F*.
Falls eine Formel G aus einer Formel F durch Substitution der Variablen in
F durch (nicht notwendigeweise variablenfreie} Terme entsteht, so heißt G
eine Instanz von F.
Im folgenden sei Fl, F2!F3,. . . wieder eine Aufzählung aller Formeln in
Gnindresolutionsalgorithmus
I
gültige
I
erfüllbare, aber nicht
gültige Formeln unerfüllbare
Eingabe: eine Aussage F in Skolemform mit der Matnx F* in
KNF
Formeln mit endlichen Modellen Formeln i := 0;
:= 0;
repeat
Die weiße Fliiche in diesem Diagramm könnte zwar noch etwas weiter ver- i := i + 1; M := M U {Fi); M := Res*(M)
kleinert weden (2.B. für Formeln in Pränexform ohne Funktionssymbole, wo- until E M;
bei nur bestimmte Anordnungen der Quantoren zugelassen sind), kann jedoch
nie vollständig elirninieri werden. Dies würde in Widerspnich zum Unent- Gib "unerfüllbar" aus und stoppe.
scheidbarkeitsergebnis von Kapitel 2.3 stehen.
Aus dem Satz von Herbrand und dem aussagenlogischen Resolutionssatz er-
gibt sich zusammenfassend dann der foIgende Satz.
2.5 Resolution
Satz
Die Tests auf Unerfüllbarkeit der jeweiligen endlichen Teilmengen von E (F), Bei Eingabe einer Aussage F in Skolemfom mit Matrix F*in KNF stoppt
die i m Gilrnore-Algorithmus durchgeführt werden müssen, können im Prin- der Gmndresolutionsalgonthmus nach endlich vielen Schritten mit der Aus-
zip auch per (aussagenlogischer) Resolution erledigr werden. Voraussetzung gabe "unerfüllbar" genau dann, wenn F unerfüllbar ist.
hierzu ist, dass die Matnx der Ausgangsfonnel in KNF vorliegt. (Dies kann
immer erreicht werden, vgl. Kapitel 1.2 und 2.2.) Da alle Fomeln in E (F) Wie auch beim aussagenlogischen Resolutionsalgorithms werden während
mittels Substitution der Variablen in F*durch variablenfreie Terme aus D ( F ) des Ablaufs des Gnindresolutionsalgorithmus' evtl. wesentlich mehr Elemen-
te in M erzeugt, als für die "Demonstration" der Unerfüllbarkeit von F wirk- Klauseln in F* (P(z)] {lPCf (X)))
lich von Belang sind (abgesehen von der Tatsache, dass bei einer erfüllbaren
Formel F der Algorithmus nicht stoppt und dann i.a. unendlich vieIe Ele- Grundsubstitutionen
mente in iV erzeugt). Von Belang sind nur diejenigen Grundinstanzen von
Klauseln in F*,die für die Resoiutionsherleitung der leeren Klausel auch gewisse Grundrnstanzen j t
benötigt werden. Wir kännen uns somit bei d e ~Darstellung eines "Bewei- der Klauseln in F* {PCf(4)) {lP(f (a))l
ses" für die Unerfiillbarkeit einer prädikatenlogischen Formel F darauf be-
schränken, zunächst geeignete Gmndinstanzen der Klauseln in F* anzuge-
Resolution der
ben, und diese dann in einem Resolutionsgraphen, der auf die leere Klausel leeren Klausel U
fuhrt, zu verknüpfen.
Beispiel: Gegeben sei folgende unerfuIlbare Formel: Betrachten wir nun ein komplizierteres Beispiel. Sei
Hierbei ist F* = ( P ( x )A l P ( f(X))), und in Klauselform geschrieben, Dann erhalten wir die Klauseldarstellung
F* = { { P ( x ) ) ,{ i P (f (X)))}. Ferner ist D ( F ) = (U, f (a), f (f(a}},. . .)
und E(FJ= {(Pb) l P ( f ( a ? ) ) ,( P ( f(0))A 1Plf (f ( a ) ) ) ) ., . .I.
Bereits die ersten beiden Substitutionen [s/a] und (X/f (n)] liefern eine un-
erfüllbare Klauselmenge, diese entspricht den ersten beiden Elementen von Die Formel F ist unerfüllbar. Ein Beweis für die Unerfüllbarkeit von F ist
E (F),und enthält damit vier Klauseln. 2.B. gegeben durch folgendes Diagramm.
Bei diesem Beispiel werden jedoch schon zwei Klauseln generiert, die für
die Herleitung der leeren KIausel nicht benötigt werden. Es genügt somit, für
jede Wausel in F*individudl geeignete Substitutionen zu finden, die dann
auf diese Klausel, nicht jedoch auf die gmze Klauselmenge F* angewandt
werden. Schematisch können wir dies im obigen Beispiel folgendermaßen
darstellen.
Zum anderen kann aus einer n-elernentigen prädikatenlogischen Klausel nach Wir führen nun eine prädikatenlogische Form der Resolution ein, die auf
der Gnindsubstitution eine m-elementige (m 5 n) Klausel aus E (F) ent- J.A. Robinson zurückgeht. Die Gnindjdee hierbei ist, dass prüdihtenlogische
stehen. Hierbei ist m < n, falls durch die Grundsubstituti~ngewisse Li- Resolvenren aus prädikatenlogischen Klauseln erzeugt werden können, wo-
teraie der Ausgangsklausel identisch werden, und daher, wegen der Men- bei jeder Resolutionsschritt mit einer geeigneten Substitution einhergeht,
gendarstellung, zu einem Element verschmelzen. (Dies ist bei der Klausel die gewisse Literale in den beiden Ausgangsklauseln zueinander komple-
{ , P ( x ) , - P ( f (U)), Q(y)) und der Substitution [X/f ( n ) ] der Fall). mentär (d.h. bis auf die Negationszeichen identisch) macht. Diese Substr-
Wir fassen unsere Beobachtungen nochmals zusammen. tutionen müssen in einer möglichst "zurückhaltenden" Art und Weise aus-
geführt werden. Es genügt 2.B. bei den beiden Klauseln (P(rc),-Q(g(z) ))
und { l P (f (y))}, die Substitution [X/f (?{)I durchzufuhren, um den (pradika-
Grundresolutionssatz
tenlogischen) Resolventen {lQ(g( f (3))) zu erhalten. Es besteht keine Not-
Eine Aussage in Skolemform F = QyiVyz . . .VykF" mit der Matrix F*
in KNF ist unerfüllbar genau dann, wenn es eine FoIge von Klauseln
?,
wendigkeit, an dieser Stelle bereits eine Substitution für die Variable vorzu-
sehen.
K1,Kz, . . . , K, gibt mit der Eigenschaft: Zentral für die folgenden Betrachtungen ist das Finden von Substitutionen,
die eine Menge von Literalen (evtl. mehr als zwei Literale) unifiziert, d.h.
K, ist die leere Klausel und für i = 1:. . . , n gilt: identisch macht. Irn obigen Beispiel unifiziert [X/f (Y)] die beiden Literale
entweder ist K, eine Grundinstanz einer Klausel K E P ( x ) und P(f (y)). Ebenso würde die Substitution [X/f ( n , ) ] [ y / a diese
] bei-
F*,d.h. K, hat die Form K, = K[yl/tl] [yk/ t k ] den Literale unifizieren, jedoch mit dem Unterschied, dass hier sozusagen
+
mit t l ,t 2 , .. . , t k f D ( F ) , mehr substituiert wird als notwendig. Diese Substitution erfüllt dann nicht
oder K, ist (aussagenlogischer) Resolvent zweier dre Definition eines allgemeinsten Uaifzkators.
Klauseln K, und Kb mit a,b < i.
Definition (Unifikator, allgemeinster Unifikator)
Eine Substitution sub (also eine Ersetzung von evtl. mehreren Variablen
Übung 76: Man formalisiere die Aussagen (a) und (b) als prädikatenlogischc durch Terme) ist ein UaiJikatoreiner (endlichen) Menge von Literalen L =
Formeln. { L 1 L, 2 , .. . , L k ) , faI1s Llsub = Lzsekb = . . . = L k ~ u bD.h.,
. durch An-
wenden der Substitution sub auf jedes Literal in L entsteht ein und dasselbe
(a) Der Professor ist glücklich, wenn alle seine Studenten Logik Literal.
mögen. Wir schreiben für diesen Sachverhalt auch JLsubl = 1, und sagen L ist an#-
(b) Der Professor ist glücklich, wenn er keine Studenten hat. zierbar. Ein Unifikator sub einer Literalmenge L heißt allgemeinster Unijika-
tor von L, falls für jeden Unifikator sub' von L gilt, dass es eine Substitution
Man zeige durch Grundresolution, dass (b) eine Folgerung aus (a) ist. s gibt mit si~b'=subs.
(Hierbei bedeutet die Gleichung sub' = subs, dass für jede Formel F Fsub' =
Die algorithmische Suche nach Grundinstanzen, die schließlich zu einer Re- Fsubs gilt).
solutionsherleitung der leeren Klausel führt, scheint sich nur sehr ineffizient
durch systematisches Durchprobieren aller Grundsubstitutionen realisieren zu Das folgende Diagramm beschreibt diese Situation.
lassen. Es müssen 2.B. die Entscheidungen fiir einige der Gmndsubstitutio-
nen in "vorausschauender" Weise getroffen werden, um Resolutionen, die erst
"'weiter unten" im Diagramm vorkommen, zu ermöglichen. Dies legt eine Mo-
difikation nahe, nämlich die Substitutionen in einer "zuriickhaltenden" Weise
auszuführen, und nur insoweit Substitutionen durchzuführen, wie es für den
direkt nachfolgenden Resoluti onsschritt erforderIich ist.
2.5. RESOLUTION 91
sei s,. Wir behaupten, dass s, die gewünschte Eigenschaft hat. Es gilt M;ui hachte, dass sub keine Gmndsubstitution für L ist, da nach wie vor die
VariabIe y in Lsub vorkommt.
sub,si = s u b , - l [ ~ / t ] ~ ,
= SU~,-~S,[X/~S,] da X in s, nicht ersetzt wird
Oft ist es günstiger, Substitutionen zu "entflechten", so dass alle Teilsubstitu-
= s ~ b , - ~ s , [ x / t s , - ~ ] da X in t nicht vorkommt
tionen voneinander unabhängig in jeder beliebigen Reihenfolge, bzw. parailel,
= SU~,-~S,-~ wegen xsi-1 = ts,-l ausgeführt werden können, ohne das Resultat zu ändern. Eine "entflochtene"
und Definition von s, Version obiger Substitution sub wäre
= sub' nach ~nduktionsvoraucsetzung
Beispiel: Wir wenden den Unifikationsalgonthmus auf die Literalmenge Übung 77: Man zeige, wie man nach Konklitenieren (Hintereinander schrei-
ben) zweier "entflochtenen", also parallel ausführbaren, Substitutionen diese
L = {+(f(2,d a ,Y)), W ]1PIf
, (f (U: W ) , W ) ,hIf Ia, b ) ) ) } wieder entflechten kann.
an und erhalten irn ersten Schritt
Übung 78: Man wende den Unifikationsalgorithmus an auf die Literalmenge
L = {P(&Y), P ( f ( a ) ,s15)l.P(f ( 2 1 , gIf ( 2 ) ) ) ) .
was die Substitution sub = [ J / f (U,V)] ergibt. Irn zweiten Schritt ergibt sich Übung 79: Zeigen Sie, dass der Uni fikati onsalgorithmus (naiv implementiert)
dann, nach Einsetzen von [ z / f ( ? L , V)]: exponentielle Laufzeit haben kann.
Hinweis: Man betrachte das Beispiel
Man ÜberIege sich eine geeignete Datenstmktur für LiteraIe bzw. Literalmen-
Nun wird die Substitution erweitert um [WJ g (rz, y)]. Im dritten Schritt erhalten gen, so dass das Unifizieren effizienter durchgefuhrt werden kann.
wir:
1
fJbung 80: In manchen Implementierungen des Unifikationsalgorithmus'
(z.B. bei Interpretern der Programmiersprache PROLOG) wird aus Effizienz-
gründen auf den Test "kommt s in t vor?" verzichtet (der occur check).
Nun wird stih erweitert um [ u / a ] . Im vierten Schritt Man gebe ein Beispiel einer zweielementigen, nicht unifizierbaren Literal-
menge { L 1 ,L 2 ) an, so dass LI und Lq keine gemeinsamen Variablen enthal-
ten, und ein Unifikationsalgorithmus ohne occur check -je nach Implementie-
rung - in eine unendliche Schleife gerät oder fülschlicherweise "unifizierbar"
konstatiert.
ergibt sich schliel3lich sub = [ X / f (18, T I ) ] [w/g(a,y ) ] [ . i ~ / a[zi/b].
] Dies ist dann
ein allgemeinster Unifikator von L, und es ist Unter wesentlicher Ausnutzung des Unifikationsprinzips sind wir nun in der
Lage, die weiter oben diskutierten Ideen zu realisieren und eine prädikatenlo-
gjsche Version der ResoIurion anzugeben.
94 KAPITEL 2. PRÄDIKATENLOGK 2.5. RESOLUTION 95
Definition (prädikatenlogische Resolution) Notation und erweitern die Bedeutung nun auch auf die Prädikatenlogik. Ins-
Seien K1,K2 und R pr;idi katenlogische Klauseln. Dann i s t R ein prüdi- besondere sei für eine prädikatenlogische Klauselmenge F definiert
kutenlogischer Resolvent von Kr und K2,falls folgendes gilt: &es(F) = F U ( R 1 R ist ein prädikatenlogischer Resolvent
I . Es gibt gewisse Substitutionen SI und s2,die Variablenumbenennungen zweier Klauseln K 1 ,K p E F ) ,
sind, so dass K1sl und K2szkeine gemeinsamen Variablen enthalten. R~s'(F) = F
) n 20
( F ) = Rcs ( f i e s n ( F ) für
2. Es gibt eine Menge von Li teralen L,, . . . ,-
L, -E Kl s,- >
(.ni, I ) und
1tf3"''
und
L i , . . . ,Ln E K2s2 (n 2 l),sodass L = {L1,&,.. . .L,. Li,Li,. . . :
L;} unifizjerbar ist. Es sei sub aIlgemeinster Unifikator von L. Res*(F) = U Resn(F).
n>O
3. R hat dieForm
Nun ist klar, dass U E Xes*(F) genau dann gilt, wenn es eine Folge
. . , L,))
R = ( ( K ~ s-, (LI,. U (K2s2
- (Li,. . . ,L:,)))sub . Kl , K2,. . . , K, von Klauseln gibt, so dass I{,L = 0 , und für z = 1,2, . . . ,n
ist K, entweder Element von F oder X,ist prädikatenlogischer Resolvent
Wir notieren diesen Sachverhalt durch das Diagramm zweier Klauseln K, und Kb mit a , B < i.
wobei möglicherweise die Literale L\, . . . , L„„ L;, . . . , L:, der Deutlichkeit
halber unterstrichen werden und die verwendeten Substitutionen rechts neben
dem Diagramm notiert werden.
Als Vorbereitung für den anschließend zu beweisenden prädikatenl ogischen
Beispiel: Resolutionssatz, zeigen wir nun, dass aussagenlogische Resolutionen von
Grundinstanzen gewisser prädikatenlogischer Klauseln "geliftet" werden
können in pAdikatenlogische Resolutionen. Dieses 'Ti fting-Lemma'' er1aubt
uns dann, die pr2dikatenlogische Resolution auf die aussagenlagische bzw.
die Grundresolution zurückzuführen.
Lifting-Lemma
Seien Ki, K2 zwei prädikatenlogische Klauseln und K i , Ki seien beliebige
Grundnstanzen hiervon, die resolvierbar sind (im aussagenlogischen Sinn),
so dass R' ein Resolvent von K,',K; ist. Dann gibt es einen priidikatenlogi-
Bemerkung: Die aussagenlogische Resolution ist ein Spezial fall der prädi- schen Resolventen B von K1 und K2,so dass R' eine Grundinstanz von R
katenlogicchen Resolution, wobei sl = s 2 = sub = [ ] und rn = 11 = 1 ist.
ist.
Dü die prädikatenlogische Resolution eine Erweiterung der aussagenlogi- Die folgenden beiden Di agramrne veranschaulichen den Sachverhalt.
schen Resolution ist, übernehmen wir die in der Aussagenlogjk eingefühfle
2.5. RESOLUTION 97
Voraussetzung des Lifting-Lemmas Damit ist gezeigt, dass R' eine Grundinstanz von R (mittels Substitution s }
ist. I
t
R'
Behauptung des Lifting-Lemmas
ist unerfüllbar. Eine Deduktion der leeren Klausel aus F ist gegeben durch
2. VxV:g3zP(,'~,y, 2)
(Abgeschl ossenheit)
(1) (T(.)) Klausel in F 2. b"uv.crv?il~z~yb'~((P(x,
y, U) A P ( y , L,V ) ) + ( P ( z :V: W) HP(u, z , W ) ) )
(2) {7T(x), i Q ( x ) l Klausel in F (Assoziativi tät)
Indem wir nun (1) A (2) A (3) A ~ ( 4in) KIauselfom bringen, erhalten wir: Gruppenaxiornen folgere man mittels ResoZutionskalkül:
Übung 85: Man drücke folgende Tatsachen aus als prädikatenlogische For-
meln.
Hierbei sind m (Zstellig), e (0-stellig), i (1-stellig) und k (I -stellig) neu ein- (a} Jeder Drache ist glücklich, wenn alle seine Kinder fliegen
geführte Skolemfunktionen. Eine Resolution~herleitun~ der leeren Klausel kirnnen.
und damit einen Beweis der Unerfüllbarkeit der Klauselmenge (a)-(f) stellt
folgendes Diagramm dar. (b) Gnine Drachen können fi iegen.
(C) Ein Drache ist @n, wenn er Kind mindestens eines grünen Dra-
chen ist.
Man zeige durch Resolution, dass aus (a), (b) und (C) folgt, dass alle gmnen
Drachen glücklich sind.
(a} Jeder Barbier rasiert alle Personen, die sich nicht selbst rasieren.
Man formalisiere (a) und (b) als prädikatenIogische Formeln. Man verwende
B ( x ) für "X ist Barbier'' und R(xl?J)für "X rasiert y". Formen Sie um in
Klauselfom und zeigen Sie per Resolution, dass aus (a) und (b) folgt:
(C) Es gibt keine Barbiere.
der leeren Klausel eine Rolle spielen. Erschwerend kommt hinzu, dass Resol- Resolution vellständig sind.
venten durchaus länger werden können als die Ausgangsklauseln, und damit
die Anzahl der Resolutionsmöglichkeiten im Laufe einer Resolutionsherlei- Die leere Klausel ist aus einer Klauselmenge F linear res»lvierbar; basierend
tung noch zunehmen kann. auf einer Klausel K E F, falls CS eine Folge von Klauseln (Ko,K I , . . . , I L )
Wir stellen nun einige Möglichkeiten der Verfeinerung der Resolution vor, die gibt mit Ka = K, K, = und für i = 1 , 2 , . . . , n gilt
diese kombinatorische Explosion bis zu einem gewissen Grad einschriinken
können. Bei diesen Verfeinerungen unterscheiden wir zwischen Resolutions-
Strategien und Resolutions-Restriktionen.
Strategien sind ledigIich heuristische Regeln, die die Reihenfolge, in
der die Resolurionsschritte vorzunehmen sind, vorschreiben. Die vielen
Wahlmöglichkeiten, die in jedem Schritt existieren, werden hierbei auf ei-
ne bestimmte Art aufgelöst, mit dem Gedanken bzw. der Hoffnung, dass die
jeweilige Strategie möglichst wenige überflüssige Resolventen erzeugt. Im
ungünstigsten Fdl müssen jedoch schließlich auch alle Alternativen durch- wobei die Klausel [eine sogenannte Sei~enklausel)entweder ein Element
gespielt werden. Ein Beispiel ist h e Einheiten- Pru~erenz-Strategie,bei der von F ist oder = K, für ein j < i .
wo immer möglich Resolutionen durchgeführt werden, bei denen mindestens
Wir werden zeigen, dass die lineare Resolution vollständig ist, das heißt, für
eine der Elternklauseln eine Einheit, also einelementig, ist.
jede unerfüllbare Kauselrnenge F gibt es eine Klause1 K (die Basiskiausel),
Diese Strategien scheinen bei den getestetcn Beispielen ganz gut zu funk- so dass die leere Klausel aus F linear resolvierbar ist, basierend auf K.
tionieren, jedoch ist aus theoretischer Sicht unklar und nahezu unerforscht,
ob und inwieweit solche Strategien wirklich und immer zu besseren Resulta-
ten führen. Diesen Strategien soll hier nicht weiter nachgegangen werden. Es Beispiel: Gegeben sei die unerfullbare Klauselmenge
sei nur erwähnt, dass sie sich m ~den
t nachfolgend diskutierten Restriktionen
kombinieren lassen.
Bei den Resotutionsrestriktionen wird die Wahlfreiheit bei der Auswahl der Eine (übliche) Resolutionsherleilung der leeren Klausel ohne Einhaltung ei-
zu resolvierenden Klauseln dadurch cingeschrdnkt, dass gewisse Resolutions- ner dieser Restriktionen benötigt 3 Resolutionsschritte.
schritte schlicht verboten sind, weil die Klauseln nicht die der jeweiligen Re-
striktion entsprechende Form haben. Diese nun zu diskutierenden Rcsoluti-
onsrestriktionen schränken also den Resolutionskdkül echt ein, und verklei-
nern damit i.a. den Suchraum. Es stellt sich natürlich sofort die Frage, ob
solche Restriktionen nicht auch "zu weit" gehen können, so dass der entstün-
dene Kalkül die Vollständigkeitseigenschsift verliert. (Dies wäre dann der Fall,
wenn bei einer unerfüllbaren KIauselmenge F die leere Klausel nicht unter
Einhaltung der Restriktionsbedingung herzuleiten ist). Dies wird im Folgen-
den zu diskutieren sein. Wir stellen nun diese Resolutionsrestriktioncn vor.
Bei der P-Restriktion (oder P-Resolution) darf nur dann ein Resolvent zwei-
er Klauseln K1:K2gebildet werden, sofern eine der beiden Klauseln positiv Eine lineare Resolution dcr Ieeren Klausel aus P, basierend auf ( A ,B}, ist
ist, also nur aus positrven Literalen besteht. Analog darf bei der N-Rrstriktion 2.B. gegeben durch das folgende Diagramm (dies i s t gleichzeitig auch Bei-
(oder N-Resolution) nur resolviert werden, wenn eine der beiden Eltemklau- spiel für eine P-Resolution).
seln nur aus negativen Lrteralen besteht. Wir werden zeigen, dass P- und N-
KAPITEL 2. PRÄDIKATENLOGIK 105
2.6. VERFEINERUNG DER RESOLUTION
einhalt, auch ein linemer Resolutionsbeweis ist. Aber im Unterschied zur li-
nearen Resolution ist die Input-Resolution nicht vollständig. Ein einfaches
Gegenbeispiel ist die unerfüllbare Klauselmenge
F = { { A ,B ) , 1-4,T B ) ,{ T A ,B ) , { T A ,- B ) } .
Bei einer Inputresolution entsteht im ersten Schritt immer ein Resolvent mit
mindestens einem Literal. Bei jedem weiteren Resolutionsschritt können wie-
der nur Resolventen mit mindestens einem Literal entstehen. Die leere Klau-
sel ist bei diesem Beispiel per Input-Resolution also nrcht herleitbar. Wir wer-
den aber später zeigen, dass die Input-Resolution vollstiindig für die Klasse
der Hornfomeln ist.
Man beachte, dass dieser Resolutionsbeweis 4 Schritte benötigt. Man kann
erahnen, dass der Preis, der für die Einschränkung der Wahlmöglichkeiten Eine weitere unvolIständige Resolutionsrestriktion, die aber vollständig für
bei den ResoIutionsrestriktionen bezahlt werden muss, in einer Zunahme der die Klasse der Hornfomeln ist, ist die Einheitsresolution (vgl. Ubung 35).
Beweislänge liegt. Diesen Effekt genau zu quantifizieren ist aktuelles Thema Es darf nur dann ein Resolvent gebildet werden, wenn mindestens eine EI-
der Forschung (vgl. hierzu Ubung 87). ternklausel einelementig ist. Diese Resolution srestriktion hat den Vorteil,
dass die Anzahl der Literale bei jedem Resolutionsschritt abnimmt. Die Un-
Bei der Stiitzmengenresta'ktiun der Resolution muss zu der gegebenen Klau- vollständigkeit der Einheitsresolution ist durch das gleiche Gegenbeispiel
selmenge F erne Teilmenge T bekannt sein, so dass F - T erfüllbar ist. Ein wie bei der Input-Restriktion einzusehen. (Diese Ähnlichkeit mit der Input-
Resolutionsbeweis der leeren Klausel aus F, relativ zur Stiitzmenge T, muss Restriktion ist kein Zufall: Es kann gezeigt werden, dass eine Klauselmenge F
die Bedingung erfüllen, dass niemals zwei Klauseln aus F - T miteinander einen Einheitsresolutionsbeweis der leeren Klausel besitzt genafi dann, wenn
resolviert werden. Diese Einschränkung bringt vor ailem dann Vorteile, wenn F einen Input-Resolutions'beweis der leeren Klausel besitzt, vgl. Ubung 91).
T besonders klein und damit F - T besonders groß ist, z.B. bei IT I = 1.
Dadurch wird eine große Zahl von potenziellen RcsoIutionsschritten (zwi- Schließlich kommen wir zur Sm-Resolution. Diese Restriktion ist nur für
schen Klauseln in F - T) vermieden. Ein typisches Anwendungsbeispiel ist, Hornformeln definiert (bzw. wir betrachten ihre Verallgemeinerung auf be-
dass festgestellt werden soll, ob eine Formel G eine Folgerung der "Daten- liebige Klauselmengen, die SL-Resolution hier nicht). Diese Resolutionsre-
bank" { F l ,&, . . . , Fk} ist. Dies ist bekanntermasen genau dann der Fall, striktion spielt eine entscheidende Rolle bei der Logik-hgrammierung, die
wenn { F I ,Fz, . . . ,Fk,1G) unerfüllbar ist. Falls aus dem Kontext bekannt wir im nächsten Kapitel diskutieren wollen. SLD-Resolutionen sind Input-
ist, dass {Fl, F2,. . . , Fk} ftir sich allein noch nicht unefiüllbar, also erfüllbar, (und damit auch lineare) Resolutionen, die eine spezielle Form haben. Und
ist; oder falIs diese sog. Konsistenz der Datenbank einfach postuliert wird, sa zwar muss die Resolutionsherleitung auf einer negativen Klausel (crner sog.
kann man als Stützmenge T = {G,, . . . , G I )wählen, wobei { G I ,. . . , G I )die Zielklausel} basieren, und bei jedem Resoluti onsschritt ist eine E1ternkl ausel
Klauselfonn von 1G ist. eine nicht-negative Inputklausel. (Nicht-negative Hornklauseln heißen auch
definite Khuseln oder Pmgrnmmkla~seln}.
Wir werden später sehen, dass die Stützmengenresolution vollständig ist.
Sei z.B. F = {Kl,K z ,. . . ,Km iV1:.. . ,;Vm),wobei K l , I&, . . . , K, die de-
Bei der Input-Restriktion muss bei jedem Resolutionsschritt eine der beiden finiten und &,. . . , n', die negativen Klauseln sind. Eine SLD-Resolutions-
Elternklauseln ein "Input", also Element der Ausgüngsklauselmenge F sein. herleitung der leeren Klausel hat dann die folgende Form (fur ein geeignetes
Man sieht leicht ein, dass jeder Resolutionsbeweis, der die Tnput-Restriktion 3 E (1,. . . :m ) und eine geeignete Folge i I ,i,, . . . , zl f { I , . . . , n)).
KAPITEL 2. PRÄDTKATENLOGTK 2.6. VERFEINERUNG DER RESOLUTION 107
Als Vorbereitung für diese Beweise führen wir folgende Notation ein. Für
eine (aussagenlogische) Klauselmenge F und ein in F vorkommendes Litera1
L sei FL=*die Klauselmenge, die man aus F erhält, indem jedes Vorkommen
von L und ferner jede Klausel, in der ¿ vorkommt, gestrichen wird. Analog
sei FL=ldefiniert, wobei die Rollen von L und ¿ vertauscht sind. Inhaltlich
gesprochen ist FL=ai(L E { O , l ) , diejenige Klauselmenge, die aus F entsteht,
wenn die Belegung von L mit a fixiert wird. Deshalb gilt, dass sowohl FL="
als auch FLZIunerfiillbar sind, sofern F unerfüllbar ist.
Satz
Die P-Restriktion der Resolution ist vollständig.
Beweis: Wie oben bemerkt, genügt es, den aussagenlogischen Fall zu betrach-
ten. Sei F eine unerfüllbare aussügenlogische Klauselmengc. Wegen des End-
Die hierbei durch Punkte dargestellten Klauseln, also die "Zwischen- lichkeitssatzes dürfen wir wieder annehmen, dass F endlich ist. Wir zeigen
resultate", können nur negative Klauseln sein, da sie durch Resolu- durch Induktion über die Anzahl der atomaren Formeln in F, dass die leere
tion einer negativen mit einer definiten Hornklausel entstehen. Das Klausel per P-Resolution aus F herleitbar ist.
heißt, SLD-Resolutionen sind immer auch N-Resolutionen. Gleichfalls Induktiunsanfang (n = 0): FalIs n = 0, so kann nm F = { U ) sein, und wir
sind SLD-Resolutionen auch immer Stützmengenresolutionen, wobei die srnd fertig.
Stützmenge { N I , .. . , Nm)ist. Induktionsschritt (n > 0): Die Klauselmenge F besitze n > 0 Atomfomeln.
Sei A eine beliebige Atomforrnel in F. Da und FAXOunerfullbar sind
Bemerkung: Die Abkürzung SLD steht für "Iinear resolution with selection und höchstens n - 1 Atornformeln enthalten, folgt mit der Indukrionsvor-
function for definite clauses". In unserer Betrachtung ignorieren wir zunächst aussetzung, dass die leere Klausel per P-Resolution sowohl aus FA=0als auch
diesen zusätzlichen Aspekt einer Auswuhlfunktion, die in jedem Resolutions- aus FA=1herleitbar ist. Wiederherstellen der ursprünglichen Klauseln in FA=*
schritt dasjenige Litera1 angibt, nach dem als nächstes zu resolvieren ist. Wjr (d.h. Wiederei nfügen von A) liefert dann eine Resolutionsherleitung von { A}
kommen jedoch auf diesen Punkt in Kapitel 3.3 zurück. Für den Moment be- aus den Klauseln in F. Diese Herleitung von { A } stellt immer noch eine P-
trachten wir die SLD-Resolution als identisch mit der sog. LUSH-Resrilution Resolution dar, da A ein positives Litera1 ist. Nun fügen wir weitere Resoluti-
(LUSH = linear resolution with unrestricted selection for Hornclauses). onsschntte hinzu, die die so erhaltene Klausel { A )mit jeder Klausel in F, die
T A enthält, resolviert. Man beachte, dass dieses wiederum P-Resolutionen
AIle VolIständigkeitsbeweise der Resolutionsrestriktionen werden zunächst sind. Damit haben wir gerade die Klauseln in FA=lbereitgestellt. Sodann
für den aussagenlogischen Fa11 (also für die Gnindinstanzen der prädikaten- fügen wir den nach Induktionsvoraussetzung existierenden P-Resolutionsbe-
logischen Klauseln) gezeigt. Wie irn Beweis des allgemeinen Vollständig- weis der leeren Klausel an, der die Klauseln in als Ausgangspunkt hat.
keitssatzes für die prädikatenlogische Resolution verwenden wir das Lifting- Das Ergebnis ist nun eine P-Resolutionsherleitung der leeren Klausel aus F.
Lemma, um aussageniogische Resolutionsbcweise, die der entsprechenden
Restriktion genügen, in die Pradikatenlogik zu "liften". Man beachte, dass
durch das Lifting-Lemma die Struktur einer Resolutionsherleitung nicht
Satz
geändert wird, so dass eine P-,N-, lineare, usw. -Resolution nach Anwendung
des Lifting-Lemmas immer noch eine solche ist. Um die Vollständigkeit einer Die N-Reskiktion der Resolution ist vollständig.
Restriktion in der Aussagenlogik zu zeigen, muss der Vollständigkeitssatz für Beweis: Man vertausche im vorigen Beweis die Rollen von "positiv" und
den aussagentogischen Resolutionskalkül entsprechend modifiziert werden. "negativ", von "A" und "TA", und von "FA=o"und "FA=l". I
2.6. VERFEINERUNGDER RESOL UTION 109
Satz F' - {K). Dann gilt A ( K ) = 0, denn es gilt A ( F t ) = 0, weil F' unefillbar
Die lineare Resolutionsrestriktion ist vollstandig. (Genauer: Für jede unerfüll- ist. Somit folgt A(L)= 0, da L E K. Damit ergibt sich A(FL=,- { K ' ) )= 1.
bare Klauselmenge F gibt es eine Klausel K E F, so dass die Icere Klausel Sei F" eine minimal unerfüllbare Teilmenge von FA=,. Wie soeben gezeigt,
durch lineare Resolution aus F, basierend auf K, herIeitbar ist). muss F" die Klausel K' enthalten (denn Weglassen von K' wurde Erfüll-
barkeit nach sich ziehen). Auf F" trifft die Induktionsvoraussetzung zu und
Beweis: Sei F unerfüllbar und F' C F sei eine minimal unerfüllbare Teil-
deshalb gibt es eine lineare Resolutionsherleitung der leeren Klausel aus F",
menge von F (d.h. F' ist unerfüllbar, aber für jede Klausel IC E F' gilt, dass
basierend auf K'. In diesem Resolutionsbeweis fugen wir nun das Litera1 L
F' - {K) erfüllbar ist. F' kann aus F konstruiert werden, indem sukzessive
überall wieder hinzu, wo es zuvor weggelassen wurde (und damit auch in den
Klauseln aus F entfernt werden, bis nur noch Klauseln übrig bleiben, deren
Resolventen). Dies ergibt eine lineare Resolutionsherleitung von {L) aus F',
Entfernen zur Erfüllbarkeit führt). Wir zeigen nun, dass sogar für jede Klau-
basierend auf K.
sel K in F' gilt, dass es eine lineare Resolutionsherleitung der leeren Klausel
aus F gibt, die auf K basiert. Sei K eine beliebige Klausel in F'. Wir fuhren Nun ist aber (F' - {K)) U {{L)) unerfüllbar und F' - {K) erfüllbar. Unter
den Beweis nun durch Induktion über die Anzahl der in F' vorkommenden Verwendung von Fall I wissen wir, dass eine lineare Resolutionsherleitung
atomaren Formeln. von aus (F' - ( K } )U ({L)) exisnert, basierend auf {L). Wir fügen nun
diesen Resolutionsbeweis an den oben erhaItenen Resolutionsbeweis, der (L)
Induktionsanfang (n = 0) : In diesem Fall ist F' = {D} und K = . Hier ist
liefert, hinten an und erhalten so die gewünschte Resolutionsherleitung von
nichts zu zeigen.
aus F', basierend auf K.
Induktionsschritt (n > 0): F' enthaIie n > 0 Atomfomeln.
FalEI: IKJ = 1
Dann ist K = {L} für ein Literal L. Für eine Atomfomel A ist dann L = A Übung 87: Sei F diejenige unerfüllbare Wauselmenge mit den Atomfor-
oder L = TA. Die Klauselmenge F;=, ist dann unerfüIlbar und enthält nur meln A l , . . . , Am die alle m = 2" Klauseln der Form {B1, B„. . . , B,) mit
höchstens n - 1Atomfomeln, denn A kommt nicht mehr vor. Sei F" eine mi- B, E {A„TA,) enthdt. Die übliche Resolutionsherleitung der leeren Klausel
nimal unerfüIlbare Teilmenge von FA=,. In F" muss eine Klausel K' vorkom- aus F enthält 7n - 1 Resolutionsschritte. Man ermjttle aus den Vollständig-
men, so dass K'u(E} 6 F',d.h. K' ist gerade durch Streichen von aus einer keitsbeweisen der P-Resolution und der linearen Resolution Rekursionsglei-
Klausel in F' entstanden. Eine solche Klause1 K' muss deshalb in F" existie- chungen für die Länge der konstruierten Resolutionsherlei tungen unter diesen
ren, weil sonst F" eine Teilmenge von F' - { K } und damit erfüllbar wäre Restriktionen. Lösen Sie diese Rekursionsgleichungen und vergleichen Sie
(da F' minimal unerfüllbar ist). Nach Induktionsvoraussetzung gibt es nun ei- diese Formeln mit m - 1.
ne lineare ResoIutionsherleitung der leeren Klausel aus F", basierend auf der
Klausel K'. Hieraus konstruieren wir die gesuchte lineare Resolutionsherlei- Satz
tung von 0, basierend auf K = {L}, wie folgt: Der erste ResoIutionsschritt Die Stützmengen-Restriktion der Resolution ist vollständig.
resolviert die Basisklausel K = {L} mit K' U { E ) . Der Resolvent hierbei
ist K< Sodann übernehmen wir obige, auf K' basierende ResoIuiionsherlei- Beweis: Dies folgt aus der Vollständigkeit der linearen Resolution. Sei F ei-
tung der Ieeren Klausel, wobei wir nun die wiederhergestellten, ursprüngli- ne unerfüllbare Klauselmenge und T C. F eine Stützmenge, d.h. F - T ist
chen Klauseln aus F (also evtI. mit dem Literal E) hernehmen. Hierdurch erfüllbar. Eine minimal unerfüllbare Teilmenge T' von F muss mindestens
entsteht eine lineare Resolutionsherleitung von { E ) , basierend auf I< = {L}. eine Klausel K aus T enthalten, denn F - T ist erfiillbar. Mit dem vori-
Im letzten Resolutionsschritt schließIich resolvieren wir die Basisklausel K gen Beweis folgt, dass es eine lineare Resolutionsherleitung gibt, basierend
mit { E ) und erhalten che leere Klausel. auf K. Dies ist gleichzeitig eine Stützmengenresolution mit Stützmenge ( K )
und damit auch mit Stützmenge T. m
Fall 2: 1KI > 1
In diesem Fall whhihlen wir ein beIiebiges Literal L 6 K und setzen K' =
K- {L). Nun ist unerfüllbar und X'ist eine Klausel in F;=, . WFTzeigen Übung 88: Man zeige, dass die Kombination zweier vollständiger Restrik-
nun, dass F;=, - { K ' } erfuI1bar ist. Hierzu sei zunächst A ein Modell von tionen i.a. nicht mehr voItständig ist. Hierzu betrachte man zwei vollständige
Resolutionsrestriktionen (z.B. P-Resolution und N-Resoludon) und gebe ein
110 KAPITEL 2. P R Ä D I I C A ~ N Z O G - I K 2.6. VERFEINER LNG DER RESOLUTrON
Beispiel einer unerfüllbaren Klüuselmenge an, so dass die leere Klausel unter Satz
Einhaltung beider Restriktionen nicht herleitbar ist. Die Input-Resolution ist vollständig für die Klasse der Hornformeln.
Wir wenden uns nun den im Allgemeinen Fall unvollständigen Resolutions- Beweis: SLD-Resolutionen sind auch Input-Resolutionen.
restriktionen zu und erhalten sofort den folgenden Satz (vgl. Übung 35).
Übung 90: Man zeige, dass die Vollständigke~tder Input-Resolution für
Satz Hornformeln ebenso einfach aus der Vollstindigkeit der N-Resolution folgt.
Die Einheitsresolution ist vollständig für die Klasse der Hornformeln.
Übung 91: Man zeige, dass für jede Klauselmenge F gilt: Es gibt einen Ein-
Beweis: Da die P-Resolution für den allgemeinen Fall vollständig ist, ist sie es heitsresolutionsbeweis der leeren Kiausel aus F g e m u dann, wenn es einen
auch für den speziellen Fall der Hornfomeln. Positive Hornfomeln kiinnen Input-Resolutjonsbeweis gibt.
jedoch nur einelementig sein. Damit folgt sofort, dass die Einheitsresolution
für Hornformeln volFständig ist. I
Übung 92: Man zeige, dass die Vollständigkeit des Resolutionskalküls nicht
verloren geht, wenn man solche Resolutionsschritte verbietet, bei denen eine
Satz Elternklausel eine Tautologie ist. Eine Klause1 ist genau dann eine Tautologie,
Die SLD-Resolution ist vollständig für die Klasse der Hornfomeln. falls sie eine Atomfomel und ihr Komplement enthält.
Beweis: Sei F eine unerfüllbare HornklauseImenge. Eine KlauseIrnenge ist Übung 93: Falls bei einem Resolutionsschritt in den Elternklauseln jeweils
erfüllbar, wenn sie keine negativen Klauseln enthält (man setze A ( A ) = I nur ein Litera1 zur Unifikation herangezogen wird, so spricht man von binärer
für aIIe Atomformeln -4, dann ist A ein Modell). Deshalb muss in F minde- Resolution. (Mit anderen Worten, in der Definition der priidikatenlogischen
stens eine negative Klausel enthalten sein. Mehr noch, beim Ubergang von F Resolution ist m = n = I gesetzt}.
zu einer minimal unerfüllbaren TeiImenge F' von F, muss mindestens eine Man zeige durch Angabe eines Gegenbeispiels, dass die Beschränkung auf
negative KIausel K in F' verbleiben. Wegen der Vollständigkeit der linearen binäre Resolutionen nicht vollständig ist. Man zeige ferner, dass binike Reso-
Resolution gibt es dann einen linearen Resolutionsbeweis der leeren Klausel lution für Hornformeln vollständig ist. Mehr noch, jede der bei Hornfomeln
aus F' (also auch aus F), basierend auf K. Diese lineare Resolutronsherlei- vollständigen Restriktionen bleibt vollständig, wenn man sie mit der binärcn
tung muss ferner die Form einer Input-Resolutron haben, denn alle Resolven- Resolution kombiniert. (Tatsächlich ist es genau diese Kombination von binä-
ten obiger Herleitung sind negative Klauseln (Resolventen von Aornklauseln rer und Sm-Resolution, die im nächsten Kapitel intensiver betrachtet wird).
mit negativen KIauseln sind negative Klauseln), und negative Klauseln sind
nicht mit negativen Klauseln resolvierbar. Dieses Argument beweist, dass die-
se lineare Resolution sogar die spezielle Form einer SLD-Resolution hat. W Bemerkung: Wir haben einen groAen Aufwand betrieben, um die Möglich-
keiten, die die Semi-Entscheidbarkeit der Prädrkatenlogik bietet, also die Aus-
sicht, automatische Theorembeweiser zu konstruieren, auszuschöpfen. Trotz
Übung 89: Beweisen Sie die Vollständigkeit der SLD-Resolution für Horn- alledem zeigt die praktische Erfahrung, dass selbst Theorembeweisprogram-
forrneln direkt, also ohne Zuhilfenahme der Vollständikeit der linearen Reso- me, die diese vorgestellten Resolutionsrestriktionen (und evtl. andere Metho-
lution. den) verwenden, nicht in der Lage sind, mit vertretbarem Aufwand kompli-
Hinweis: Orientieren Sie sich an dem Ablauf des Marluerungsalgorithrnus' ziertere Theoreme zu beweisen -oder gar die Mathematiker zu ersetzen.
für Hornfomeln von Kaprtel 1.3. Eine andere Möglichkeit besteht darin, Dies mag daran liegen, dass der Ansatz noch zu aIlgemein ist. Sei M =
Ubung 38 (in verallgemeinerter Form) zu verwenden. {Fl,F2,. . . ,Fk) ein beliebiges Axjomensystem. Der Resolutionskalkül ist
grundsätzlich in der Lage, nachzuweisen, ob eine Formel G ein Satz der
Theorie Cons(M), also eine Folgerung von M, ist. Man muss nur testen,
ob ( F l , Fz, . . . , Fk,1 G ) unerfüllbar ist. Oftmals ist man aber nur an ganz
bestimmten (axiomatischen) Theorien interessiert, etwa der Gmppentheorie.
Deshalb wird versucht, Kalküle zu entwickeln, die auf diese speziellen Theo-
rien zugeschnitten sind, und die dann effizienter (aber nur für Sätze dieser
Theorie) verwendet werden können. Solche Kalküle verkörpern sozusagen
mehr Wissen über die zugrundeIiegende Theoie.
Kapitel 3
Logik-Programmierung
F = { {liebt(Eva,Essen)),
{liebt {Eva,Wein)},
{liebt(Admrn,X ) , -liebt (X,Wein)})
Hierbei ist liebt ein zweistelliges Prädikatsymbol, und Eva, E.v.sen, Wein,
Adam stellen Konstanten dar. Inhaltlich konnten die Klauseln in F folgendes
bedeuten:
KAPITEL 3. LOGIK-PROGR AMMlER UNG 3.1. ERZEUGEN VOAV ANTWORTEN 115
"Eva liebt zu essen" Da die leere Klausel herleitbar ist, ist G tatsächlich eine Folgerung von F.
"Evaliebt Wein" Es gibt also jemanden, den Adam liebt. Aber wen'? Nun, dies kann an den
'Adam liebt jeden, der Wein liebt" Substitutionen abgelesen werden, denen die fragliche Variable I/ im Verlauf
der Resoluitionsherleitung der leeren Klausel unterworfen ist. In unserem Fall
Hiermit ist der aiigemeine (zugegebenermaßen nicht sehr tiefsinnige) Pro- wird y durch Eva im 2. Resolutionsschri tt ersetzt und dies ergibt die Antwort:
blemkontext beschrieben. Ein Aufiuf dieses Programms könnte nun die For- ''Adam liebt Eva".
mel
Eine Möglichkeit, den Substitutionsprozess transparent zu machen, ist
G = 3p laebt(Ada~n, y)
das Einfügen eines Antwor~prüdikats.Anstelle der ursprünglichen (von
sein. InhaItlich bedeutet dies: "Gibt es jemanden, den Adam liebt?" und G stammenden) Arafrufklausel {~Eiebt(Adam, g ) ) wählen wir nun (-hebt
zusätzIich - dies ist der Antworterzeugungsaspekt - "Wer ist dies?'. Typisch (Adam,y); Antwort (y]}. Ziel ist nun nicht mehr die Resolution der lee-
für eine solche als Frage aufgefasste FormeI, wie G, sind die vorkommenden ren Klausel, sondern die Resolution einer Klausel, die nur noch aus emem
Existenzquantoren. Es so11 hierbei nicht nur die Fragc, ob die Existenz eines (oder cvtl. mehreren) Antworiprädrkat(en) besteht. Bei unserem Beispiel er-
(oder mehrerer) Objekte mit gewissen Eigenschaften aus dern Programm F gibt sich:
folgt, vom Auswertungsmechanjsmus (dem Logik-Progmmminteyreter) mit
ja oder nein beantwortet werden. Es soll vielmehr im ja-Fall ein entsprechcn- X), ~ l a e b t { zWein))
,
des Objekt (oder mdglicherweise alte) ausgegeben werden.
In der Terminologie vom Ende des Abschnitts 2.3 kann der Sachverhalt auch
so gedeutet werden, dass F ein Axiomensystem für eine gewisse Theorie,
nämlich Cons(F),darstellt, und es so11 die Frage beantwortet werden, ob G
ein Satz dieser Theorie ist.
Mit anderen Worten, wir wollen wissen, ob G aus F folgt. Wir testen dso
mittels Resolution, ob F A 1G unerfülIbar ist. Es gilt
F A 1G { (liebt(E?ie,Essen)), Ein Beispiel, in dem die Antwort etwas komplexer ausfällt, ist folgendes.
{lzebt(Eva, Wein)],
(liebt (Adam,X),daelit(z, Wezn)}: { {laebt(Eva,Essen)),
{-liebt(Adam, y ) } }. liebt(Anna, Wein,)),
{Iiebt(Eua, Weir~),
{lieht(Adrzm.z),~lzebt(z,Ween)},
Eine Herleitung der leeren Klausel ist dann gegeben durch folgendes Dia- {llzebt (Adam,y) , Antwort(y)) }
gramm.
Dies bedeutet inhaltlich:
Variable(n) des Logik-Programms und die Ausgabeparameterübergabe durch Diese das Logik-Programm darstellenden Klauseln beschreiben die Problem-
die Substitutionen für die Variable(n) des Antwortprädikates. situazion. Zur Beantwortung der Frage
Nun beachte man, dass ein und dasselbe Logik-Programm F auch verwendet
werden kann miic einer anderen Aufrufkiausel, etwa
also "gibt es einen Zustand, in dem der Affe die Banane erreicht hat - und wie
ist dieser Zustand herzustellen?" wird die Frage negiert und in Klauselform
wobei nun die Rollen von Eingabe- und Ausgabeparameter vertsiuscht sind. überfuhrt. Dies ergibt zusammen mit dem Antwortpriidikat
Man kann also sowohl feststellen, wen oder was Eva liebt (Essen und Wein),
als auch, wer Eva Liebt (Adam). Man spricht von Invertibilitiis des Parame-
terübergabemechanismus'.
Eine Resolutionsherleitung der reinen Antwortklausel ist dann gegeben durch
die Folge K1, K 2 ,K3,K4,Kr;mit
Tm nächsten Beispiel, dem bekannten Affe-und-Bananen-Problem, kommen
Funktionssymbole vor, die hier die Rolle von Operatoren auf einem "Zu-
standsraum" (dem Herbrand-Universum) übernehmen, wobei das Ziel darin
liegt, einen Anfangszustand so mittels dieser Operatoren zu verändern, bis K1 = (+(X, ;C, 2,climb(s) j, Antwort (grasp(climb(s)))}
ein gewünschter Endzustand erreicht wird. Gegeben seien folgende Klauseln (Resolvent von ( 5 ) und (6))
Kz = {~P(x,z,z,s),Ant~~~~~t(~rasp(climb(s))))
(Resolvent von (4) und K I }
Interpretation: "In der Startsituation d befindet sich der Affe bei K3 = { ~ P ( yx ,;X ,s) , Aratwort(grccp(clirnb(p~csh(x~
y, s)))))
Position a,die Banane hängt unter Position 8, und der Stuhl steht (Resolveni von (3) und K2)
bei Position C." werbei sind n, Ii, c, d Konstan tcn).
Kq = { i P ( x ,Y)J , s ) , Antwort(grasp(cli~nh(push(x. y, walk(x, 2 , s)))))}
(2) { l P ( x IY,2 , s ) ,P ( w , Y,Z , walk(x;U ] , s))} (Resolvent von (2) und K 3 )
"Wenn sich der Affe in der Situation s bei Position s befindet, K5 = ( ~ n t w o r t ( g m s ~ ( c 1 i m b ~b,uwalk(n,
s h ~ C,d ) ) ) ) ) }
so bewirkt die Anwendung der Funktion wa&k(x,ui,s), dass der (Resolvent von (1) und K4)
Affe nachher bei Position ru ist. M.a.W., der Affe kann zu jeder
Position hinlaufen." (Hierbei sind X;?I, z , s, w Variablen). Interpretation der Antwort: ''Ausgehend von der Situation d gehe von CL nach
C, schiebe den Stuhl von C nach b, ersteige den Stuhl und ergreife die Banane".
"Wenn der Affe beim Stuhl ist, so kann cr den Stuhl zu jeder
Position ui schieben". Übung 95: Sechs Münzen, die auf der Vorderseite eine Zahl und auf der
Rückseite einen Kopf zeigen, liegen in folgender Anordnung:
"Wenn der Affe beim StuhI steht, so kann er jederzeit darauf stei- Kopf Kopf Kog( Zahl a h l Zahi
gen".
(5) { y P ( a ;2,X, climb(s)),Reach~rnsp(clirnb(s)))} In einem Zug dürfen je zwei nebeneinanderliegende Münzen umgedreht wer-
'Wenn der Affe auf den Stuhl gestiegen ist, und die Position von den. Gesucht ist eine Folge von Zügen, die die Münzen in h e Anordnung
Stuhl, Affe und Banane übereinstimmen, so kann der Affe durch
Greifen nach der Banane diese erreichen." Zahl Kopf Zahl Kopf Zahl Kopf
bringt. Fomuiieren Sie ein entsprechendes Logik-Programm. schnitt formale Sätze über Korrektheit und Vollständigkeit des Antworterzeu-
gungsprozesses TU beweisen).
Übung 96: Drei junge Frauen und ihre drei eifersüchtigen Freunde möchten Der dritte Grund für die Beschrrinkung auf Hornklauseln ist die Effizienz. Tm
an den Strand fahren. Als Transportmittel steht ihnen nur ein Sportwagen mit aussagenlogischen Fall haben wir sehr effiziente Algorithmen auf der Klasse
zwei Sitzgelegenheiten zur Verfügung. Wie stellen sie es an, die Fahrten so der Hornformeln kennengelernt - ganz irn Gegensatz zu den exponentiellen
zu arrangieren, dass zu keinem Zeitpunkt eine Frau mit einem anderen Mann Algorithmen im allgemeinen Fall. Eine gewisse Form der Effizienz bei Horn-
beisammen ist - außer der eigene Freund ist dabei? Man formuliere ein Logik- iormeln schlägt auch nmh im prSdikatenlogischen Fall durch (wenngleich
Programm mit Antwortprädikat. die Gültigkeit und Erfüllbarkeit auf der Klasse der pddikatenlogischen Horn-
klauseln gleichfalIs unentscheidbar ist).
Übung 97: Man formuliere das folgende Rätsel in der Prädikatcnlogik und Insbesondere ist es die Vollständigkeit der SLD-Resolution für die Klasse der
verwende die Antwortprädikatmethode, um es zu lösen. Hornformeln, die hier attraktiv i s t , denn SLD-Resolutionsherleitungen haben
Tom, Mike und John gehören dem Alpenverein an. Jedes Mitglied des Alpen- bereits den Charakter von sequentiell ablaufenden Berechnungen und sind
vereins ist entweder Skifahrer oder Bergsteiger oder beides. Kein Bergsteiger deshalb für eine prozedurale Interpretation von Hornklauselprogrammen be-
liebt den Regen und alle Skifahrer lieben den Schnee. Mike liebt alles, was sonders geeignet. Tm Hinblick auf diese pmzedurale Tntepretation unterschei-
Torn nicht liebt und umgekehrt. Mike und John lieben den Schnee. Gibt es den wir folgende Q p e n von Hornklauseln.
ein Mitglied des Alpenvereins, das Bergsteiger ist und kein ShFhrer? Wer ist Tatsachenklauseln sind einelementige positive Klauseln, diese bestehen also
dies? nur aus einer positiven Atomfomel. Diese Klauseln steilen die Behauptung
eines Faktums dar.
Übung 98: Man finde mit der Antwortprädikatmethode nachtriiglich heraus,
wie die rechtsinversen Gruppenelemente bei dem Beispiel in Abschnitt 2.5 zu Prozedurklauseln haben die Form {P,7 Q I , .. . ,Y&), wobei P, C), . . . , Q k
wählen sind. prädikatenlogische Atomfomeln sind. Die Notation in PROLOG, nämlich
Eine Zielklausel besteht also aus einer Folge von Prozedurüufrufen. Sie stellt also "berechne 3+2, und liefere das Resultat in u ab". Eine standardisierte
das Berechnungsziel dar; jede der Prozeduren Q,, . . . , Qk soll erfolgreich SLD-Herleitung der leeren Klause1 ist gegeben durch das folgende Diagramm
ausgeführt werden. (hierbei ist z' eine durch Umbenennung entstandene Variable).
Beispiel: Betrachten wir die rekursive Definition der Addition (wobei y' den
Nachfolger von y bedeutet):
Um es deutlicher zu machen, können wir die Substitution subl suh2sttb3 auch
direkt auf die in der ZielHause1 vorkommende Vüriable u anwenden und wir
erhalten:
M.a.W., das Resultat ist 5. Diese Art der Bestimmung des Rechenresultats 1st
Hierbei bedeutet A ( x , y, L), dass X + y = z, und s stellt die Nachfolger-
in der Wirkung identisch mit der Antwortpriidikatmethode des vorigen Ab-
funktion dar. Die Klauseln ( I ) und (2) sind das Logik-Programm und eine
LielkIausel könnte 2.B. sein: schnitts. An diesem Beispiel kann man erkennen, dass in der reinen Form der
Logik-Programmiening keine arithmetischen Berechnungen ausgeführt wer-
den können, lediglich Symbolmanipul;itionen. (Wir haben "s(s(s(s(s(0)))))"
als Resultat erhalten und nicht "Y.) Die Möglichkeit, Funktionen oder Priidi- wohldefiniert ist, d.h. jedes Berechnen von a(x, mit X ,y E IN führt nach
kate zu evaluieren,muss in einer konkreten Programmiersprache (wie PRO- endlich vielen Schritten zum Ziel.
LOG) natürlich zusätzlich vorgesehen sein. Auf diese nicht-logischen Aspek- Formulieren Sie ein entsprechendes Logik-Programm fiir die Ackermann-
te einer Logik-Programmiersprache gehen wir hier jedoch nicht ein. funktion!
Übung 99: Das oben beschiebene Logik-Programm für die Addition kann Wir wollen diese beispielhaft eingeführten Konzepte nun formalisieren irn
auch zum Subtrahieren verwendet werden. Wie? Hinblick auf eine rigorose Definition der prozeduralen Semantik eines Logik-
Programms. In der folgenden Definition wird insbesondere hervorgehoben,
Übung 100: Man füge zu dem Logik-Programm für die Addition weitere Pro- dass in der Folge der berechneten allgemeinsten Unifikatoren das Rechener-
grammklauseln hinzu, die es erlauben, die Fibonaccifunktion zu berechnen. gebnis einer SLD-Resolution entsteht.
Diese ist die Funktionfib mit
Definition (prozedurale Interpretation)
Die prozedurale Interpretation von Wornklauselprogrammen ist gegeben
durch die Angabe eines abstrakten Interpreters für diese Programme. Hierzu
definieren wir als Konfiglcrationen des Interpreters alle Paare (G, sub), wobei
G eine Zielklausel und sub eine Substitution ist.
Sei F ein Logik-Programm. Kunafigürationsübergänge (in Bezug auf F) wer-
Übung 101: Man formuliere ein Logik-Programm für die Addition, das auf den wie folgt definiert: Es gilt (G1, s u b l ) k (Gz,subzj, falls G1 die Form
folgender rekursiver Darstellung beruht: hat
G1 = ( l A i , TA?,. . . , l A k ) ( k 2 1)
und es eine Programmklausel
Falls es sich um eine endliche Rechnung handelt, und die letzte Konfiguration
während a(4,2) bereits mehr als 19 000 Dezimalstellen hat! Beweisen Sie hierbei die Bauart (n,sub) hat, SO heißt diese Rechnung erfolgreich und die
diese Behauptung und weisen Sie ferner nach, dass diese Darstellung von a Formel (Al A . . . $i Ak)sub ist dann das Reclienergebnis.
126 KAPITEL 3. LOGIK-PROGRAMMIERUNG
Man erkennt, dass Rechnungen (in Bezug auf die ersten Komponenten der
Konfigurationen) nichts anderes d s standardisierte SLD-Resoiutionen dar-
stellen. Es kommt lediglich in der zweiten Komponente der Konfigurationen
hinzu, dass über die jeweils berechneten allgemeinsten Unifikatoren buch-
geführt wird - ahnlich der Antwortprädikatmethode von Abschnitt 3.1. die nicht weiter fortgesetzt werden kann. Hierbei wurde zur Resolution die
Man beachte ferner, dass d~eseRechnungen von Hornklauselprogrammen l., 3., 1. und 2. Programmklausel herangezogen. Es gibt jedoch auch zwei
nichldetenninistisch sind, d.h. jede Konfiguration kann evtl. mehrere Nach- erfolgreiche Rechnungen mit jeweils unterschiedlichen Rechenergebnissen.
folgekonfigurationen besitzen. Die möglichen Rechnungen eines Log~k- Dieses sind
Programms F bei gegebener Eingabe G kann man sich somit als Baum vor-
stellen. (i+(.: bS1, [ I)
(mit 1.
k ( ( l Q ( v , Y), ~P(Y,
b)}. [ ~ / v ] [ ~ / ~ ] ) Programmklausel)
(G3 S?Eb3) r
'
(mit 3.
( I l P ( 46) 1,IJ/~:I[+dhLu/1u ] kdbj) Prngrxnmklausel)
{mit 2.
F (Gd1~ u b d )
(G1 [ I) (G5;S
USW.
T E ~ ~ )
und
({-p(vl 1:[ 1) (mit 2.
Programmklausel)
Wenn man von Nachfolgekonfigurationen absieht, die sich nur durch Varia- Die erste Rechnung liefert das Rechenergebnis
blenumbenennungen von anderen unterscheiden, so ist dieser Baum endlich
verzweigt, kann jedoch unendiiche Pfade enthalten.
und die zweite
Beispiel: Das Logik-Programm P(., b ) [v/bl = P(&,b)
Übung 103: Man beschreibe alle Rechnungen, die unter dem Logik-
Programm
P(., y) :- P ( g l X).
oder in der PROLOG-Notation
bei Eingabe der Zielklausel ?- P(b,x ) möglich sind.
Übung 104: Welche Art von Programmklauseln kann man auffassen wie E-
kursive Prozeduren (im Sinne konventioneller Programmiersprachen)?
hat bei Eingabe der Zielklausel G = { 1 P ( v ,b ) } bzw. ?- P ( v , B) eine nicht
erfolgreiche Rechnung Beispiel: Gegeben sei folgendes Logik-Programm, das Teil eines größeren
Programms zum symbolischen Differenzieren sein könnte. Wir verwenden
dieses Mal die PROLOG-Notation. Außerdem bezeichnen irn folgenden s
und 1 (unkonventionellenveise)Konstanten; F,DF,G,DG,H Variablen, Diff
128 KAPITEL 3. LOGIK-PROGRAMMIERUNG
eine Rechnung des Logik-Programms F bei Eingabe Gsub' ist, dann gibt es
eine Rechnung (der gleichen Länge) von F bei Eingabe G der Form
also: bestimme die Ableitung von z * sin(x).Die folgende Rechnung ist er-
folgreich und liefert das gewünschte Resultat s t cos(xj + sin(x) (allerdings I 1 ) k. . ' k ( n I ~ ~ b t t j ,
{G,
in der Form z x (cos(x) * 1) + sin(xj * I). wobei für eine geeignete Substitution s gilt: subtsv,b = subUs.
(?- Dzfl(x * sin(x), H ) , [I) Mit den Resultaten von Kaprtel 2.6 folgt sofort, c k s F U {G} unerfüIIbar ist
( Y- D z f ( x , D F ) :Dxfl(sin(x):DG), s u b l ) genau dann, wenn es eine erfolgreiche Rechnung von F mit Eingabe G gibt.
( ?- D i (sin(z),
~ DG),s%blduliZ) Dies ist der logische Aspekt von Homklauselberechnungen. Was die ermittel-
( ?- D2#(x, D F ) , sub1 suhzsuhs) ten Rechenergebnisse betrifft, so können wir im Moment noch keine Aussage
sd1~sub2sub3suA~)
(0; über deren Korrektheit und über das Spektrum der berechneten Rechener-
gebnisse machen. Dieses regelt der folgende Satz, der als Verschirfung des
Hierbei ist Korrektheits- und Vollständigkeitssatzes für die SLD-Resolution verstanden
werden kann. Man erkennt an der Aussage des Satzes, dass die ermittelten
s?4bl = [ F J z [G/sin(x)][H/z
] DG * + s2n (X)r DF] Rechenergebnisse immer so allgemein wie möglich sind, also so viele Varia-
sub2 = [DFJI] blen wie möglich enthaiten.
sub3 = [ F I X[DG/
] cos(2) s DF]
sub4 = [DF/l] Satz {Clark)
Sei F ein Logik-Programm und G = ?- Al, . . . ,AI, eine Zielklausel.
Somit ergibt sich
1. (Korrektheitsaussage) Falls es eine erfolgreiche Rechnung von F bei
Eingabe G gibt, so ist jede Gnindinstanz des Rechenergebnisses (Al A
. . . A Ak)suh Folgerung von F.
Übung 105: Schreiben Sie ein Logik-Programm, das Formeln weitgehend 2. (Vollständigkeitsaussage) Falls jede Grundinstanz von (AI A . . . A
vereinfacht - durch Eliminieren von überflüssigen Summanden, die 0 sind, Ak).qubrFolgerung von F ist, so gibt es eine erfolgreiche Rechnung
und Faktoren, die 1 sind. (Dieses Programm konnte dann mit dem Differen- von F bei Eingabe G mit dem Rechenergebnis (Al A . . . A Ak) wb, so
zierprogramrn kombiniert werden). Das gesuchte Programm sollte folgendes dass für eine geeignete Substitution s gilt
leisten können:
3.2.HORNKLAUSELPROGR AMME 131
Beweis: 1. Wir fuhren den Beweis per Induktion über die Länge n der Rech- Nach Voraussetzung ist dann F U {Gf) unerfüllbar, und wegen der Voilstän-
nung. digkeit der SLD-ResoIution (siehe auch Übung 93) gibt es eine erfolgreiche
Falls TL = 0, so ist G = I7 und sub = [ I und es ist nichts zu zeigen. Rechnung von F der Form
Eine typische Rechnung der Länge T a > O sei nun (G', [])b
* * . k ( D , .wbl . . . s?~b„).
Da in G' kelne Variablen vorkommen, gilt G' = G'siib, . . .sub,. (D.h. die Er-
setzungen in subl . . . sub, beziehen sich nur auf die Variablen der Programm-
Hierbei sind sub,, . . . , sub, die berechneten allgemeinsten Unifikatoren. Die
klauseln.) Indem wir nun die Variablen X „ . . . , X„ textueIl für nl:. . . , n,
Zielklauseln G und G , haben die Form
wieder einsetzen, erhalten wir eine Rechnung der Form
und Hierbei sind s7ib',; . . . , sub: bis auf die textuelle Änderung identisch mit
GI= ?- (Al, . . .,P l i - r , C l ,. . . , Ci, Ai+, , . . . ,Ak)suhl, subl, . . . , sub,. Insbesondere gilt
wobei es eine Programmklausel in F der Form
Mit dem Lifting-Lemma (vgl. Ubung 106) kann diese Rechnung überführt
gibt, so dass ( B :A,) unifizierbar ist mittels allgemeinstem Uni fikator subl. werden in eine Rechnung (desselben Länge) der Form
Betrachten wir nun folgende Rechnung der Länge n - 1:
[I)
(G,, ... (U, . ~ ~ b. .2. sub,). Hierbei seien sub;, . . . , sah: die neuen, vom Lifting-Lemma gelieferten, all-
Nach Induktionsvoraussetzung ist jede Gnindinstanz von gemeinsten Unifikatoren. Nun gilt
für eine geeignete Substitution 3. Also folgt für die Substitution sub =
Folgerung von F. Insbesondere ist dann jede Gmndinstanz von
sub','. . . ssbn,dass
(Cl A - - A C E ) ~ u b. .1.S U ~ ,
+
Wir wo1len nun klären, was unter der Semantik eines Logik-Programms zu
ist jede Gmndinstanz von Aisulil . . . sub, und damit auch von verstehen ist. Wie bei konventionellen Programmiersprachen gibt es auch hier
verschiedene Ansätze. Zunächst geben wir die Definition einer infegwta-
tivea bzw. prozeditralen Semantik von Logik-Programmen. Dahinter steckt
Folgerung von F. die Vorstellung, dass durch ein Logik-Programm ein (paralleler, nichtdetcmi-
nistischer) Prozess dcfinicri wird. Das durch das Logik-Programm Bezeich-
2. Seien X I ,. . . ,X, die in Gsuhf vorkommenden Variablen und al. . . . um . nete, die Semantik, ist dann die Menge der potenziellen Rechenergebnisse
seien beliebige bisher nicht verwendete Konstanten. Sei dieses Prozesses. Aus Normierungsgründen beschränken wir uns im Folgen-
den auf Grundinstunzea der Rechenergebnisse (in Bezug auf das Herbrand-
Universum von F U { G } ) .
132 KAPITEL 3. LOGIK-PROGRAMMIERUNG
Sv, ( F , G) = Srnd
( F ,G ) .
bei gegebener Zielklausel
Beweis: (C) Sei H E S„„(F, G). Dann gibt es eine erfolgreiche Rechnung
von F der Form
ist. (G1[l)b ..' k P , s a b ) ,
so dass H eine Grundinstanz von (Al A + . A Ak)sub ist. Mit dem Satz von
+
Ein zweiter, ganz anderer Ansatz geht von der Vorstellung aus, dass die Clark (Teil 1) ergibt sich, dass H aus F folgt. Somit ist H E &&(F, G ) .
Semantik (bzw. die Denotation) eines Logik-Programms F und einer Ziel- ( 2 )Sei H E Smod(F, -
G).Dann ist H eine Grundinstanz von (Al A . A A k ) ,
klausel G = ?- A l , . . . , A h durch die Menge der Grundinstanzen H von die aus F folgt. Mit dem Satz von Clark (Teil 2) folgt, dass es eine Rechnung
( A l A - ..h A k ) gegeben ist, die aus F folgen. Dieser modelltheore~ischeAn- von F der Form
satz ähnelt der Zuordnung der Theorie Cons(F) zu einem gegebenen Axjo- (G1 [ l}b ' .. (0, $ab),
mensystem F (vgl. Kapitel 2-41. Die dem Axiomensystem F zugeordnete
Theorie Cons(Fj kann als (modelltheoretische) Semantik von F aufgefasst gibt, so dass H eine Instanz (und in hesem Fall Grundinstanz) von (Al A . - . A
werden. Ak)sub ist. Somit gilt H E S„„(F1G). R
der kleinste Firpunkt (in Bezug auf C) des Operators OpF ist.
Die Fixpunktsemaatik von F bei Eingabe G = 7- A l , . . . , Ak sei definiert als Dann ergibt dies drei mögliche SLD-Resolventen und damit neue Zielklau-
seln:
?- A, D,C.
(F,G } ={H I H ist eine Grundinstanz von ( A l S\ . - . A Ak)
Sfhpernkt ?- A, C.
und fGr alle Atomfomeln A in H gilt A E F p p }. ?- A, E , F, C.
wurde man bei den Verzweigungen für den Nichtdeteminismus 2. Art immer B und Aisub: (mittels s) unifizierbar. Also kann der zweite Resolutionsschritt
den linken Ast wählen und die anderen nicht berücksichtigen). Hieau zeigen ausgeführt werden. Hierbei sei sub', der allgemeinste Unifikator von B und
wir in einem Lemma, dass die Reihenfolge der Auswahl der Prozeduraufrufe Al.~ubl.
immer vertauscht werden kann, ohne das Rechenergebnis zu verändern.
Es verbleibt noch zu zeigen, dass sublsub2und sub', sub; (im Wesentlichen)
identisch sind. Hierzu zeigen wir, dass es Substitutionen s' und s" gibt mit
Vertauschungslemma ~ 7 ~ h ~= s usub~sub~s'
b~ und suhisubl, = sub1sub2s1'.
Gegeben seien zwei aufeinanderfolgende SLD-Resolutionsschritte Da sub; allgemeinster Unifikator von B und Aisub\ ist, und da Es = A,subi s
gilt, gibt es eine Substitution s' mit s = subis'. Also ist s?ih,subz = sub',s =
subisub2~'.
Als nkhstes beobachten wir, dass A,stibisubL = Bsubisubk gilt, und da
sub, ein allgemeinster Unifikator von A, und B ist, gibt es eine Substitu-
tion so mit sub\subk = sublso. Ferner gilt Ajsublso = A,szkb~sub~=
Dstlb: sub; = Dsublso = Dso. (Hierbei gilt das lewe Gleichheitszeichen,
da subl keine Variablen in D ersetzt). Dies bedeutet, dass so ein Unifikator
von D und A, r u h l ist. Da sub2 alIgemeinster Unifikator von D und A,subl
ist, gibt es eine Substitution s" mit so = sub2s".Zusammengesetzt ergibt dies
sub~5116~ =S T L ~= ~ S~ ~u b ~ s u bwas
~ szu~ zeigen
~, war.
wobei C für Cl,.. . , Ck und E für E,, . . . : Ei steht. Dann kann man die Rei-
henfolge der Literale, nach denen resolviert wird, vertauschen:
Definition
Eine Rechnung eines Logik-Programms heißt kanonisch,falls bei jedem Kon-
figurationsübergang nach dem ersten (also am weitesten links stehenden} Li-
teral der Zielklauseln resolviert wird. (Hierbei werden Klauseln also als Fol-
gen, nicht als Mengen, aufgefasst).
Satz
Sei (G,[ 1) . V ( 0 ,sub) eine erfolgrerche Rechnung des Logik-Pro-
gramms F. Dann gibt es eine erfolgreiche und kanonische Rechnung von F
bei Eingabe G d e r s e h n Lange und mit demselben Rechenergebnis.
Ferner ist sub, sub2 (bis auf eventuelle Viablenumbenennungen) ide~itisch
mit sub:subi. Beweis: Nehmen wir an, dass obige Rechnung bis zum 1:-ten Rechenschntt
kanonisch ist ( i 2 0). Wir zeigen nun, wie man diese Rechnung in eine Rech-
Beweis: Wir müssen zunächst zeigen, dass die SLD-Resolutionsschritte in nung mit gleichem Rechenergebnis überführen kann, die bis zum ( i 1)-ten +
vertauschter Reihenfolge möglich sind. Rechenschritt kanonisch ist.
u iDi ~J U ~=ZD s ~ b ~ s u bda
Es gilt zunächst A , ~ ~ h ~ s = ? ,sub, keine Variablen Angenommen, im i-ten Rechenschritt wird eine gewisse Konfiguration (H,s)
in D ersetzt. Deshalb sind A, und D unifizierbar, und der erste Resolutions- erreicht. Sei H =:I- A l , . . . , Ak. Dader (2 + 1)-te Rechenschritt nicht kano-
schritt kann ausgeführt werden. Es sei s?~bider allgemeinste Unifikator von nisch ist, wird nach einem Literal Al mit 1 > 1resolviert, wahrend nach dem
Aj und D. Da sublsub2Unifikator von A, und D ist, gibt es eine Substitution Literal Al (bzw. einer Instanz von A,) erst in einem späteren Rechenschtitt,
s mit subI~7~ba = sub: s. sagen wir 3 ( j > z + 1),resolviert wird. Wir wenden nun das Vertauschungs-
Weiterhin gilt Bs = Bsubis = Bsub,suh2 = Aisulilsub2 = A,aubis. (Das lemmaaufdiepaare vonRechenschritten j-1 u n d j , j - 2 u n d j - 1 , . . . ,i+l
erste Gleichheitszeichen gilt, da sub; keine VariabIen in B ersetzt). Somit sind und z f 2 an und erhalten auf diese Weise eine Rechnung, die im (i + 1)-ten
138 139
KAPITEL 3. LOGIK-PROGRAMMIER UiVG 3.3. AUS WERTUNGSSTRATEGIEN
Schritt nach dem am weitesten links stehenden Litera1 Al resolviert. (Es 1st und die Zielklausel> Q (X,C ) . Dann erhalten wir den folgenden Baum (wobei
nicht falsch, sich an dieser Stelle an Bubble-Sort zu erinnern). Damit haben zusätzlich die Kanten mit den Nummern der ausgewählten Pmgramnklauseln
+
wir eine bis zum (i 1)-ten Rechenschritt kanonische Rechnung mit dem beschriftet sind).
gIeichen Rechenergebnis erhalten. Sukzessives Anwenden dieses Verfahrens
macht die gesamte Rechnung kanonisch. M
Wir können uns irn Folgenden auf die Betrachtung von kanonischen Rechnun-
gen beschrinken. Diese Rechnungen sind nach wie vor nichtdeterministisch,
aber es verbleibt nur noch der Nichtdetermiriismus 1. Art. Dies erklärt nun irn /
7- Q(pi C), R ( 5 ,Y)
Nachhineln den Buchstaben S (für selectioa function), der in der Abkürzung
SLD vorkommt. Unter jeder Auswahlregel fur die Wahl des nächsten zu re-
fi Rechenergebni s:
solvierenden Literals in der Zielklausel (2.B. von links nach rechts) bleibt die
SLD-ResoIution vollständig.
Man beachte, dass kanonische Rechnungen ähnlich wie aichtdereminisrische
KelIerautoazaten operieren: Als KeIlerinhalt fassen wir hier die aktueI1e Ziel-
klausel ?- Al, Az, . . . , Ak auf, wobei Al das oberste Kellerelement ist. Dieses
oberste KelIereIernent wird bei jedem Rechenschritt nach Unifizieren mit dem
Prozedurkopf B einer Programmklausel B :- C,. . . . , C, durch C l : .. . ,C, I Rechenergebnis:
ersetzt. Gegenüber Kellerautomaten kommt jedoch hinzu, dass der hierbei er-
mittelte allgemeinste Unifikator sub dann auf den gesamten Kellerinhalt an- unendliche
Rechnung
gewandt wird, und die nächste Zielklauscl die Form
nicht-erfolgreiche
Rechnung
hat. Als weiterer Aspekt kommt hinzu, dass wir in der zweiten Komponente
der Konfiguration buchführen über die berechneten alIgemeinsten Unifikato- Dieser Baum enthält zwei erfolgreiche Rechnungen mrt den unterschiedli-
ren, um so das Rechenergebnis zu erhalten. chen Rechenergebnissen &(b. C) und @(C, C). Ferner kommt eine endliche,
Wir stellen die kanonischen Rechnungen eines Logik-Programms F bei Ein- jedoch nicht-erfolgreiche und nicht weiter fortsetzbare Rechnung vor. Falls in
gabe von G durch einen Baum dar, wobei die Wurzel des Baumes mit der jedem Rechenschritt mit der 1. Programmklausel resolviert wird, so erhalten
Startkonfiguration (G, [ I) beschriftet ist. Die Nachfolgerknoten eines mit wir eine unendliche Rechnung, wobe~in jedem Schntt die Zielklausel um
(G', sub) beschrifteten Knotens entsprechen dann genau den in einem kanoni- einen Prozeduraufmf länger wird.
schen Re~henschnttvon (G', ~ 2 1 6 )aus erreichbaren Konfigurationen. Der bes-
seren h r s i c h t wegen lassen wir jedoch bei der Beschriftung clieser Bäume Übung 112: Da Klauseln in unserer jetzigen Betrachtungsweise als Folgen
oft die zweite Komponente der Konfigurationen weg, in denen das Rcchener- von Literalen und nicht mehr als Mengen von Literalen aufgefasst werden,
gebnis berechnet wird. kann es sogar bei Logik-Programmen, die nur aussage~tlogiscl1eKlauseln (al-
so keine Variablen) enthalten, zu unendlichen Rechnungen kommen. Man fin-
Beispiel: Betrachten wir das Logik-Programm de hierfür ein Beispiel !
Wie im Fa11 des Nichtdeterminismus 2. Art kann man sicherlich nicht vor- und bei depth-first Auswertung in der Reihenfolge
gehen und Teile des Baumes unberücksichtigt lassen, wie die obigen Bei-
spiele zeigen. Die jeweilige Auswahl der niichsten Programmklausel, wie sie
im Nichtdeterminisrnus 1. AL?vorkommt, ist sehr kritisch und entscheidet durchlaufen.
darüber, ob eine erfolgreiche oder nicht-erfolgreiche (evtl. unendliche) Rech-
Der folgende Algorithmus realisiert die depth-first (bücktracking) Strategie.
nung zu Slande kommt. Im Fall einer erfolgreichen Rechnung entscheidet
die Auswahl der ProgrammkFauseln auch noch iiber das erhaltene Rechener-
gebnis. Da es (anscheinend) keine Möglichkeit gibt, den Nichtdetern~inisrnus
1. Art wie den der 2. Art zu eliminieren, muss eine deterministische Aus-
wertungsstrategie systematisch den gesamten Berechnungsbaum eines Logik- Eingabe: Logik-Programm F = (K1,K2,. . . , I<*), wobei
Programms (bei gegebener Eingabe) durchlaufen - zumindest bis eine erfolg- I< = Bi :- C,,J,. . . , C,,„ und Zielklausel G = ?- A i , . . . , An.
reiche Rechnung gefunden wird. Kienu gibt es zwei gnindsiitzliche Möglich-
keiten: die breadth-jrst und die depth-first Strategie. Das Hauptprogtamm besteht aus
Bei der breadth-first Strategie (Breitensuche) werden zunächst alle Kno-
success := false;
+
ten der Tiefe t besucht, bevor die Knoten der Tiefe t 1 besucht werden
auswerte(G, [ ] );
(t = 0 , 1 , 2 , .. .). Es ist klar, dass hierbei jede erfolgreiche Rechnung nach
if success then write('ja') else write('nein');
endlich vielen Suchschritten gefunden wird. Mit anderen Worten, die breadth-
firnt Auswemingsstrategie ist vollstindig. Diese Vollständigkeit wird jedoch wobei die rekursive Prozedur 'auswerte' folgendermaßen arbeitet.
erkauft durch einen großen Aufwand an Speicherplatz und Rechenzeit: Um
bis zu den Knoten auf der Tiefe t des Baumes vorzudringen, benötigt die procedure auswerte(G : Zieiklausel; sub : Substitution);
breadth-first Strategie exponentiell (in t )viele Rechenschritte (vorausgesetzt, var z : integer;
der Berechnungsbaum besteht nicht nur aus einem einzigen Pfad). begin
Bei (Standard-) Interpretern für die Programmiersprache PROLOG wird da- if G = U then
gegen die depth-first Auswertungsstrategie (Tiefensuche) eingesetzt. Hierbei begin
werden, von der Wurzel des Baumes ausgehend, die Teilbäume in einer fe- H := (Al A . . " A Ak)suEi;
sten Reihenfolge (von links nach rechts) rekursiv durchsucht. Es wird also write('Ergebnis: ',H);
im Unterschied zur Breitensuche zunächst in die Tiefe des Baumes gegangen. success := true
Bei VorfEndeneiner nicht-erfolgreichen Rechnung, die nicht weiter fortgesetzt end
werden kann, kehrt die Suche an den Elternknoten zurück (backtrachng). hbn else {G habe h e Form G = ?- Di, . . . :Dk)
dort aus wird versucht, mit einer anderen Folgekonfiguration fortzufahren. begin
L! := 0;
Sn wird 2.B. der Baum
while (i < n) and not success d o
begin
z:=if 1;
if {D,. B,) ist unifizierbar mittels allgemeinstem
Unifikator s (wobei h e Variablen in B, evtl. zu-
vor umbenannt wurden) then
auswerte(?- (C,,i,... , Cx,n,,Da,. . .:Dk)s, suks)
bei der breadth-first Auswertung in der Reihenfolge end
end
end
144 KAPITEL 3. LOGIK-PROGRAMMIERI%NG 3.4. PROLOG 145
dass vom System gewisse Prädikate (wie read, write, . .. ) bereitgestellt wer- Ein Merkmal von PROLOG ist, nicht besonders zwischen Funktionen und
den, die vom Benutzer nicht rnodifizieri werden können, und die vom Iogi- Priidikaten zu unterscheiden; mehr noch, das (logische) Symbol : - , das
schen Gesichtspunkt betrachtet keine Bedeutung haben. SIe werden bei Bear- fiir den Implikationspfeil steht, wird aufgefasst wie ein zweistelliges Prädikat
beitung durch den PROLOG Auswertungsmechanismus einfach übergangen, oder auch eine zweistellige Funktion (geschrieben in Infixnotation), das als
erzeugen jedoch (erwünschte) Seiteneflekte, wie 2.13. das Schreiben auf den System-Prädikat/Funktioneinzustufen ist und eine besondere Auswertung er-
Bildschirm oder in eine Datei. fordert. So werden dann konsequenterweise auch Klauseln wie Terme aufge-
Dies setzt aber auch voraus, dass dem Programmierer die Abfolge der Aus- fasst und können vom Programm aus modifiziert werden. Es ist die Möglich-
wertung seines PROLOG-Programms bewusst ist. Eine Zielklausel wie keit vorgesehen, dass das PROLOG-Programm selbst neue Klauseln generiert
und an seine eigene "Datenbank" anfilgt - oder umgekehrt - Klauseln wieder
?- read ( X ) ,compute(X,Y ) ,write(Y) streicht.
Komplexere Datenstmkturen können in PROLOG durch die Terme bzw. deren
kann sinnvoll nur von Iinks nach rechts ausgewertet werden - im Gegensatz
Art der Verschachtelung dargestellt werden. So soll etwa
zu den theoretischen Betrachtungen des letzten Abschnitts, wo gezeigt wurde,
dass eine derartige Klausel (wenn keine Seiteneffekte vorhanden sind) genau-
so gut von rechts nach Iinks ausgewertet werden kann.
Bei anderen Prädikaten, die das PROLOG-System bereitstellt, werden ab- die Liste bestehend aus den 3 Elementen a, b und e darstellen. Hierbei be-
weichend vom Unifikationsalgorithmus Varjableninstantiierungen enwun- zeichnet die Konstante nil die leere Liste. Das Funktionssymbol cons ist der
gen. Ein Beispiel ist das Prädikat ix. Wenn das PROLOG-System z.B. auf Listenkonstmkior. In dem Term c o n s ( ~y), bezeichnet s das erste Element der
i s ( X ,Y * 5 ) (oder in Infixnotation: X is Y * 5) trifft und Y bereits mit der Liste und y den Rest der Liste. Es ist bequemer, eine atikücürzende Schreibweise
Konstanten 7 instantiiert ist, so wird X mit 35 instantiiert. Hierdurch können zu verwenden. So bezeichnet
dann arithmetische Rechnungen in PROLOG realrsiert werden.
Übung 114: Berechnen Sie mit Hilfe des is-Prädikats die Fakultätsfunktion.
und [ I steht für die leere Liste nil.
Durch dieses Konzept geht allerdings die Investibilität von Logik-Pro-
grammen verloren. Obiges Programm für die Fibonacci-Funktion kann sinn- Beispiel: [ [ U , [b, C]] 1 [d, e]] ist eine abkürzende Bezeichnung für
voll nur so aufgerufen werden, indem der erste Parameter als Eingabeparame-
ter und der zweite als Ausgabeparameter aufgefasst wird.
Ein weiterer Aspekt ist, dass Funktionen und Pradikate entweder in der Das folgende Diagramm macht die Struktur dieses Terms deutlich, wobei je-
Prafrxnotation (z.B. +(5,7)) oder in der Infixnotation (5 + 7) geschrieben der Punkt für eine Anwendung von cons steht.
werden können.
KAPITEL 3. LOGIK-PROGR AMMIERUNG 3.4. PROLOG
permut([j, [I).
] ,) :-perrnut(Y, W). anser-t(X,W , Z ) .
p c r m u t ( [ X J Y2
insed(A,B. [AIB]).
insert(A,[ B ] C ][EID]), :- inse.rt(A,C , D).
Die häufigste Operation auf Listen ist deren Verknüpfung. Folgendes Logik-
Programm beschreibt die Verknüpfung (Konkatenation) zweier Listen.
So führt 2.B. die Zielkiausel
w e n d ( [ ] L,
, L).
append([X/Lt], L2, [XIL3]E - w ~ e n d ( L Lz,
l , Ls). ?- p e m u t ([viele,kriche,verderben,den,brei]; 2)
Hierbei sind X, L, L,, L?, LS Variablen und uppend(L1. LLlLB) drückt aus, auf die Resultate
dass L3 die Konkatenation der Listen L, und L2 ist.
Z = [viele,Eche,verderben, den,brei]
Übung 115: Man gebe eine erfolgreiche Rechnung obigen Programms bei Z = [köche,viele,verderben, den,brei]
Eingabe der Ziel klausel Z = [köche,verderben,vieie, den,brei]
Z = [köcite,verderben,den,vieie,brei]
Übung 116: Man gebe ein PROLOG-Programm zum Umdrehen einer Liste sort (Ll, .L2) :- pernrtit ( L I ,L2),
ord(L~).
an. So soll wverse(L1,L2) genau dann gelten, wenn L2 die gespiegelte Ver- 01.4[1).
sion der Liste L, ist. o4lXl).
Man formuliere ein weiteres PROLOG-Programm, so dass L,und jede Teil- or.d(IXl[YlZ]]) :-X 5 Y, o~.d([Y1Z]).
liste von LI gespiegelt wird.
Schreiben sie ein Sortierprogrmm, das Quicksort realisiert.
Hierbei bezeichnet load das Laden eines Elements auf einen Keller, und nsul depth-first Auswertungsstrategie. Ein Teil des Suchbaums wird durch den cut
bzw. udd verarbeiten die obersten zwei Kellerelemente und legen das Resultat abgeschnitten, und dadurch können Teilbäume, die keine erfolgreichen Rech-
wieder auf den Keller. Das Kommando sture legt das oberste Kellerelement nungen oder. schlimmer noch, unendliche Berechnungspfade enthalten, bei
jm Speicher ab. der Lösungssuche ausgelassen werden. Eine weniger vorteilhafte Wirkung
des cut ist allerdings, dass genauso gut Teilbäume, d ~ eerfolgreiche Rech-
comioibe(X := Y,2) :- compile(Y, W ) , nungen enthalten, abgeschnitten werden können.
X ] ] ,2 ) .
append (W,[[stop-e, Hier gehen nun die Meinungen über den cut auseinander. Die "Cut-Befürwor-
ter" wollen gerade solche Effekte wie das bewusste Uberspringen von (an
comptEe(X * Y , 2) :- compile(X,U), sich vorhandenen) Lösungen programmieriechniscti einsetzen (vgl. die nach-
compile (Y,V ) , folgende Diskussion über die Negation).
apgiend (U, V,W ) , Die andere Auffassung ist, dass der cut der Idealvorstellung der Logik-
append (!Vl [muIt],2). Programmierung entgegenläuft, wo der Programmierer eigentlich nur das zu
lösende Problem spezifizieren soll, nicht jedoch - oder nur indirekt - wie
compile(X + Y,2) :- comprle(X, U), dieses zu lösen ist. Ein solches Konzept wie der cut gehort sicherlich in die
eompile(Y,V ) , wie-Kategorie.
append (U,V,W ) , Was bewirkt nun der cut im Einzelnen? Sobald eine cut-Atomformel, wie 2.3.
acppend (W.[add], 2).
in folgender Zielklausel
compile(X, [[load,X]]) :- atomic(X)
zum ersten Mal abgearbeitet wird, führt dies unmittelbar zum Erfolg (als
Übung 119: Definieren Sie sich formal die Syntax einer Programmiersprache ob eine Tatsachenklausel, bestehend aus "!", im Logik-Progrümm vorhanden
ASCA (eine geeignet einfache Teilmenge von PASCAL) und schreiben Sie wäre). Damit ist die nächste abzuarbeitende ZielMause1
dann einen Compiler für ASCA-Programme in PROLOG.
(a} Konstruieren Sie den SLD-Suchbaum für die Zielklausel '.L spaj.
Was würde PROLOG auf diese Frage antworten?
(b) Stellen Sie die Klauseln des Programms so um, dass die Anfrage
nicht
besuchte T spaJ in endlicher Zeit beantwortet werden kann.
Tei lbäume
(C) Fügen Sie einen cut in obiges Programm ein, so dass der von
des PROLOG durchlaufene Teil des Suchbaums endlich, aber so groR
wie möglich ist.
(d) Beschreiben Sie den Effekt, den das Einfügen eines cut an je-
der der drei möglichen Positionen in der ersten Programmklausel
hervorruft.
keine erfolgreiche
Rechnung hier vorhanden Wir fassen nun die möglichen und typischen Einsatzmoglichkeiten des cut
zusammen.
1. Nach Finden einer ersten Läsung erlaubt der Einsatz des cut jede wei-
Übung 121: Modifizieren Sie den PROLOG-AuswertungsaIgorithmusaus
tere Lösungssuche zu verbieten - entweder weil der Programmierer an
Abschnitt 3.2 so, dass er den cut korrekt ausführt.
keiner anderen als der zuerst gefundenen Lösung interessiert ist, oder
weil aus dem Problemkontext bekannt ist, dass keine weiteren Lösun-
Übung 122: Das Programmstück gen (oder höchstens nur noch unendliche Berechnungspfade) exrstic-
ren. Bei dem Additionsprogramm aus Abschnitt 3.2 kann dusch Einsatz
(1 :-/~,!~c. des cut jede weitere Rekursion vermieden werden, sobald der Suchpro-
n :- d. zess auf die Klausel, die den Rekursionsanfang symbolisiert, stößt:
wird in konkreten PROLOG-Programmen verwendet, um das aus konventio-
nellen Programmiersprachen bekannte if-then-else,irn Sinne von
a :- if b then c else d.
3.4. PROLOG 153
2. Der cut erIaubt Konsiruktionen, die dem aus den herkömmli- oder 1 A E Cons(F).Wenn also eine Aussage -4 aus F nicht folgt, so gilt
chen Programmiersprachen bekannten if-then-else entsprechen (siehe A auch nicht. Man spricht in diesem Zusammenhang von closed world as-
Übung 122). Ähnliches gilt auch für die Negation (vgl. die nachfolgen- surnption. Da A aus F genau dann nicht folgt, wenn F A 1'4 erfullbar ist, also
de Diskussion). genau dann, wenn die leere Klausel per SLD-Resolution aus F U ((TA)}
nicht herleitbar ist, spricht man auch von negution by fuilure.
3. Der cut erlaubt die Steigerung der Effizienz von Programmen, indem
Es wäre wünschenswert, zumindest dieses 'negatien by failure' in den
Teilbäume bei der Losungssuche übersprungen werden können, von de-
PROLOG-Auswertungsmechanismus aufzunehmen; also wenn nicht beweis-
nen aus dem PToblemkontext klar ist, dass sie keine Lösungen enthalten
bar ist, dass A aus F folgt, so nimm an, dass IA aus F folgt. Aber auch dies
kfinnen.
lässt sich (aus prinzipiellen Grirnden) nicht ganz realisieren: Falts für jedes A
4. Der cut kann - bei überlegtem Gebrauch - der logischen Unvoll-
nach endlicher Zeit entschieden werden könnte, ob A aus F folgt oder nicht,
stiindigkeit der dcpth-first Auswertungsstrategie entgegenwirken, in- so würde dies die Entscheidbarkeit der Prädikatenlogik nach sich ziehen, und
dem er es erlaubt, Tei lbäume mit unendlichen Berechnungspfaden bei das ist ein Widerspmch zu den Resultaten von Abschnitt 2.3. (Dies gilt auch,
der Lösungssuche zu überspringen. wenn man sich auf HornformeIn beschränkt!)
Die nächstschwiichere Form der Negation ist aegation hy jnite failure. Dies
bedeutet, dass nur von solchen Aussagen A angenommen wird, dass TA aus
Aus verschiedenen zu Beginn von Abschitt 3.2 diskutierten Gründen sind die F folgt, bei denen der (nicht-erfolgreiche) SLD-Berechnungsbaurn bei Ein-
Klauseln in PROLOG auf die Homfom eingeschränkt. Diese Beschränkung gabe A endlich ist. Diese Form der Negation ist nun bei PROLOG realisiert:
ermöglichte erst die prozedurale Interpretation von Logik-Programmen und Die Eingabe der Zielklausel ?- not (p) veranIasst den PROLOG-Interpreter,
die recht weit entwickelte Theorie, wre sie insoweit dargestellt wurde. Nun nach erfolgreichen Rechnungen der Form
kann es jedoch Fälle geben, wo Hornformeln zur Problem-Beschreibung nicht
mehr ausreichend bzw. nicht adäquat sind. Diese "Ausdmcksschwäche" von
Hornfomeln kann in manchen Koblemkontexten ein großes Hindernis dar-
zu suchen. Nur wenn der Suchbaum hierzu endlich ist und keine erfolgreiche
stellen. Hierbei spielt die Negation eine besondere Rolle. Man denke daran, Rechnung enthiilt, so gibt der PROLOG-Interpreter schlreElich 'ja' aus. Falls
dass die Negation einer Hornformel im allgemeinen zu keiner Aomfonnel eine erfolgreiche Rechnung gefunden wird, wird 'nein' ausgegeben. Diese
mehr äquivalent ist. In manchem Kontext mag es wichtig sein zu erfahren, ob
Form der Negation birgt die Gefahr in sich, dass der Suchprozess in einen
ein negatives Literal (z.B. TA) aus einem Logik-Programm folgt. Dies würde unendlichen Berechnungspfad gerät.
dann formal betrachtet einer Zielklausel der Form ?- T A bzw. ?- not(.A)
entsprechen. Die logische Antwort auf eine derart gestellte Frage ist e r s t a k Diese Form des 'negation by finite failureVässt sich auch in PROLOG seIbst
lichenveise ganz einfach, nämlich immer "nein". einfach realisieren - und zwar durch eine "missbräuchliche" Verwendung des
cut (es werden hier existierende Lösungen durch den cut abgeschnitten).
Übung 124: Man zeige, dass es kein Hornklauselprogramm F gibt und kein not (P):- P,!)fall.
negatives Literal, 2.B. YA, so dass TA aus F folgt. M.a.W., aus Hornklausel- not (P).
Programmen k ~ n n e nkeine negativen Schlüsse gezogen werden.
Hierbei ist fail ein (Standard-) Prädikat, das nie zu erfolgreichen Rechnungen
Dieser erste Versuch ist also fehlgeschlagen. Anstelle die Frage zu stellen, ob führt (d.h. es ist einfach keine Programmkiausel mit dem Prozedurkopf fail
die Negation von A aus F folgt, fragen wir nun danach, ob das Literal A aus vorhanden). Man beachte, dass die Variable P hier unkonventionellerweise
F nicht folgt. Dieses macht natürlich mehr Sinn, ist jedoch nicht dasselbe wie ein Platzhalter für eine Atomformel ist.
die Negation im logischen Sinn. Diese beiden Begriffe gleichzusetzen bedeu-
tet nichts anderes als die Vollständigkeit des Logik-Programmes F zu postu- Übung 125: Vollziehen sie den Ablauf des obigen Programms nach bei Ein-
lieren, d.h. für alle Aussagen A anzunehmen, dass entweder A E Coras(F) gabe der Zielklausel ?- not(not(not(a))). Führen Sie dies unter der An-
154 KAPlTEL 3. LOGM-PROGRAMMIER UNG
nahme durch, dass n als Tatsachenklausel vorkommt, und dann, dass a nicht
vorkommt.
Vollziehen Sie nach, was PROLOG auf jede der folgenden Fragen antwortet: 1. "Zu jeder Mahlzeit trinke ich Bier und esse nie gemeinsam Fisch und Eis-
creme''.
(4 ?- PP).
(b) ?- not(p(b)).
2. ( ( AH B ) # C )
(C) ?-4td.
(d) ?- not (q(a)).
3. Sei A eine beliebige, zu F l , . . . , Fk und G passende Belegung.
(e) ?- 4 ( X ) ,n o t ( p ( X )1.
(1 + 2) Falls A((A~=, F,))= 0, so ist d(((l\f=, F,) + G)) = 1 und wir
(f) ?- n o f ( p I X ) ) q, ( W . sind fertig. Sei also A((A;=, F,)) = 1 angenommen. Dann ist A Modell für
{ F l ,.. . , F k ) .Nach Voraussetzung ist dann A(G) = 1, also A(((A~=,F,) +
Ein weiteres Problem mit der Negation besteht darin, dass bei einer Zielklau- G ) )= 1.
sel der Form ( 2 t 3) FaIts A((& F, A 1G)) = 1, so ist A ( ( A ~F,)) = ~ = 1 und
A(1G) = 1, also A(G) = 0. Dies ergibt A(((A:=,F,) + G)) = 0, und
steht in Widerspruch zu 2.
(3 + 1) Sei d Modell von { F l , .. . , F k ) , d.h. A((r\:=,F,)) = 1. Nach
in dem Term (bzw. der Atomformel) t keine zum Zeitpunkt der Ausweming Voraussetzung gilt A(((A~=, F?)r\ 1G)) = 0, also muss A(7G) = 0 bzw.
uninstantiierten Variablen vorkommen sollten. Dies kann zu einer inkorrekten A(G) = 1 sein.
Auswertung fuhren. So führt etwa das Programm
4. Sei A = "ich laufe lOOm unter 10,O Sekunden" und sei B = "ich werde
zur Olympiade zugelassen". (-4 + B) ist nicht äquivalent zu ( T A+ T B ) .
bei der Zielldausel
5. Die erste Behauptung folgt unmittelbar aus der Definition der ErfülIbürkeit;
?- n o t ( p ( X ) ) , q ( X , X ) - die zweite Behauptung gilt nicht.
nicht zur gewünschten Antwort. Anders sieht es mit der ZieIklausel
?- q ( X ,X ) , n o t ( p ( X ) ) .
aus, die auf die Antwort X = b führt. 7. M = {A; B, -l(A A B ) }
In diesem Abschnitt sollte klar geworden sein, dass PROLOG eine Möglich-
keit ist, Ideen der bgik-Programmierung irn Rahmen ciner konkret einsetz- 8. M ist erfüllbar. Eine erfüllende Belegung ist z.B. A : {AI: Az, . . .) +
baren Programmiersprache zu realisieren. Es sollte jedoch gesehen werden, {O,l}mit
dass auch andere Konzepte denkbar sind, und dass die Forschungen in dieser 1, falls i ungerade
Richtung durchaus noch nicht abgeschlossen sind. 0, falls i gerade
12. F enthalte nur Atomformein der Menge und G enthalte nur Atom-
formeIn der Menge M2, ;zlI1r l M, = 0. Angenommen, F ist erfüllbar und
G ist keine Tautologie. Dann gibt es Belegungen Al : iVl + {0,1) und
Az : M2 -+ ( 0 , 1 } mit A l ( F ) = 1 und A2(G)= 0. Dann ist A = AI U Az
eine passende Belegung für ( F + G) und es gilt A({F + G)) = 0. Also ist
(F + G) keine Tautologie. Widerspruch.
13. Induktion über die Anzahl n der Atomformeln, die in F, aber nicht in G,
vorkommen.
Falls n = 0, so w a l e H = F.
Sei nun n > 0 und sei A eine Atomfomel, die in F, aber nicht in G,
vorkommt. Wir eliminieren A aus F, indem wir jedes Vorkommen von A
in F durch 0 (bzw. durch 1) ersetzen (und elementare Vereinfachungen
durchführen, z.B.(0 V B) B). Die resultierende Formel helße F. (bzw.
Fl).Es muss nun (Fo + G) und (Fl + G) gelten. Somit existie-
ren nach Induktionsvoraussetzung Formeln Ho und Hl mit (Fo + H o ) ,
A B C ( A +t ( B H C ) ) (Ho + G ) , t= (Fl + Hl), ( H 1 + G). Die Formel H = (Ho v H l )
0 0 0 0 leistet dann das Gewiinschte.
Alternativ zu dem eben gegebenen Beweis kännte man auch direkt eine Wahr-
heitstafel für H konstruieren. Seien Al; .. . , Ak die gemeinsamen Atomfor-
meln von F und G. Eine solche Wahrheitstafel sei im folgenden skizziert:
10. (a) Sei A eine passende Belegung. Dann gilt A((F + G)) = 1 und
A ( F ) = 1 nach Voraussetzung. Also muss auch A(G) = 1 sein. Da A belie-
big gewahlt war, ist G eine gültige Formel.
(b) Gegenbei spiel: F = A und G = ( B A 1B). Hierbei tragen wir in der Spalte für F bzw. G eine 0 bzw. 1 ein, falls bei
(C) Sei A eine Belegung mit A(F) = I. Für diese Belegung muss nach Vor- der betrachteten Belegung der Atome A l , . . . ,Ak - und jeder Belegung der
aussetzung AI (F + G)) = 1 gelten. Somit ist auch A(G) = 1. Also ist G restIichen Atome - F (bzw. G) den Wert 0 (bzw. 1) erhält. Wir tragen ? ein,
erfüllbar. falls die Formel F bzw. G bei manchen Belegungen der restlichen Atomfor-
mein den Wert 0 und bei anderen den Wert 1 erhält. Da nach Voraussetzung
11. Wir führen die folgenden Abkürzungen ein: G = "gutes Gehör haben", + (F -t G) gilt, sind nur die oben angegebenen Kombinationen für F und G
R = "richtig singen können", M = "wahrhafter Mus~kersein", Z = "seine mögljch. (Z.B. ist die Kombination ? ? nicht möglich, da es dann eine Bele-
Zuhörerschaft begeistern können" und S = "eine Sinfonie schreiben können". gung A gäbe mit A ( F } = 1 und A(G) = 0). Für jede dieser Möglichkeiten ist
Dann können die angegebenen Aussagen in folgende Formeln umgesetzt wer- in obiger Tabelle auch gleich angegeben, wie H definiert werden muss (wobei
den: (G + R),( M + Z),(2 + G ) und (S + M). Ferner ist in der Frage- an einer Stelle beide Alternativen 0 oder 1 möglich sind), so dass (F 4 H)
stellung die Angabe des Faktums S enthalten. Eheraus ergibt sich dann, dass und (H -i G) gilt.
M, 2, G, und R gelten müssen.
14. Falls F E G gilt, so Iassen sich die beiden Formein allein durch die irn 1I.
Satz angegebenen Äquivalenzumfomungen ineinander überführen (da beide (('4 V -(B A A ) ) A (C V (DV C ) ) )
Formeln in dieselbe Normalform umgeformt werden können). Alle in dem E ( ( AV ( 1 D V -Al) /\ (C V (DV C))) deMorgan
Satz angegebenen Umformungen treten paarweise auf, so dass in der jeweils E ( ( AV ( T AV TB)) A (C V (DV C)))Kommut.
zweiten Version nur "An und "V" vertauscht auftreten. Dies bedeutet, dass E ( ( ( AV T A ) V TB) r\ (C V (D C))) Assoz.
die oben angesprochene Äquivalenzumformungskette von F nach G in eine ( ( AV 1 A ) n (C V (DY C))) Taut.
entsprechende, duale, von F' nach G' umgeformt werden kann. E (C V ( D v C)) Taut.
= (C V (C vD)) Komrnut.
15. Man kann jede Teilfomel von F der Form (G V H ) und (G A H) durch E ((CV C) V D) Assoz.
eine äquivalente Formel, die nur die Operatoren 1 und + enthält, ersetzen ( C V D) Edern.
(und dann das Ersetzbarkeitstheorem verwenden), und zwar wie folgt:
18. (a) (((Fiebrig V Hustet) A Erreichen) + Rufen)
(b) (Erreichen +J(Fiebrig --+ Rufen)) A (Erreichen + (Hustet + Rufen))
(V:="=,F,)) (VyLlG,)) -
schrjtt werden der Reihe nach dic Distri butivität, die Induktionsvorausset-
zung und die obige Behauptung verwendet: FF,)A
((F1A (V,"=, G J ) )V ((V:="=,*)
G,)) = (I F1 V
(V,", GJ)))
((Fr A (VyLIGJ)) V (VF2(VyLl(& A G , ) } ) ) E ((V;tdFi G j ) ) V
Iv,"=,(Vy=l(F, GJj))) = IV,"„CV,"=l(F, f, G,))).
Die Teilfomeln in eckigen Klammern können nun separat in äquivalente
KNF umgefomt werden. Hierbei entstehen aus einer Teilformel in eckigen
Klammern im Allgemeinen - In Abhängigkeit von op - 3 bzw. 4 Klauseln.
21. Irn ersten Schritt werden die Atome C, B und G markiert. Daraufhin
werden irn zweiten Schritt -4 und D markiert. Dies führt dann irn nächsten
Schleifendurchlauf auf die Ausgabe “unerfüllbar", denn es wird die Klausel 27. Die gesuchte Folge 7 r i 1 , wq,. . . kann in Stufen wie folgt konstruiert wer-
( A I\ ß A D + 0) vorgefunden, wobei A, B, D markiert sind. den:
Stufe O: 7rio := E ; (das leere Wort)
22. Es gibt - bis auf Aquivalenz - nur endlich viele Homformeln, die aus Stufe k + l :
den Atomen A und B aufgebaut sind; diese sind alle inäquivalent zur Formel If wkO ist Anfangsstück von unendlich
(A V B). vielen EIementen aus L
t h e n , u ~ k +:=
~ wkO
23. Die AtomfomeI A ( S ) stehe für die Aussage "der Stoff S ist herstell- else w k + := ~ wt 1 ;
bar oder verfügbar". Die chemischen Gleichungen können dann in folgende
Hornfomel umgeschrieben werden: F = ( A ( M g 0 )A A(H2)+ i l ( M g ) )A
(A(MgO)AA(H,) 4 A(I-lzo)) ( A ( C )/\A(O2)+ - 4 ( c & ) )(A(H20)A ~ 28. { A , C , E ) , { 7 B 1 1 D , E ) ,{ B , C , + , E } , { A , B ) , { A 1 C , 7 D , E } ,
A ( C 0 2 )+ A(H2C0,))A A ( M g 0 ) A A(H2}A A ( 0 , ) A A ( C ) .Die Aufgabe (-C, 7D.E ) , { B :4,E ) , { A ,E ) , {.;L, 7 D ;E } , (.4, B , l D , E } , {TD, E}.
verlangt nun zu zeigen, dass A ( H 2 C 0 3 )eine Folgerung von F ist. Wir fügen
deshalb -A(H2C03)zu F hinzu (vgl. Ubung 31, und stellen durch Anwenden 29. Nein.
des Markieningsalgorithnius' fest, dass diese Formel unerfüllbar ist.
M.h ' e s O ( ~=) F ; R e s l ( ~=) Res0(F)U { { A . C } ,{ l B , C ) ,{ A , l B ,B):
24. Da alle sl, auf A723undefiniert sind, tritt in der Konstruktion in Stufe
723 der else-Fall ein. Daraus ergibt sich, dass d(A7„) = 0 gesetzt wird. (Die (A,C,-C}, { A , l B ) ,{ B ) , ( i A , B ) ,( T A ) ] ; R e s 2 ( ~ = ) Resl(F) U
Konstruktion wäre jedoch ebenso korrekt, falls in diesem Fall der then-Teil { { B , T B , C ) , {-4,7A,C), { C ) , ( A , B , c } , ( C : l C ) , {-4,C}, ( A , B ) ,
ausgeführt und A(A72.3)= 1gesetzt würde). { A ,B , TC), { A l , { T B ) ,( A l -C)}.
31. Sei F eine Klauselrnenge mit den AtomfomeIn A l , . . . , An. Dann können
25. Wenn M erfüllbar ist, existiert eine Belegung A mit A(F,) = 1 für z = h~chstens4" viele verschiedene Klauseln in Res* ( F ) vorkommen. (Jede der
1,2, . . ..Damit gilt sogar für jedes n,, dass ~I(l\r="=,~)= 1, insbesondere dass
n Atomfomeln kann in einer KIausel: positiv vorkommen, negativ vorkom-
F*)erfüllbar ist. men, positiv und negativ vorkommen, überhaupt nicht vorkommen. Dies sind
Sei umgekehrt angenommen, dass für unendlich viele n erfüllbar ist. 4 Möglichkeiten). In jedem Schritt von ResYF) nach ResEt1(F)könnte ge-
Sei Mn = { Fi,, F„, . . F„} eine beliebige endliche Teilmenge von M. Dann rade nur eine weitere Klausel hinzu kommen.Als (grobe) obere Schranke für
gibt es nach Voraussetzung ein n > max{il, a z , . . . ,xk}, so dass (Ar!, FR) k erhalten wir deshalb: k 5 4".
erfüllbar ist. Also ist auch Mo erfüllbar. Da Mo beliebig gewählt war, ist jede
endliche Teilmenge von M erfüllbar. Mit dem Endlichkeitssatz folgt, dass 32. Dasselbe Argument wie in Übung 3 1 zeigt, dass IRes" ( F )I 5 4".
damit auch M erfüllbar ist.
33. -4 A B A C ist eine Folgerung von F gdw. G := F U { { T A ,-B, 1C))
26. Falls M endlich axiomatisierbar ist, so gibt es ein endliches Axiomensy- unerfüIlbar ist. Dieses zeigt der folgende Resolutionsbeweis:
stem Mo für M. In Mo können nur endlich viele verschiedene Atomfomeln,
z.B. Al, . . . ,Al vorkommen. Da nach Voraussetzung (Fw1+ F,) und
(F, t F,+1)fiir alle n gilt, muss die Menge { F l , F2,F3, . . .) unendlich
viele Atomformeln enthalten. Insbesondere muss für ein k > E gelten: es gibt
Belegungen A und Ar,die sich nur in Ak unterscheiden, so dass A Modell für
M ist, A' dagegen nicht. Da Ak in Mo nicht vorkommt, sind entweder bei-
de Belegungen Modell für Mo oder beide sind es nicht. Also kann Mo kein
Axiomensystem für M sein.
&. Die Homformelbedingung garantiert nun, dass weder in K1 noch in K2 Terme:
zwei positive Literale vorkommen können, und damit ist gewährleistet, dass
der eben drskutierte Fall nicht eintreten kann. Es gilt also K"' = K7.
Die folgenden Vorkommen von Variablen sind frei (dic anderen sind somit
39. Falls F keine positive Klause1 enthält, so kommt in jeder Klausel minde-
gebunden):
stens ein negatives Litera1 vor. Indem wir nun alle Atomfonneln mit 0 belegen
(und dadurch diese negativen Literale den Wert 1 erhalten), erhalten wir eine
erfüllende Belegung f i r F.
48. Flir (a) genügt es offensichtlich zu zeigen: F ist gültig g n a u dann, wenn
VxF gültig ist. Es gilt:
F ist gültig gdw für alle (zu F passenden) A ist A ( F ) = I gdw für alle (zu
F passenden) A und für alle a E UA ist AITIfi1(F) = 1 gdw für alle (zu F
passenden) A ist A ( V z F ) = 1gdw Q z F ist gültig.
(b) zeigt man analog.
50. Sei a ein beliebiges Element aus FA.wr definieren nun B = (u~, I~ijmit
Uo = U { h l , . . . , b,-, 1. Ferner ist IB eine Erweiterung von I J , SO dass fiir
jedes Prädikatsymbol P, für das IA definiert ist, gilt: (. . . , b„. . . b,, . . .) E .
PB gdw. (. . . ,n, . . . , a , . . .) E PA.Ähnlich wird mit den Funkhonen ver- 57. A(Vz3yP(x,y)) = 1 gilt genau dann, wenn es für jedes ,IL E U> ein
fahren: f "(. . . ,b„ . . . , b j , . . .) = f A ( . . . , U , . . . , U! .. .). Mit dieser Definiti- 11 E L> gibt mit p A ( u ,V).
on von B gilt Bl,/,l(F) = AI,I,l(Fj für alle Variablen X, FormeIn F und Ferner ist A(3yVxP(s,Y)) = 1genau dann, wenn es ein u f UA gibt, so dass
U E { b l , . . . , h,-,). Nun kann durch Induktion über den Formelaufbau ge- für alle v E UA gilt: p A ( u , V ) .
zeigt werden, dass A ( F ) = BIF). Wenn also A ein Modell für F ist, dann
Die erste Aussage folgt offensichtlich aus der zwerten.
auch B. Der interessanteste Fall bei deser Induktion entsteht, wenn F die
Bauart VTGhat. Dann gilt: A(F) = 1gdw. für alle u E U* gilt ALTIM] (F)= 1 Die Umkehrung gilt jedoch nicht, wie das Gegenbeispiel
gdw. für alle ?J, 6 UB gilt B[,/,](F)= 1 gdw. B(VxG) = 1.
Ein entsprechender Beweis zeigt die Existenz von B,.
zeigt.
51. F = V x b V x ( ( x = y) V (y = z j V (T = z )j. WesentIich ist hier das Vor-
handensein der IdentitM. Die vorige Ubung ist nur für Formeln ohne Identität
korrekt. 58. Wir zeigen zunächst eine Variante des Überf~hnin~slernmmas
für Terme
t ,'t und Variablen X
A(t'[x/tl) = drZ~~(t)l(t'l
durch Induktion über den Aufbau von t'.
Für t' = y - also eine andere Variable als X - gilt:
55. Gegenbeispiel für beide Inäquivalenzen: Sei die Grundmenge von A die
Menge der natürlichen Zahlen. Die Interpretationen von F und von G seien Wrr zeigen nun das Überführungslernma durch Induktion über den Formel-
so beschaffen, dass AkJnl(F) genau dann = 1 ist, wenn n geradzahlig ist, und aufbüu von F.
bei G entsprechend mit ungeradzahlrgern n. Falls F eine atomare Formel ist, also F = P(t,, . . . :t,), so geht der Beweis
analog zu dem oben gegebenen (ersetze f durch P).
56. Sei A eine beliebige, zu F und G passende Struktur. Es gilt: A(F) = I Falls F die Form F = (G V H) hat, so gilt
genau dann, wenn aus A(3xP(s)j = 1 folgt A ( P ( y ) )= L. Dies gilt genau
dann, wenn folgendes gilt: Wenn es ein Element u E lj'A mit PA(u)gibt, dann
A ( F [ x / t ] )= 1 gdw. A(G[s/t] V H[rc/t]) = 1
muss auch P A ( y Agelten.
) Nochmals anders ausgedrückt: für alle u E UA gdw. A(G[z/t]) = a oderA(H[x/t]) = 1
folgt aus PA(u),dass PA(yA)gilt" Diese letzte Formulierung entspricht aber gdw- A [ x ~ ~ ( t ) J=( 1 ) A [ T / A ( ~ )=
Goder ](H
1)
gerade A(G) = 1. gdw. A[,JA(~)](G V H ) = 1
Die Fälle F = (G A H ) und F = 1 G gehen analog. 63. Bereinigen:
Habe nun F die Form F = 39G, dann gilt: Vz3y(P(x, g(y), z ) V +tQ(t)) /1 -Vu3viR(f (V, U): U )
input (X);
forn := 0 , 1 , 2 , . . . dobegin
if f (n)= z then output (1);
if f (n) > X then output (0);
end
for n := 1 , 2 , 3 , .. . do
for alle Indexfolgen ( i T .l ..,in) f (1, . ..:k)" do
if xii .. . zi,= ui,. . . yinthen stop
input (n);
Interpretiere n als Codierung eines Paars von natürlichen Zahlen,
als0 R = c ( x , ~ ) . Umformen in KIauseldarstellung von (a) und ~ ( bergibt:
)
if A angesetzt auf z stoppt in y Schritten
then output(x) else output(a);
Der Algorithmus stoppt offensichtlich immer und kann nur Wörter ausgeben,
die in M liegen. Daher ist f eine totale und berechenbare Funktion und der
Wertebereich von f ist eine Teilmenge von M. Sei nun umgekehrt z E M
beliebig. Dann stoppt A, angesetzt auf z innerhalb einer gewissen Schrittzahl Der Beweis ist erbracht durch
77. Nehmen wir an, zu "entflechten" sei s 7 i l i l sub2. Teste für jede Einselsub-
~ , t eine (oder mehrere) Vanable enthält - sagen wir ?I
stitution [ x / t ]in Y T L ~ ob
- die in subz ersetzt wird, 2.B. durch [y/s] . Ersetze in diesem Fall [.r/t]durch 84. (a) Die Existenz eines rechts-neutralen Elements wird ausgedrückt durch:
[x/tI~/sll-
79. Bei dem angegebenen Beispiel wächst bei jedem Unifikationsschritt Lsub
etwa auf die doppette Lmge an. Daher hat jeder Algorithmus, der Lsu6 expli- Gesucht ist nun ein Resolutionsbeweis, der auf den Klauseln (aj ( f ) basiert.
zit - etwa als String - intern reprhentiert, exponentielle Laufzeit. Hier hilft
Die folgenden Beweise wurden per Computer gefunden. Der kompakteren
das Verwenden von Zeigern weiter: Sobald in einem Literal eine Variable X
Darstellung wegen verkürzen wir mehrere, drekt aufeinanderfolgende Reso-
durch einen Term t im "gegenüberliegenden" Literal crsetzt werden muss,
lutionsschritte graphisch in einen einzigen Schritt (sog. Hypemsolirtion):
wird lediglich ein Zeiger von X nach t eingerichtet. Diese Zeiger sind in einer
"Variablenbindungsliste" zusammengefasst. Hierdurch wird vermieden, dass
t (evtl. mehrfach) dupliziert werden muss, um für (alle Vorkommen von) X
einkopiert werden zu können.
Vw (Gr (W) 3 GI ( W ) ) .
Hierbei sind U , 6, c Skolemkonstanten. Eine Herleitung der leeren Klausel aus Umformen der Negation der Behauptung in Klauselform ergibt die beiden
(a)-(e) und (g)-(i) ergibt sich wie folgt: Klauseln
Ein Beweis der Behauptung ist gegeben durch das folgende Diagramm:
85. Da nur von Drachen die Rede ist, verzichten wir auf ein explizites Prädikat
''Drache sein". Wir führen die felgenden Prädikate ein:
87. Sei n die Anzahl der Atomformeln. Seien P ( n ) bzw. L ( n ) die im Beweis
der Vollstiindigkeit der P-Resolution bzw. linearen Resolution erzeugten Be- 90. Da die N-Restriktion vollständig ist, gibt es für jede unerfüllbare Horn-
weislängen (bezogen auf das Beispiel des Aufgabenstellung). Dünn ergeben klauselmenge einen Resolutionsbeweis, in dem immer mindestens eine El-
sich die Rekursionsgleichungen: ternklausel negativ ist. Die Hornklauseleigenschaft garantiert, dass alle Re-
solventen in einer solchen Resolutionsherleitung negativ sind. Zwei negüti-
ve Klauseln können jedoch nicht miteinander resolviert werden. Somit ergibt
sich, dass eine Elternklausei immer aus dem Input stammen muss. Dieser N-
Diese Gleichungen haben die Lösungen: Resolutionsbeweis ist also gleichzeitig ein Input-Resolutionsbeweis.
91. Wir zeigen durch Induktion über die Anzahl der vorkommenden Atomfor-
meln, dass jeder Einheitsresolutronsbeweis in einen Input-Resolutionsbeweis
überführt werden kann. Der Induktionsanfang n = 0 ist klar, Angenom-
88. Bei dem Beispiel men, wir haben einen Einheitsresolutionsbeweis für eine Klauselmenge F
mit n > O Atomformeln gegeben. Dann muss in der Ausgangskfauselmen-
{A, B ) , (4+I1 {TA:B } , (TA:T B ) ge mindestens eine ernelementige Klausel vorhanden sein, z.B. {L). Wir be-
trachten nun FLeI.Diese Klauselrnenge besitzt gleichfalls einen Einheitsreso-
einer unerfüllbaren Klauselmenge kann bei Einhaltung sowohl der P- als auch
lutionsbeweis (der sich abzüglich von Resolutionen nach L aus der Struktur
der N-Restriktion im ersten Schritt nur {A, B) und { T A :T B } resolviert wer- des ursprünglichen Beweises ergibt). Nach Induktionsvoraussetzung gibt es
den (was die beiden Resolventen (B, T B ) und { A ,1,-2} ergibt). Weitere Re- einen Input-Resolutionsbeweis für FL=l. Wicdereinführen von ¿ in dicsen
solventenbildungen sind dann nicht mehr möglich. Beweis liefert eine Input-Resolutionsherleitung von von { E ) . Diese Klausel
kann dann im letzten Schritt gegen {L) resolviert werden. Dieser letzte Schritt
89. Sei (XI,K 2 , .. . , &) die Folge derjenigen Klauseln, die in Schritt 1 ist ebenfalls eine Input-Resolution.
bzw. 2 des Markiemngsalgorithmus' aus Abschnitt 1.3 Anlass zu Marhe-
Die Umkehrung zeigen wir auch durch eine Induktion über die Anzahl der
rungen geben. (Dies srnd in Schritt 1 die einelementigen, positiven Klau-
vorkommenden Atomformeln. Der Induktionsanfang n = 0 ist klar. Ange-
seln und in Schritt 2 alle Klauseln der Form K, = {-.41, . . . . lrl„ B ) bzw.
nommen, wir haben einen Input-Resolutionsbeweis für eine Klauselmenge F
mit n, > 0 Atornfomeln gegeben. Dann muss in der AusgangsklauseImen-
ge mindestens eine einelementige Klausel vorhanden sein, z.B. {L}, denn im
letzten Resoluiionssch~ttwerden zwei einelementige Klauseln resolviert, und { P ( k o pf , k o p f , kopf , zahl, zahl, zahl, so)],
eine davon muss aus dem Input stammen. Dieser Input-Resolutions'beweis {1P(X~,X2y X3, x d , x 5 i x6,S),7R(X11X), 1R(x2, '2)i
kann zu einem Input-Beweis von FfAXlverkürzt werden. Nach Induktions- p(ylr X3rX4i X5iX6i tl2(S))}i
&1
voraussetzung gibt es einen Einheitsresolutionsbeweis für FL=i.Ferner kann { y P ( X I :X2, X3, X4,AG,X e , S ) . l R ( X 2 ,Y,},l R ( X 3 ,Y3),
mittels Einheitsresolutionen aus F erzeugt werden. Zusammengesetzt P ( X 1 , hihrX41X5iX61t23(S))]l
ergibt dies dann einen Einheitsresolutionsbeweis für F.
{ l p ( X l : X?,X3.1%1 X5,X6. S):-'R(X3,y3)i'R(X4: Y i ) i
p ( X l , X ? :Yb X i X 5 i X ~ f34(S)))i
i~
92. Wir argumentieren semantisch: Sei F eine unerfüllbare Klauselmenge, sei {lP(X1,X2,X3:X~lX5iX6:S)g~R(X4rh).~R(X~:%),
I< eine Tautologieklausel in F und sei F' eine minimal unerfüllbare Teilmen-
P(X1,x2, Y4, Y5,X ~ t&(S)))l
i
ge von F. (Wir wissen, dass jeder potenzielle Resolutionsbeweis schon auf F'
{ ~ P ( XX2,X3,X4,
I, X5, X61S ) ,l f l ( X 5 ,I$): 7R(Xsl & I l
basieren kann). Dann gilt: K $! F' (und dies beweist dann die Behauptung).
Begründung: Angenommen, K E F', d.h. F' - K ist erfullbar. Dann ist aber P(X11X2i X3tX4i Y5:hrt56(S)?}i
auch F' erfüllbar (mit derselben Belegung), da K eine Tautologie ist. C R ( k 0 ~ fzahl)
i 1,
IR(zahE7 kopf 11,
Ein syntaktischer Beweis müsste aufzeigen, wie ein Resolutionsbeweis, so- l , f , A l , knp f , zahl, kopf, S ) ,An,tuiort(S)}
{ ~ P ( z a h kop
fern er eine Tautologieklausel verwendet, umstrukturiert werden kann, so dass
er ohne diese Klausel auskommt.
Hierbei sind Variablen durch Großschreibung zu erkennen.
93. Gegenbeispiel:
96. Diese Aufgabe lässt sich grundsätzlich nach dem gleichen Rezept wie die
vorige (und die Affe-und-Bananen Aufgabe) lösen. Es entstehen so jedoch
unangemessen viele Klauseln.
Da Hornformeln höchstens ein positives Literal enthalten, wird in mindestens
einer der Elternklauseln in einem Resolutionsschritt immer nur ein Literal
zur Unifikation herangezogen. Es kann also höchstens in der anderen Eltem- 97. (a) {mitjlied(tom))
Hause1 passieren, dass mehrere Literale durch den Unifikationsprozess ver- (b) {mitglied ( m i k e ) }
schmelzen. In diesem Fa11 kann dieser eine Resolutionsschritt immer durch (C) {mitglied(johra)}
mehrere aufeinander folgende binäre Resolutionsschritte ersetzt werden. Die- (d) {lmitglied(x),skz(x), berg(z))
ser Umfomungsschritt zerstört nicht die bei Hornfomeln vollständigen Re-
(e) {-berg(z), liebt ( X ,regen))
striktionen.
(0 { y s k i ( x ), liebt ( X ,schnee))
( g ) {yliebt (mrke,schnee),lIiebt(tom, schnee)}
94. Die genau eine-Bedingung ergibt zwei Klauseln: (h) {liebt (turn, scknee j, liebt (mike, schnee))
(i) { l l i e b ~ ( m i k eregen),
, iliebt(tom,regen)}
{ i l i e b t ( E v a ,Wezn),-liebt(Anna, Wem)}
(j) {lzebt(tom,regen),lieht(mike,regrrt))
{liebt(E?in,Wein),lieht(Anna,Wezn)}
(k) {Iiebt(rnike,schnee))
(1) {liebt(john,schnee)}
Zusammen mit der Aufrufklausel {~Eicbt(Eua, z ) ,Antwort (2)) ergibt sich
(m) {lmitglied(a),lberg (X),s k i ( x ) ,Antworf(x)}
nur ein möglicher Resolvent: {Eiebt(Anna,Wem),Antwort(Wezn,)}.Die-
ser könnte in Worten so interpretiert werden, dass die Antwort Wein ist, wenn
bewiesen wäre, dass Anna nicht Wein liebt. Der Gesuchte ist Tom:
v-
ski (X), Antwort (X)} ( f j
{~rn~t,~lied(x),
nach Induktionsvoraussetzung wohldefiniert als a(rc - 1: 1).Für X
y > 0 ist
> 0 und
{-.rnitglied
V
(X), liebt (X,schnee), Ant~i)ort(x))(a)
(liebt
V
sch,nee),Antwort (tom)} (g)
(tom,
Daher wird a ( x ,y) auf mehrfaches Auswerten von a(z- I,. . .) zurückgeführt,
welches nach Induktionsvoraussetzung wohldefiniert ist.
V
schnee) , Anteriart(tom)} (k)
{ilkieht (mike,
Logik-Programm:
Ack(0, I', s ( Y ) ) .
V
{Antworf(tom)}
A c k ( s ( X ) ,0 , Z ) :- Ack(X, s(O), 2).
A c k ( s ( X ) ,s ( Y ) ,2) :- A c k ( s ( X ) ,Y,W ) ,A c k ( X , W,2 ) .
99. Indern man den zweiten und dritten Parameter als Eingabeparameter ver-
steht und den ersten Parameter als Airsgabeparametec
?- P(b,2 )
Antwort:
X =a I
Die Berechnung von 3+2 verläuft nun 105. Ein f nch(G * F, 0) :- Ein f ach(G, 0).
wie
add(s(s(3(0))), ~ ( ~ ( 0 Z) ,) ; ~ ( 0 12)
add(~(~(~(3(0))))? , Ein f uch(F * G ,U) :- Ein jnch(G, 0).
), 2)
u d d ( s ( s ( s ( ~ ( s ( O ) ) ) ) 0: a,wobei sich im letzten Schritt die Substi- Ein f arh(F + G , H):- Ein f nch(G,0), Einfach ( F ,H ) .
tution [Z/s(s(s(~(s(O)))))] ergibt.
EPnf aeh(G + F, H ) : - Einf adl(G,U), Einf ach(F,H ) .
102. Mit Induktion nach y weist man leicht nach, dass n(1, y) = y 2, + Ezn f ach(F * G ,H ) :- Ein f nch(G, l ) ,Ein f ach(F,I-I).
u(2, y) = 2y+3, (I@. y) = 2Y+3-3. Damit erhalten wir: a (4,2) = 4 3 : ~ ( 4 1 ~ 1 ) ) Ezn f ach(G * F H ) :- Etn f ach(G,1) Ein f ach(F H).
= a(3, a(3, a ( 4 , O ) ) ) = a ( 3 , a(3,a(3, l j ) ) = a(3, ~ ( 3 ~ 1 3=) )4 3 , 6 5 5 3 3 ) = Ein f ach(F, F ) .
265533 3 > 1019728-
Wir zeigen, dass n(x,y) wohldefiniert ist durch Induktion nach X. Für X = 0 (Hier wird die Beweis-Suchstrategie von Prolog vorausgesetzt).
und beliebiges ist a wohldefiniert als y + 1. Für z > 0 und y = 0 ist a(x,y)
106. Wir betrachten zunächst den Fall, dass die Ableitung aus nur einem
Schritt besteht. Genauer, wir zeigen, wenn Gsuh' mit einer Progrmmklau-
sel K E F resolvierbar ist zu einem Resolventen K' (wobei der allgemeinste
Unifikator sub angewandt wurde),
309. Es gilt (durch Induktion nach n): UpF(0) C 0 ~ ? ' ( 8 ) für alle r i 2 0.
Deshalb folgt F ~ F OpF(Fp=).Sei umgekehri G E OpF(FpF).Dies ist
V:,
Gsub'
der Fall, weil es aufgrund der Definition von OpF() entsprechende Formeln
G I ,... ,GkE FpF gibt. Es gibt einen Index n, so dass GI, . .. ,GI, E 0~x0).
Daher ist G E Op",+'(fl) FpF Damit ist die Fixpunkteigenschaft von F ~ F
gezeigt.
dann sind auch G und K direkt resolvierbar zu einem Resolventen I<", so Sei nun M ein beliebiger Fixpunkt, also M = O p F ( M ) Dann. gilt 0 C hf
dass bei dieser Resolution ein allgemeinster Unifikator sub" angewandt wird und wegen der Monotonie des OpF( } Operatms: & ) F ( @ ) C O p p ( M )= M.
und für eine geeignete Substitution s gilt: K' = Kt's. Und weiter, für beliebige n, D$(@) OpF(M) = M. Deshalb ist F p F =
u,OpF(@)C M. Daher ist FpF der kleinste Fixpunkt.
G K Als nächstes zeigen wir S„, (F,G) Sfixpunkt (FiG ) . Wenn H = (.41A . . . A
ilk)sub E Sv„(F,G), dann gibt es eine SLD-Hesleitung des Form
Die Behauptung beweisen wir wie folgt: K' ist Resolvent von Gsub' und K
und hat deshalb die Form
K' = ((Gsub' - L ) ( K - Li))suh Hierbei seien subl, . . . , sub, die verwendeten allgemeinsten Unifikatoren.
wobei L und L' unjfizierbx sind mittels sub. Deshalb existiert in G ein Litera1 Dann ist (AL A . . . A Ak)subl... sub, das Rechenresultat und für eine ge-
L,,, so dass Losubl= L. Da sich subr und sub gegenseitig nicht beeinflussen eignete Substitution s ist H = (Al h . . . S\ Ak).9ubl. . . sub,^.
(Gund K sind variablendisjunki umbenannt), gilt Lgsub'~ub= Ltsub's~b. Indem wir die verwendeten Programmklauseln Kl, . . . , K, - also die Seiten-
Das heißt, LU und L' sind unifiüerbar und damit G und K resolvierbar. Sei klauseln bei der Resolution - in umgekehrter Reihenfolge verwenden, und
sub" allgemeinster Unifikator von Ln und L'. Dann gilt für eine geeignete zwar in der mittels sub1 . . . S U ~ grund-substituierten
~ S Version, erhalten wir
Substitution s: sub'sub = subl's und ferner, dass die entsprechenden Formeln in O p k ( @ .).,.,Oien,(@), die 'bezeugen", dass H
in Sfixpunkt ( F ,G)liegt-
K" = ((G - L,) U (K - Fjjsuh'' Für die umgekehrte Inklusion sei H E Sfi,,,unkt (F,G). Hierki ist H = (Ai A
. . . /\ AL) eine Gnindinstanz von (Al /\ . . . h Akj, wobei G = ?-Al, . . . ,Ak.
Resolvent von G und K ist. Damit ist die Behauptung bewiesen.
Es ist H E Fpp. Daher ist H für ein n in OpF(0).Aufgrund der Definition
Die allgemeine Form des Lifting-Lemmas erhält man nun durch iteratrves von OpF() können wir für i = 1,.. . , k gewisse Grundinstanzen K: = Ai
Anwenden der Behauptung (also durch Induktion). :- B , . . . , B i 3 ,von Programmklauseln K, E F identifizieren, die für die
Mitgliedschaft von A, in OpF(0)verantwortlich sind. Hierbei sind die BI, in
107. Die einzig mögliche erfolgreiche Rechnung liefert die Substitution [e/u]. OpF1(fl). Aus diesen Angaben setzen wir den Anfang einer SLD-Resolution
Daher ist wie folgt zusammen:
= { ( P ( a ,U) A P(a, 0)))
P.
115. Der Prolog-Interpreter lieferk X = [rl, [d, e],b; C, n, C, f Irn zweiten Fa11
ergeben sich die möglichen Antworten:
,Y = [ I Y = [U. b, C, a]
X = [U] Y = [b, C . U]
Diese Ableitungsfolge können wir nun nach dem gleichen Schema für n - X=[u.b] Y=[c,a]
1, n - 2 , . . . ,1 fortsetzen. Tm Fa11 n = 1 können nur einelementige Fak- X=[a,b,c] Y=[a]
tenklauseln Kiangewandt worden sein. Daher ergibt sich am Ende die Ieere X = [a,b,c,a] Y =[I
Klausel. (Bem: Da wir bei dieser Ableitung nicht immer nach dem am weite-
sten links stehenden Litera1 in der Zielklausel resolviert haben, müssen wir -
irn Vorgriff - eigentlich das Vertauschungslemma verwenden). 116. Die "naive" Programmierung von recersc wäre folgende:
Aus dem RechenresuItat dieser Resolutionsherleitung I ässt sich nun durch reverse([ 1, [ 1).
Grundsubstitution H gewinnen (Lifting-Lemma), also ist H in S„„ (F,G). reverse([AIB], C) :- [Al, C),
reverse(B, D), uppti.r~d(D,
Diese hat jedoch den Nachteil, dass zum Umdrehen einer n-elemenligen Li-
ste etwa n2 viele Rechenschritte auszuführen sind. (Dies ergibt sich dusch
die fortgesetzten Anwendungen von a.ppend). Eine raffinierte Lösung ist die
folgende:
111. Beispiel: a :- a. re.iierse(A, B ) :- rev(A, [ I , B).
I,
rev(I z,z1.
112. Nach der Ergebnisausgabe wird der Benutzer gefragt, ob er weitere .r.ev([XIY],U,V ) :- rcv(Y,[Xllij,V ) .
Lösungen sehen will. Wenn ja, so wird success auf false gesetzt und einfach Diese Lösung hat nur einen Aufwand, der linear in n ist.
die Prozedur auswerte fortgesetzt. Soll jede Teilliste gespiegelt werden, so ginge das etwa mittels
113. Wir drücken Symmetrie und Transitivität einer zweistelligen Relation P deepreverse(X,X ) :- atomic(?l).
aus und geben einige Fakten über P-Beziehungen an: deepreverse([1: [ 1).
deepreverse([+4131,C) :- deeprevcrsr(A, D);
(a) 6). deepreverse(ß, E);
(b) P(c,B). append(B, [D],C).
(C} P ( X , Y ) :- P ( X , Z ) , P ( Z , Y ) .
(d) P ( X , T) :- P ( Y , X ) .
117. anzahl ( [ I ,0).
Die Anfrage ?-PIc. U ) könnte beantwortet werden dusch Anwenden der Pro- anzahl(X, 1) :- atornir(X).
grammklauseln (C), (b), (d), (a) - in dieser Rcihenfolge. Da jedoch die Regeln anzahl([X I Y], N) :- anzahl(X, 1Vlj,
(C), (d) immer anwendbar sind, gerat der Frolog-Interpreter bei jeder Anord- anzahl(Y,N 2 ) ,
nung der Klauseln in eine Endlosschleife. ihr is 1Y1 11-2. +
q.uort(Y2;22),
append(Z1:[X 1221,Z).
pfirtition(X, [ J, [ I , [ 11.
pnrtztion(X, [AIB],[AIYI],Y2) :- X 5 A,pnri2tion(X, B, Y1,Y2).
Y l , [AIY2]) :- X > A,partition(X,B , Y1, Y 2 ) .
p a ~ t z t i o n ( X[AIB],
,
Wenn in diesem Fall C nicht beweisbar ist, wird wegen des cuts dre Regel a:-d
(wie gewünscht) nicht mehr berücksichtigt.
119. Eine vollständige Losung dieser Aufgabe würde den Rahmen dieses Bu- Fall 2: b ist nicht beweisbar:
ches sprengen. Der LRser sei stattdessen auf che Bücher von Arnble und von
Sterling, Shapiro hingewiesen.
120. Für diese Aufgabe sei auf das Buch von Kluiniak und Szpakowicz ver- - b ! ?Lfj
wiesen.
121, Der Prolog-Auswertealgorithmus muss an zwei Stellen modifiziert wer- 123. (a) Endlosschleife:
den: Als erstes muss (zwischen else und begin) ein Test eingebaut werden,
der feststellt, ob D 1 = !. Im positiven FA1 wird die Prozedur rekursiv mit
auswerte.(?-Dz, . . . , Dk.sub) aufgerufen. Falls dieser rekursive Aufruf mit
success=false zurückkehrt, wird eine globale Boolesche Variable cut auf true
gesetzt (die mit false initialisiert wurde).
Nach dem rekursiven Aufruf von auswerte innerhalb der while-Schleife muss
eingefügt werden:
(b) Die Klausel spaß an die erste Position bringen.
if cut then (C) Die Klausel lustig :- unsinn ersetzen durch lustig :- !,unsinn.
begin (d) spaß :- !,W&,lustig fuhrt dazu, dass Prolog mit der Antwort nein stoppt.
if C*,1,.. . , Ci,„
enthält den cut then spaJ3 :- witz, !,lustigund spaJ :- witz, lustig,! führen auf Endlosschleifen.
cut := false;
return {Rückkehr aus der Prozedur)
124. Ein Hornkl auselprogramm F besteht bekanntermaßen aus positiven Fak-
end
ten und aus Regeln. Wenn T A eine Folgerung aus F ist, dann ist F -+TA
eine gültige Formel und F A A unerfüllbar. Dies ist ein Widerspnich, denn
Diese Modifikation ist nur für ein Vorkommen eines einzigen cuts korrekt. Im F A A ist sicher dadurch erfüllbar, dass alle Atomformeln mit 1 belegt wer-
allgemeinen Fall müssen die cuts "markiert" bzw. nummeriert werden, um den.
diejenige Prograrnmklausel, die für einen bestimmten cut verantwortlich war,
feststellen zu können.
Dieser allgemeine Fa11 tritt 2.B. in Ubung 125 auf.
b
1
? - U , ! , fad, !, fail,!,fai
1
3-!, f ail, !, f ail, !, f ail
T. Amble. Logic Pmgmmming und Knowledge Eagineeririg. Addison-
I
?-fail,!, jail,!, fail Wesley, Reading, MA, 1987.
K. R. Apt und M. H. van Emden. Contributions to t h t theory of logic pro-
1 g r d n g . Journal of the Associatina for Complating Machirzey, 29
?-!, S c l i l
Icut] (1977): 841-862.
G . Asser. Einführung in die mathematische Logik I - 171. Verlag Harri
Deutsch, FrankfurtIM, 1972.
M. Bauer, D. Brand, M. Fischer, A. Mcyer, M, Paterson. A note on dis_iunc-
a nicht als Fakt vorhanden: tive form tautologies. SIGACT NEWS, Vol. 5, No. 2, (1973) 17-20.
1r-7
D. M. Gabbey. Eiernentary Logic - A Prcicedurai Perspwctiva. Vorlesungs- R. Kowal ski. Predicate logic as programming language. fnfomzation Pm-
sknpt, Imperial College, London, 1984. cessing 74,569-574, North-Holland, 1974.
J. H. Gallier. h g i c for Computer Science - Foundations ofAutomtic n e o - R. Kowalskr. Logicfor Problem Solving. Eisevier North-Holland, Amster-
mm Pmving. Harper & Row, New York, 1986. darn, 1979.
M. Gardner. b g i c Machines nnd Diaigrums. The University of Chicago R. Kowaiski. Algonthm = Logic + Control. Journal of the Association ji7r
Press, Chicago, 1958. Contputing Muckiae-y 22 (1979): 424436.
M. Genesreth und N. Nilsson. Logical Foundatioas qf Arrijiciai Intelligence. M. k v i n . Marhemcarical Logic for Cnmp~iterScielatisas. TechnicaI Report,
Morgan Kaufmann Publ., 1987. MIT Project MAC, 1976.
F, Giannesini, H. Kanoui, R. Pasero und M. van Canegham. PROLOG. Add- H. R. Lewis und C. H. Papadimitriou. Elements of the Theory of Computa-
ison-Wesley, Reading, MA., 1986. tion, Küpitel 8-9. Prentice Hall, Englewood Cliffs, NJ, 1981.
D. Siefkes. Fomalisieren und Beweisen - Logik für Informatiker. Vieweg,
H.R. Lewis. Unsolvable Classes of Quanrlficational Formulas. Addison-
Braunschweig, 1990.
Wesley, Reading, MA., 1979.
J . W. Lloyd. Foundations of h g i c Progrmming. Springer-Verlag, Berlin, J. Siekrnann und G. Wrightson (Hg.). Automation qf Reasoning 1 + 2.
Springer-Verlag, Berlin, 1983.
1984.
L. Sterling und E. Shapiro. The Arf of Prolog. MIT Press, Cambridge,
D. W. Loveland. Autonaaled Theorem Proving: A Logical Basis. Elsevier Massachusetts, 1987.
North-Holland, New York, 1979.
A. Tarski, A. Mostowski und R. M. Robinson. Undecidable TAeuries.
D. Maier und D.S. Warren. Computing wifh Logic. BenjaminlCummings
North-Holland, Amsterdam, 1971.
Fubl. Comp., Menlo Park, 1988.
A. Thayse ('I@ .)Logic to Logic Programming. Wiley, 198 8.
From Standard
2. Manna. Mathematical n e o y of Computatiun, Kapitel 2. McGsaw-Hill,
New York, 1974. R. Turner. Logics for Artijiciak Intelligence. Elis Horwood Limi tcd, 1984.
J. Minker (Ed.). Foundations of Deductiw Databoses und h g i c Program- A. Urquhart. Hard examples for resolution. Journal of the Assocation of
ming. Morgan Kaufmann Publ., Los Altos, Ca., 1988. Computiag Mahineql34 (1987): 209-2 19.
L. Naish. Negation und Control in PROLOG. Lecture Notes in Computer T. Varga. Mathematische L,ugik,firA.fÜnger I t II. Verlag Harri Deutsch,
Science 238, Springer-Verlag, Berlin, 1986. FrankfurtlM, 1972.
N.J. Nilsson. Problem Solving Methods in Art@cial Intelligence, Kapitel H. Vollmer. Resolutionsverfeinerun~e~~ Stu-
w d ihre Vollst~ndigkitss~tze.
6-8. McGraw-Hill, New York, 1971. dienarbeit, EWH Kobfenz, 1987.
R. Nossum. Automated theorcrn proving methods. BIT, 25 (1985): 5 1-64. C. Walther. Automatisches Beweisen. in: Kün.stliche Intelligenz. Fachbe-
richte Informatik 259, Springer-Verlag, Berlin, 1987.
M.S. Paterson und M.N. Wegman. Linear Unr fication. Jounzal uf Cumputer
aad System Sciences, 16 (1978):158-167. L. Wos. Automated Reasoning - 33 Basic Research Problems. Prentice-
Hall, Englewood Cliffs, NJ, 1988.
PROLOG. Spezialausgabe von Cornmunications of tlie Assoclution for
Computing Machinery, 28, No. 12 (1985). L. Wos, R. Overbeek, E. Lusk und F. Boyle. Automated Reasoning - Inrro-
ductinn uadAplications, Prentice-Hall, Englewood Cliffs, NJ. 1984.
W. Rautenberg. Nichtklassiscl~eAussagenlogik. Vieweg, Braunschweig,
1979.
M.M. Richter. Logikkulküle. Teubner Verlag, Stuttgari, 1978
M.M. Richter. Prinzipien der kidnstiichen Intelligenz. Teubner-Verlag, Stutt-
gart, 1989.
J. A. Robinson. h g i c : Form and Function. Elsevier North-Holland, New
York, 1979.
B. Rödding. Einfuhrung in die Pradikurenlogik. Vorlesungsskript, Univ.
Münster, 1970.
J. R. Shoenfield. Mathemarical Logic. Addison Wesley, Rcading, MA.,
1967.
W. Schwabhäuser. Modellthenrie 1 + 11. Bibl. Institut, Mannheim, 197I.
W . Schwabäuser. Prärlikatenlogik. Vorlesungsskript, Univ. Stuttgart, 1976.
Symbolverzeichnis Index
Absorption 24 Berechenbarkeitstheorie 69,7 1
Ackermannfunktion 124 bereinigt 62
7 14 Res* ( F ) 42,97 E ( F ) 84 Addition 122 Beweis 43
V 14 3 52 [I 94,152 add 147 binäre Resolution 111
A 14 V 52 QH 101 Affe-und-Bananen-Problem 11 8 BPF 63
-+ 14 F* 52 Antwort 121 Algorithmus von Gilmore 82 breadth-first Strategie 140
tt 14 F r e i ( F ) 53 --. 127 Allabschluss 97 Breitensuche 140
14 U, 54 ?- 128 allgemeingültig 55 Bubble-Sort 138
A2=1
V:==' , 14 I, 54 + 131 allgemeinster Unifikator 89
Allquantor 50 Church 7 1
A 15,5F fA 54 0 138
d 15 PA 54 Smod 139 Antwortemugung 113 Clark 129
18.57 z A 54 OpF 140 Antwortprädikat 115 closed world assumption 153
anzahl 147 Colmerauer 143
$L 18,57 .AI./.] 57 O p y 140
compactness theorem 34
append 146
23,61 [xltl
63 F~~ 140 äquivalent 23 compiIe 148
KNF 27 BPF 66 Sjispunkt 140 Arithmetik 76 cons 145
DNF 27 E 75 [~YI 152 ASCA 148 czlf 148
40 T h ( A ) 78 ! 156 Assosiativität 24
Res(F) 41,97 Cons(M) 78 not 161 atomare Formel 14, 50 Datenbank 132, 145
Resn(F) 42,97 D ( F ) 80 fail 161 atomic 146 Deduktion 43
Aufrufklausel 1 15, 121 definite Klausel 105, 121
Ausdrucksschwäche 152 deMorgan 24
Ausgabeparameter 1 17 Denotation 132
Aussage 50 depth-erst Strategie 140
Aussagenlogi k I3 Differenzieren 127
Auswahlaxiom 65 Disjunktion 14
Auswahlregel 138 disjunktive Normalform 27
Auswertungsstrategie 141 Distributivität 24
axiomatisch 75 DNF 27
rtxiomatisierbar 36, 76 Doppelnegation 24
Axromensystem 36, 75, 114 dove-tailing 172
Tatsachenklausel 121
Tautologie 18
Teilfomel 14
Term 49
Theorie 74, 114
Theorie der Gruppen 75
Tiefensuche 140
überfühmngslemma 61
Urnbenennung 61
unentscheidbar 68, 69
Unentscheidbarkeit 68