[Michael r. genesereth,__nils_j._nilsson__(auth.),(book_zz.org)

1. Michael R. Genesereth Nils J. Nilsson Logische Grundlagen der Knstlichen Intelligenz

2. Artificial Intelligence Knstliche Intelligenz herausgegeben von Wolfgang Bibel und Walther von Hahn Knstliche Intelligenz steht hier fr das Bemhen um ein Ver- stndnis und um die technische Realisierung intelligenten Verhaltens. Die Bcher dieser Reihe sollen Wissen aus den Gebieten der Wissensverarbeitung, Wissensreprsentation, Expertensysteme, Wissenskommunikation (Sprache, Bild, Klang, etc.), Spezial- maschinen und -sprachen sowie Modelle biologischer Systeme und kognitive Modellierung vermitteln. Bisher sind erschienen: Automated Theorem Proving von Wolfgang Bibel Die Wissensreprsentationssprache OPS 5 von Reinhard Krickhahn und Bernd Radig Prolog von Ralf Cordes, Rudolf Kruse, Horst Langendrfer, Heinrich Rust LISP von Rdiger Esser und Elisabeth Feldmar Logische Grundlagen der Knstlichen Intelligenz von Michael R. Genesereth und Nils J. Nilsson 3. Michael R. Genesereth Nils 1. Nilsson Logische Grundlagen der Knstlichen Intelligenz bersetzt und bearbeitet von Michael Tamowski Friedr. Vieweg & Sohn Braunschweig / Wiesbaden 4. Dieses Buch ist die deutsche bersetzung von Michael R. Genesereth und Nils J. Nilsson, Logical Foundations of Artificial Intelligence. Morgan Kaufmann Publishers, Los Altos, California 94022 Copyright 1987 by Morgan Kaufmann Publishers Inc. bersetzt aus dem Amerikanischen von Michael Tarnowski, Stuttgart Das in diesem Buch enthaltene Programm-Material ist mit keiner Verpflichtung oder Garantie irgend- einer Art verbunden. Die Autoren, die Herausgeber der Reihe, der bersetzer und der Verlag bernehmen infolgedessen keine Verantwortung und werden keine daraus folgende oder sonstige Haftung bernehmen, die auf irgendeine Art aus der Benutzung dieses Programm-Materials oder Teilen davon entsteht. Der Verlag Vieweg ist ein Unternehmen der VerJagsgruppe Bertelsmann. Alle Rechte vorbehalten Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig 1989 Das Werk einschlielich aller seiner Teile ist urheberrechtlich geschtzt. Jede Verwertung auerhalb der engen Grenzen des Urheberrechtsgesetzes ist ohne Zustimmung des Verlags unzulssig und strafbar. Das gilt insbesondere flir Vervielfltigungen, bersetzungen, Mikroverfilmungen und die Einspeicherung und Verarbeitung in elektronischen Systemen. Umschlaggestaltung: Peter Lenz, Wiesbaden ISBN 978-3-528-04638-5 ISBN 978-3-322-92881-8 (eBook) DOI 10.1007/978-3-322-92881-8 5. v DANKSAGUNG Wir danken der Universitt Stanford und unseren zahlreichen Kol- legen und Studenten fr ihre Hilfe und Untersttzung. Der zweite Autor dankt auch SRI International fr die hervorragende For- schungsatmosphre ber viele Jahre hinweg sowie dem Palo Alto La- boratory des Rockwell Scientific Center fr die wertvolle Hilfe. Viele Leute haben die ersten Entwrfe dieses Buches gelesen. Einige schlugen wesentliche Vernderungen vor, andere entdeckten kleine, aber gefhrliche Feh;Ler. Ihnen allen danken wir und hof- fen' da die nachfolgende Liste nicht allzu viele von ihnen uner- whnt lt. James Allen Benjamin Grosof Karen Myers Mario Aranha Haym Hirsch Pandu Nayak Marianne Baudinet Jane Hsu Eunok Paek Edward Brink J osef J acobs Judea Pearl Peter Cheeseman Leslie Pack Kaelbling Donald Perlis Jens Christensen Doanld Knuth Liam Peyton Lai-Hen Chuan Kurt Konolige Charles Restivo Michael Dixon Ami Kronfeld Stan Rosenschein David Etherington Vladimir Lifschitz Dave Singhal David Fogelsong John Lowrance David Smith Peter Friedland Kim McCall Devida Subramanian Matthew Ginsberg Bill McClung Tom Strat Andrew Golding Andreas Modet Richard Waldinger Jamie Gray John Mohammed Elizabeth Wolf Yoram Moses 6. VII VORWORT Dieses Buch basiert auf zwei zentralen Annahmen: Fr den wissenschaftlichen und technischen Fortschritt einer wissenschaftlichen Disziplin ist erstens ein geeignetes mathematisches Handwerkszeug zur Formulierung und Zusammenfassung neuer Ideen ntig. Zweitens ist die symbolische Logik ein sehr wesentlicher Bestandteil der in der Forschung ber Knstliche Intelligenz (KI) verwendeten Mathe- matik. Beide Behauptungen mssen begrndet werden. Man sollte allerdings meinen, unser erster Grundsatz fnde eigentlich allgemeine Zustimmung. Dennoch gibt es in neuen Wissen- schaftsgebieten, in denen das Wissen hauptschlich an die Praxis und empirische Fallstudien gebunden ist, vehemente Einwnde gegen die Versuche einer Mathematisierung. (Einer der Autoren erinnert sich beispielsweise daran, wie sich in den 50-er Jahren einige Elektroingenieure darber beklagten, da zum Verstndnis von elek- trischen Schaltkreisen und Kontrollsystemen Differentialglei- chungen doch vllig unntig seinen!) Wir behaupten nicht, da das Wissen um die mathematischen Grundlagen und Techniken einer Diszi- plin allein ausreicht, um in der Forschung oder in der Praxis er- folgreich zu sein. Wir sind allerdings der Meinung, da zu einem 7. VIII Vorwort erfolgreichem Studium der modernen, insbesonders technisch orientierten Wissenschaftsdisziplinen immer auch ein solides mathematisches Handwerkszeug der jeweiligen Disziplin gehrt. Das Studium dieser Grundlagen bietet die Voraussetzungen, um die jeweilige Disziplin interpretieren, verstehen und ausbauen zu knnen. Da die KI eine noch relativ junge Disziplin ist, ist es nicht verwunderlich, da es hitzige und geistreiche Debatten zwischen "Formalisten" und "Experimentalisten" gibt. Die Formalisten meinen, die Experimentalisten kmen schneller voran, wenn sie ein tieferes Verstndnis der theoretischen Grundlagen der KI besen. Die Experimentalisten sind dagegen der Ansicht, die Formalisten tten besser, sich weniger mit den formalen als vielmehr mit den inhaltlichen Problemen zu beschftigen. Auch wenn wir zugeben, da die meisten Fortschritte in der KI (oder in einer anderen technischen Disziplin) durch Experimentalisten angeregt worden sind und die Formalisten meist nachtrglich dazu dienten, "aufzurumen und zu gltten", so sind wir dennoch der berzeugung, da die bedeutenden und neuen Ergebnisse in der KI von Forschern erzielt wurden, die ihren Experimenten eine fundierte theoretische Grund- lage zugrundegelegt hatten. Die theoretischen Gedanken der lteren Ingenierswissenschaften sind in der Sprache der Mathematik formuliert. Wir behaupten, da fr die KI die mathematische Logik die Grundlage jeder Theorie bildet. Obwohl zahlreiche Informatiker die Logik als grundlegend ansehen, stufen wir jedoch die Bedeutung der Logik noch sehr viel hher ein. In den Kapiteln 1 und 2 behaupten wir, da sich die KI hauptschlich mit dem Problem der Reprsentation und des Gebrauchs von deklarativem (im Gegensatz zum prozeduralen) Wissen befat. Dieses deklarative Wissen wird in Stzen formuliert. Die KI ver- langt daher nach einer Sprache, in der diese Stze auch darstell- bar sind. Weil die Sprachen (natrliche Sprachen wie Deutsch und Englisch), in denen diese Stze gewhnlich ausgedrckt sind, fr 8. Vorwort IX eine Computerreprsentation ungeeignet sind, mu man andere Spra- chen mit den bentigten Eigenschaften verwenden. Unserer Meinung nach wir es sich zeigen, da diese Eigenschaften mindestens auch dieselben sind, die die Logikern bei der Entwicklung formalisier- ter Sprachen wie dem Prdikatenkalkl intendierten. Unserer An- sicht nach mu daher jede Sprache, die in KI-Systemen bei der Wis- sensreprsentation Verwendung findet, mindestens auch die Aus- drucksstrke des Prdikatenkalkls besitzen. Wenn wir also zur Reprsentation von Wissen eine Sprache wie den Prdikatenkalkl verwenden, so mu die Theorie, die wir ber solche Systeme bilden, auch Teile der Beweistheorie und der logischen Modelltheorie enthalten. Unsere Ansichten sind in diesem Punkt sehr strikt: jeder, der ohne die Bercksichtigung der theoretischen Ergebnisse der Logiker versucht, einen theoretischen Be- schreibungsapparat fr Systeme aufzustellen, die deklarativ repr- sentiertes Wissen bentzen und manipulieren sollen, der luft Ge- fahr, (bestenfalls) die Arbeit der besten Kpfe noch einmal zu wiederholen, und (schlimmstenfalls) dieses falsch zu machen! Von diesen beiden Voraussetzungen ausgehend stellt das Buch in der Sprache und mit der Technik der Logik die zentralen Gebiete der KI dar. Dies sind die Wissensreprsentation (knowledge representation) , Schlufolgern (reasoning) , die Induktion (induction) als eine Form des Lernens und verschiedene Architekturen fr schlufolgernde, wahrnehmende und handelnde Agenten. Allerdings zeigen wir nicht die einzelnen Anwendungsmglichkeiten dieser Gebiete, wie beispielsweise in Expertensystemen (expert systems), bei der Verarbeitung natrlicher Sprache (natural language proces- sing) oder beim Bildverstehen (vision). Hierber gibt es spezielle Bcher. Unser Ziel ist es vielmehr, uns auf die all diesen Gebie- ten gemeinsamen und grundlegenden Gedanken zu konzentrieren. Als Reprsentationssprache fr das Wissen, das ein schlu- folgernder Agent ber seine Welt besitzt, schlagen wir den Prdi- 9. x Vorwort katenkalkl erster Stufe vor. Dabei gehen wir davon aus, da der Agent in einer Welt von Objekten, Funktionen und Relationen existiert, die die Basis fr ein Modell der Stze des Agenten im Pr- dikatenkalkl bilden. Als zentrale Inferenztechnik eines intelligenten Agenten stellen wir die deduktive Inferenz vor. Die Kapitel 1 bis 5 sind daher einer kurzen aber vollstndigen Darstellung der Syntax und Semantik des Prdikatenkalkls erster Stufe, der logischen Deduktion im allgemeinen und der Resolution im besonderen gewidmet. Der Stoff der Kapitel Ibis 5 und der Kapitel 11, 12 (der sich mit Schlufolgerungen ber Handlungen und Plne befat) gehrt heute schon zum klassischen Lehrgut der KI. Viele Aspekte aus den restlichen Kapiteln stammt aus der aktuellen Forschung. Wir haben dabei versucht, solche aktuellen Ergebnisse zusammenzustellen, von denen wir glauben, da sie in nchster Zeit ebenfalls zu den Klassikern gehren werden. Wir glauben, da unser Buch, das erste Lehrbuch ist, welches diese neuen Themen behandelt. Sie umfassen nicht-monotones Schlieen (nonmonotonic reasoning) , Induktion (induction) , Schlufolgern bei unsicheren Information (reasoning with uncertain information), Schlieen ber Wissen- und ber berzeugungen (reasoning about knowledge and belief), Reprsentation und Schlufolgern auf einer Metaebene (metalevel representation and reasoning) und Architekturen fr intelligente Agenten. Wir sind berzeugt, da die Dynamik und Entwicklung einer Wissenschaftsdis- ziplin durch einen frhen Einzug zentraler Gedanken aus den For- schungspapieren in die Lehrbcher vorangetrieben wird. Wir sind uns aber auch der Tatsache bewut (und der Leser sollte es auch sein), da man mit solch einer frhen bernahme auch Riskiken ein- geht. Wir sollten noch einiges dazu sagen, warum das Thema Suche (search) in diesem Buch nicht behandelt wird. Suchalgorithmen und -heuristiken zhlt man meist zu den Eckpfeilern der Kl. (Einer von 10. Vorwort XI uns unterstrich diesen Vorrang auch in einern frheren Buch). Wie der Titel es schon andeutet, soll das vorliegende Buch keine allgemeine Einfhrung in das gesamte Gebiet der KI darstellen. Eine Behandlung des Themas 'Suche' htte von dem Schwerpunkt Logik, den wir fr dieses Buch beibehalten wollten, weggefhrt. In jedem Fall ist das Thema Suche aber in anderen Bchern ber KI ausfhrlich behandelt. Das Buch setzt einige Kenntnisse ber Computerprogrammierung voraus, obwohl niemand programmieren knnen mu, um es mit Gewinn zu lesen. Wir setzen auch einige mathematische Kenntnisse voraus. Der ein wenig mit Wahrscheinlichkeitstheorie, Logik, lineare Alge- bra, Listennotation und Mengentheorie vertraute Leser wird es an einigen Stellen des Buches leichter haben als ein mit diesen The- men weniger vertrauter Leser. Die mit einern Stern (*) hinter der berschrift gekennzeichneten weiterfhrenden Abschnitte eines Kapitels knnen beim ersten Lesen bersprungen werden. Am Ende jedes Kapitels sind bungsaufgaben angefhrt. (Die Lsungen zu den bungen finden sich am Ende des Buches). Einige Themen sind nicht im Text selbst, sondern in den bungen dargestellt. Die meisten Aufgaben haben sich in Seminaren, welche die Autoren an der Uni- versitt Stanford hielten, bewhrt. Besonders der Leser, der das Buch zum Selbststudium verwendet, ist aufgefordert, die bungen zu bearbeiten. Selbst wenn der Leser die AufgabensteIlungen nicht durcharbeitet, so sollte er sich doch zumindest die von uns ausge- arbeiteten Musterlsungen anschauen. Er sollte sie als ergnzende Beispiele fr die im Buch behandelten Themen heranziehen. Am Ende eines jeden Kapitels stellen wir in einern Abschnitt "Literatur und historische Bemerkungen" die wichtigsten zitierten Quellen vor. Die angegebene Literatur ist am Ende des Buches zu- sammengestellt. Zusammen mit diesen Quellenangaben kann man die Kapitel 6 bis 10 und 13 als Einfhrung in die Literatur der weiterfhrenden Themen betrachten. 11. XII Vorwort In diesem Buch finden mindestens drei verschiedene Sprach- ebenen Verwendung. Wir haben uns bemht, einige typographische Re- geln streng einzuhalten, um es dem Leser zu erleichtern, die je- weils verwendete Sprachebene zu erkennen. Herkmmliche deutsche Stze sind in Prestige und zur besonderen Akzentuierung in Kursiv- schrift gedruckt. Stze des Prdikatenkalkls sind in einer schreibmaschinenhnlichen Type gesetzt. Mathematische Formeln und Gleichungen sind in einer kursiven Schrift gedruckt. Einige typographische Hinweise findet man auf Seite xix abgedruckt. Fr Verbesserungsvorschlge, Kommentare und Korrekturen sind die Autoren dankbar. Diese knnen direkt an sie oder an den Ver- leger gesandt werden. 12. XIII VORWORT DES BERSETZERS MIT DIESEM BUCH VERFOLGEN die Autoren zwei Anliegen: den Leser in die logischen Grundlagen der Knstlichen Intelligenz einzufhren und ihn mit der aktuellen Forschung bekannt zu machen. Beiden Aspekten versucht die bersetzung Rechnung zu tragen. Es wurden daher so wenig englische KI-Fachtermini wie mglich verwendet, um das Verstndnis zu erleichtern. Gleichzeitig sollte die Lektre der englischen Originalliteratur nicht durch deutsche Be- griffe erschwert werden, die nicht mehr mit den englischen Termini zu identifizieren sind. Nur sehr wenig KI-Literatur erscheint in Deutsch, aktuelle Forschungsergebnisse werden primr in Englisch verffentlicht. Auerdem gibt es fr die wenigsten KI-Fachbegriffe in der deutschen KI-Gemeinde einen Konsens fr eine bersetzung. Daher wurde ein Kompromi gewhlt: Beim erstmaligen Vorkommen wird ein Begriff in der deutschen bersetzung und in Englisch angefhrt. Konnte keine passende deutsche bersetzung gefunden werden, oder hatte sich der englische Begriff als terminus technicus eta- bliert, so wurde das englische Original belassen. Am Ende des Buches findet man einen Index der englischen Termini mit der ge- whlten deutschen bersetzung. Das Stichwort-Verzeichnis wurde gegenber dem Original berarbeitet und ergnzt. 13. xv INHALTSVERZEICHNIS Typographische Hinweise ........................................ xxi KAPITEL 1 1.1 Literatur und historische Bemerkungen..................... 8 bungen ......................................................... 12 KAPITEL 2 2.1 Konzeptua1isierung ....................................... 14 2.2 Der Prdikatenkalkl ..................................... 19 2.3 Semantik ................................................. 30 2.4 2.5 2.6 2.7 2.8 Ein Beispiel Ein Beispiel Beispiele aus Beispiele aus Beispiele aus aus aus der der der der Kltzchenwelt ....................... 39 der Welt der Schaltkreise ............... 41 Welt der Algebra ....................... 45 Welt der Listen ........................ 46 Welt der natrlichen Sprache ........... 48 2.9 Spezielle Sprachen....................................... 50 2.10 Literatur und historische Bemerkungen.................... 56 bungen ......................................................... 57 14. XVI Inhaltsverzeichnis KAPITEL 3 3.1 Ab1eitbarkeit ............................................ 63 3.2 Inferenzprozeduren....................................... 69 3.3 Logische Implikation..................................... 75 3.4 Beweisbarkeit ............................................ 78 3.5 Das Beweisen der Beweisbarkeit ........................... 83 3.6 Literatur und historische Bemerkungen.................... 87 bungen......................................................... 87 KAPITEL 4 4.1 Klauselform .............................................. 89 4.2 Unifikation.............................................. 90 4.3 Das Resolutionsprinzip ................................... 97 4.4 Resolution.............................................. 101 4. 5 Unerfllbarkeit ......................................... 106 4.6 Wahr/Falsch-Fragen...................................... 107 4.7 Einsetzungsfragen....................................... 109 4.8 Beispiele aus der Welt der Schaltkreise ................. 112 4.9 Beispiele aus der Welt der Mathematik................... 119 4.10 Konsistenz und Vollstndigkeit .......................... 120 4.11 Resolution und Gleichheit ............................... 127 4.12 Literatur und historische Bemerkungen................... 131 bungen ........................................................ 131 KAPITEL 5 5.1 Eliminationsstrategien.................................. 137 5.2 Die Unit-Reso1ution..................................... 139 5.3 Die Eingabe-Resolution .................................. 140 5.4 Lineare Resolution ...................................... 141 5.5 Sttzmengenresolution ................................... 143 5.6 Geordnete Resolution .................................... 145 15. Inhaltsverzeichnis XVII 5.7 Gerichtete Resolution................................... 146 5.8 Die sequentielle Erfllung von Randbedingungen.......... 153 5.9 Literatur und historische Bemerkungen................... 159 bungen....................... , ................................ 160 KAPITEL 6 6.1 Die Closed-World Annahme ................................ 167 6.2 Prdikatvervollstndigung............................... 174 6.3. Taxonomische Hierarchien und Default-Schlsse ........... 182 6.4 Die Zirkumskription..................................... 188 6.5 Allgemeinere Formen der Zirkumskription................. 208 6.6 Default-Theorien........................................ 214 6.7 Literatur und historische Bemerkungen................... 219 bungen ........................................................ 222 KAPITEL 7 7.1 Induktion ............................................... 226 7.2 Konzeptbildung .......................................... 232 7.3 Erzeugung von Experimenten.............................. 240 7.4 Literatur und historische Bemerkungen................... 245 bungen ........................................................ 247 KAPITEL 8 8.1 Die Wahrscheinlichkeit von Stzen....................... 250 8.2 Die Anwendung der Baye'schen Regel bei unsicheren Inferenzen................................... 254 8.3 Unsicheres Schliessen in Expertensystemen............... 264 8.4 Probabilistische Logik .................................. 271 8.5 Probabilistische Folger~ng ............... '" ............ 276 8.6 Berechnungen mit kleinen Matrizen....................... 283 8.7 Berechnungen mit grossen Matrizen....................... 288 16. XV" I Inhaltsverzeichnis 8.8 Bedingte Wahrschein1ichkeiten spezifischer Informationen ........................................... 291 8.9 Literatur und historische Bemerkungen................... 294 bungen ........................................................ 295 KAPITEL 9 9.1 9.2 9.3 9.4 9.5 9.6 9.7 9.8 9.9 9.10 9.11 9.12 9.13 Vorbemerkungen .......................................... 299 Die Aussagenlogik von berzeugungen ..................... 301 Beweismethoden.......................................... 306 Mehrfach eingebettete berzeugungen ..................... 310 Quantifikation in modalen Kontexten ..................... 313 Beweismethoden bei quantifizierten berzeugungen ........ 317 Zu wissen, was etwas ist ................................ 321 Logiken mglicher Welten ................................ 322 Die Eigenschaften von Wissen ............................ 326 Die Eigenschaften von berzeugungen ..................... 334 Das Wissen von Agentengruppen ........................... 335 Gleichheit, Quantifikation und Wissen ................... 339 Literatur und historische Bemerkungen ................... 342 bungen ........................................................ 344 KAPITEL 10 10.1 Metasprache ............................................. 349 10.2 Die Klauselform ......................................... 353 10.3 Resolutionsprinzip ...................................... 354 10.4 Inferenzprozeduren ...................................... 357 10.5 Ab1eitbarkeit und berzeugungen ......................... 360 10.6 Schlussfolgerungen auf Metaebenen ....................... 362 10.7 Parallele Schlussfolgerungen auf zwei Deduktionsebenen ........................................ 366 10.8 Reflektion ............................................. 372 10.9 Literatur ,und historische Bemerkungen ................... 380 bungen ........................................................ 381 17. InhaItsverzeichnis XIX KAPITEL 11 11.1 Zustnde ................................................ 383 11.2 Aktionen ................................................ 389 11. 3 Das Frame-Problem ....................................... 394 11.4 Die Reihenfolge von Aktionen ............................ 396 11.5 Konditiona1it .......................................... 399 11.6 Literatur und historische Bemerkungen................... 408 bungen ........................................................ 409 KAPITEL 12 12.1 Anfangszustnde ......................................... 414 12.2 Ziele ................................................... 415 12.3 Aktionen ................................................ 416 12.4 Plne ................................................... 419 12.5 Die Methode von Green ................................... 420 12.6 Aktionsblcke ........................................... 421 12.7 Bedingte Plne .......................................... 425 12.8 Planungsrichtung ........................................ 426 12.9 E1iminierung der unerreichbaren Planungsalternativen.................................... 429 12.10 Lineare Zustandsordung (State A1ignment) ................ 431 12.11 Die Unterdrckung von Frame-Axiomen..................... 432 12.12 Zielregression.......................................... 435 12.13 Zustandsdifferenzen..................................... 439 12.14 Literatur und historische Bemerkungen................... 443 bungen ........................................................ 445 KAPITEL 13 13.1 Tropistische Agenten .................................... 448 13.2 Hysteretische Agenten ................................... 454 13.3 Wissensorientierte Agenten .............................. 458 18. XX Inhaltsverzeichnis 13.4 Iterativ wissensorientierte Agenten..................... 464 13.5 Wiedergabetreue ., ....................................... 468 13.6 Bewut handelnde Agenten................... '" .......... 476 13.7 Literatur und historische Bemerkungen................... 479 bungen........................................................ 480 ANHANG A: Lsung der bungsaufgaben............................ 483 Literaturverzeichnis ........................................... 523 Verzeichnis der englischen Fachbegriffe ........................ 563 Stichwortverzeichnis ........................................... 567 19. XXI TYPOGRAPHISCHE HINWEISE (1) Objekte, Funktionen und Relationen (d.h. die Elemente einer Konzeptua1isierung) sind in kursiv gedruckt: Die Extension der Relation Auf ist die Menge {(a,b), (b, e) ,(d, e)}. (2) Ausdrcke und Teilausdrcke des Prdikatenkalkls sind in einer fetten, schreibmaschinenhnlichen Type gedruckt, wie (Ix ApfeI(x v (3x Pfirsich(x (3) Griechische Kleinbuchstaben dienen als Meta-Variablen fr Ausdrcke und Teilausdrcke des Prdikatenkalkls. Sie treten manchmal gemischt mit objektsprachlichen Ausdrcken des Pr- dikatenka1k1s auf: (4)(0:) v P(A) ==> 1/1) Dem besseren Verstndnis wegen verwenden wir, wie in dem folgenden Beispiel, kursive Grobuchstaben als Meta-Variablen fr Re1ationen- und Objektkonstanten Angenommen, wir haben eine Relationskonstante P und eine Obj ektkonstante A, so da P (A) ==> P / Q(B). 20. XXII Typographische Hinweise (4) Griechische Grobuchstaben bezeichnen Menge'n von Formeln des Prdikatenkalkls, wie: Gibt es einen Beweis des Satzes ~ aus einer Prmissen- menge A und den logischen Axiomen mithilfe des Modus Ponens, so sagt man, ~ sei beweisbar aus A(geschrieben als A I- ~). Da Klauseln Mengen von Literalen sind, verwenden wir griechische Grobuchstaben auch als Variablen fr Klauselmengen: Angenommen, ~ und ~ seien zwei standardisierte Klauseln. (5) Fr meta-logische Formeln ber Aussagen des Prdikatenkalkls verwenden wir den normalen mathematischen (keinen schreibmaschinenhnlichen) Schriftsatz: Falls ~ eine Objektkonstante ist, so gilt ~IEIII. Manchmal enthalten meta-logische Formeln auch Ausdrcke des Prdikatenkalkls: (6) Wir bentzen groe Schreibschriftbuchstaben ~ zur Bezeichnung einer "Theorie" im Prdikatenkalkl. (7) Algorithmen und Programme sind in einer schreibmaschinenhnlichen Type gedruckt: Procedure Resolution (Ganma) Repeat Termination(Ganma) ==> Return(Success), End Phi und'" hat die Eigen- schaft, da, es dann eine Substitution 0 mit der Eigenschaft gibt. Eine wichtige Eigenschaft des allgemeinsten Unifikators ist, da er bis auf eine Umbenennung der Variablen eindeutig ist. Die Substitution {xlA} ist fr die Ausdrcke P(A,y,z) und P(x,y,z) der allgemeinste Unifikator. Einen weniger allgemeinen Unifikator {xlA, ylB, z/C} erhlt man durch die Komposition des allgemeinsten 116. 96 4 Resolution Recursive Procedur Mgu (x,y) Begin End x=y ==> Return(), Variable(x) ==> Return(Mguvar(x,y, Variable(y) ==> Return(Mguvar(y,x, Constant(x) or Constant(y) ==> Return(False) Not(Length(x)=Length(y ==> Return(False) Begin i und '11 seien zwei Klauseln. Wenn es nun ein Literal ~ in 4> und ein Literal ,W in '11 gibt, so da ~ und Weinen allgemeinsten Unifikator 0 besitzen, so knnen wir diejenige Klau- sel ableiten, die aus der Anwendung der Substitution 0 auf die Vereinigung von 4> und '11 abzglich der komplementren Literale entsteht. 4> mit ~ E 4> '11 mit ,W E '11 ((4> - {~})u(4) - {,W}o, wobei ~o = Wo Die folgende Deduktion zeigt den Einsatz der Unifikation bei der Anwendung der Resolutionsregel. In diesem Beispiel unifiziert das erste Disjunkt des ersten Satzes mit der Negation des ersten Disjunkts des zweiten Satzes durch den allgemeinsten Unifikator {xlA} . l. 2. 3. {P(x), Q(x, y)} {,P(A), H(B, z)} {Q(A,y),H(B,z)} A A 1, 2 Wenn zwei Klauseln resolvieren, so knnen sie mehr als eine Re- 120. 100 4 Resolution solvente besitzen, denn es kann ja mehrere Mglichkeiten geben, ~ und ~ zu whlen. Als Beispiel betrachten wir hierzu die folgende Deduktion. Im ersten Fall ist ~ = P(x,x) und ~ = P(A,z) und der allgemeinste Unifikator ist {xlA} , {z/A}. Im zweiten Fall ist ~ = Q(x) und ~ = Q(B) und der allgemeinste Unifikator ist {xIB} . Glcklicherweise knnen zwei Klauseln aber hchstens endlich viele Resolventen besitzen. l. {P(x,x),Q(x),R(x)} A 2. {,P(A, z), ,Q(B)} A 3. {Q(A), R(A), ,Q(B)} 1, 2 4. {P(B, B), R(B), ,P(A, z)} 1, 2 Leider reicht diese Definition immer noch nicht aus. Sind uns nmlich die Klauseln {P(u),P(v)} und {,P(x),,(y)} gegeben, so sollten wir auch in der Lage sein, die leere Klausel, d.h. einen Widerspruch abzuleiten. Mit unserer vorangegangenen Definition ist dies aber unmglich. Durch eine kleine nderung in unserer Defini- tion knnen wir dies allerdings beheben. Besitzt eine Teilmenge von Literalen einer Klausel ~ einen allgemeinsten Unifikator~, so nennt man diejenige Klausel ~', die durch Anwendung von ~ auf ~ entsteht, einen Faktor von ~. Bei- spielsweise haben die Literale P(x) und P(F(y den allgemeinsten Unifikator {xIF(y)} , so da die Klausel {P(F(y,R(F(y),y} ein Faktor von {P(x),P(F(y,R(x,y)} ist. Natrlich ist jede Klausel ein trivialer Faktor von sich selbst. Mit dem Begriff des Faktors knnen wir nun unsere endgltige Definition des Resolutionsprinzips formulieren. Angenommen, ~ und ~ seien zwei Klauseln. Kommt in einem Faktor ~' von ~ ein Literal ~ vor und in einem Faktor ~' von ~ ein Literal ,~ vor, so da ~ und ~ den allgemeinsten Unifikator r besitzen, dann sagen wir, da die beiden Klauseln ~ und ~ miteinander resolvieren und die neue Klausel ~I - {~} u (~' - {'~}r eine Resolvente der beiden Klauseln sei. 121. 4 Resolution 101 ~ mit ~ E ~' I}I mit ,I/l E I}I' ( (~' - {~}) u (~' - (, I/l}))l' , wobei h = I/ll' Die Standardisierung von Variablen knnen wir nun als eine triviale Anwendung der Faktorisierung auffassen. Inbesondere erlaubt uns unsere Definition, die Variablen in einer Klausel umzu- benennen, damit keine Probleme mit den Variablen anderer Klauseln entstehen knnen. Die Situationen, in denen nicht-triviale Fak- toren auftreten, sind in der Praxis extrem selten und keine der Klauseln in unseren Beispielen enthalten nicht-triviale Faktoren. Daher vernachlssigen wir, mit Ausnahme der Umbenennung von Varia- blen, im weiteren Verlauf unseren Betrachtungen die Faktoren. 4.4 RESOLUTION Eine Resolutionsableitung einer Klausel ~ aus einer Datenbasis ~ ist eine Klauselfolge , bei der (1) ~ ein Element der Folge ist, und (2) jedes Element entweder ein Element von ~ ist oder durch die Anwendung des Resolutionsprinzips aus Klauseln, die frher in der Folge vorkommen, entstanden ist. Die nachstehende Klauselfolge ist beispielsweise eine Resolu- tionsableitung der leeren Klausel aus der mit ~ bezeichneten Klauselmenge . Die Klausel in Zeile 5 ist aus den Klauseln der Zeilen 1 und 2 abgeleitet. Die Klausel in Zeile 6 ist aus Klauseln der Zeilen 3 und 4 entstanden, und die Konklusion (Zeile 7) ist durch Resolution dieser beiden Konklusionen (Zeile 5 und 6) abgeleitet worden. 1. {P} 2. {,P,Q} 3. {,Q,R} 4. {,R} 122. 102 4 Resolution Procedure Resolution (Delta) Repeat End Termination(Delta) ==> Return(Success) Phi ein Computerprogramm verbinden, das im end- lichen Bereich der Anwendungsdomne des Programmes Zahlen ver- gleicht. Nennen wir dieses Programm Grerp. Wir sagen nun, das Programm Grerp sei dem Prdikatensymbol > zugewiesen (engl. attached to). In dieser Hinsicht knnen wir auch die sprachlichen Symbole 7 und 3 (d.h. die Ziffern) mit den Datenobjekten 7 und 3 des Computers verknpfen. Wir sagen dann, da die Zahl 7 dem Datenobj ekt 7 zugewiesen und die Zahl 3 dem Obj ekt 3 zugewiesen sind und da das Computerprogramm und die von Grerp(7,3) repr- sentierten Argumente dem sprachlichen Ausdruck 7>3 zugewiesen seien. Jetzt knnen wir das Programm laufen lassen, um festzu- stellen, da 7 wirklich grer ist als 3. Auf diese Weise knnen wir auch den Funktionssymbolen Proze- duren zuweisen. Beispielsweise kann dem Funktionssymbol + ein Ad- ditionsprogramm zugewiesen werden. Auf diese Weise knnen wir eine Verknpfung oder eine prozedurale Zuweisung zwischen dem ausfhr- barem Computercode und einigen sprachlichen Ausdrcken unseres Prdikatenkalkls herstellen. Die Auswertung der zugewiesenen Pro- zeduren kann man sich dabei als einen Interpretationsproze bezglich eines partiellen Modells denken. Mit prozeduralen Auswer- tungen kann man den Suchaufwand, der anderenfalls fr den Beweis von Theoremen bentigt wrde, eventuell reduzieren. Ein Literal wird ausgewertet, wenn es zur Laufzeit der zuge- 126. 106 4 Resolution wiesenen Prozeduren interpretiert wird. Normalerweise lassen sich zwar nicht alle Literale einer Klauselmenge auswerten, die K1au- se1menge vereinfacht sich aber. Erweist sich ein Litera1 als falsch, so kann dieses Litera1 aus der Klauselmenge entfernt werden. Erweist sich allerdings ein Litera1 als wahr, so kann die gesamte Klausel entfernt werden, ohne da die Unerfllbarkeit der Rest- menge davon betroffen wre. Die Klausel {P(x),Q(x),73 ist wahr. Die Zuweisung von sprachlichen Objekten zu semantischen Elementen ist ein wichtiges Prinzip in der KI und hat einen weiten Anwendungsbereich. 4.5 UNERFLLBARKEIT Der einfachste Anwendungfall der Resolution ist der Nachweis der Unerfllbarkeit. Ist eine Klauselmenge unerfllbar, so lt sich aus ihr mit der Resolution immer ein Widerspruch ableiten. In der Klauselform stellt sich ein Widerspruch in Form der leeren Klausel dar, die quivalent zu einer Disjunktion ohne Literale ist. Alles was wir deshalb tun mssen, um den Nachweis der Unerfllbarkeit zu automatisieren, ist, die Resolution zum Testen aller Konsequenzen der zu prfenden Menge zu verwenden und genau dann aufzuhren, wenn die leere Klausel erzeugt wurde. Die in Abschnitt 4.4. beschriebene Ableitung ist ein gutes Bei- spiel fr die Anwendung der Resolution bei der Bestimmung von Un- erfllbarkeit. Da die Resolutionen die leere Klausel erzeugen, ist die Ausgangsmenge unerfllbar. Den Nachweis der Unerfllbarkeit einer Klauselmenge kann man auch bentzen, um zu zeigen, da eine Formel von einer Formel- menge logisch impliziert wird. Angenommen, wir wollten zeigen, da die Formelmenge ~ die Formel Wlogisch impliziert. Wir knnen dies 127. 4 Resolution 107 dadurch erreichen, da wir fr ~ aus einen Beweis finden, d.h. da wir zeigen, da I-~. Mit dem Widerlegungstheorem (Kapitel 3), knnen wir durch den Nachweis, da u {,~} inkonsistent (unerfllbar) ist, zeigen, da I- ~. Wenn wir also gezeigt haben, da die Formelmenge u {,~} unerfllbar ist, so haben wir damit auch gezeigt, da logisch ~ impliziert. Betrachten wir diese Technik einmal vom modelltheoretischen Standpunkt. Falls F~, so sind alle Modelle von auch Modelle von ~. Daher kann keines davon ein Modell von ,~ sein und deshalb ist u ,~ unerfllbar. Nehmen wir umgekehrt einmal an, u ,~ sei unerfllbar, aber sei erfllbar. I sei eine Interpretation, die erfllt. I erfllt nicht ,~, denn wenn es dies tte, wre u ,~ erfllbar. Daher erfllt I~. (Eine Interpretation mu entweder ~ oder ,~ erfllen). Weil dies fr ein beliebiges I gilt, gilt es auch fr alle I, die erfllen. Deshalb sind alle Modelle von auch Modelle von ~, und daher impliziert logisch ~. Fr die Anwendung dieser Technik - die logische Implikation ber den Nachweis der Unerfllbarkeit nachzuweisen - haben wir zuerst ~ negiert und es dann zu addiert, was uns zu ' fhrte. Danach haben wir ' in die Klauselform berfhrt und die Resolu- tion angewendet. Wurde dabei die leere Klausel erzeugt, so war das Original ' unerfllbar, und wir hatten damit gezeigt, da ~ logisch impliziert. Diese Methode nennt man Resolutionswiderlegung (eng1. resolution refutation). In den nchsten Abschnitten werden wir sie noch durch weitere Beispiele erlutern. 4.6 WAHR/FALSCH-FRAGEN Eines der Anwendungsgebiete fr den Beweis der logischen Implika- tion durch die Resolutionswiderlegung ist die Beantwortung von Wahr/Falsch-Fragen. Als Beispiel betrachten wir die folgenden Re- solutionsspur. Unsere Datenbasis enthlt die Fakten, da Artur der 128. 108 4 Resolution Vater von Johann, da Robert der Vater von Isabell ist, und da Vter ein Elterteil sind. Um zu beweisen, da Artur ein Elternteil von Johann ist, negieren wir die entsprechende Formel und erhalten die Klausel 4, die besagt, da Artur kein Elternteil von Johann ist. Das r gibt an, da die entsprechende Klausel aus der Negation der zu beweisenden Formel abgeleitet wurde. Wie im vorherigen Bei- spiel steht t:. dafr, da die entsprechende Klausel in der Aus- gangsdatenbasis enthalten ist. l. {V(Artur, Johann)} t:. 2. {V(Roberl,Isabell)} t:. 3. {,V(x,y),E(x,y)} t:. 4. { ,E(Artur, Johann)} r 5. {E(Artur, Johann)} 1, 3 6. {E(Robert, Isabell)} 2, 3 7. {,V(Artur, Johann)} 3, 4 8. 0 4, 5 9. 0 1, 7 Oft nennt man die zu beweisende Formel Ziel (engl. goal) und die Klauseln, aus deren Negation das Ergebnis entsteht, Ziel-Klau- seIn. Im vorigen Beispiel gab es nur eine einzige Ziel-Klausel. Die Negation und die anschlieende Umwandlung komplizierterer Fra- gen in die Klauselform kann aber auch zu mehreren Ziel-Klauseln fhren, die dann alle der Datenbasis hinzugefgt werden mssen. In einigen Fllen mu man nur einige oder sogar auch alle dieser Ziel-Klauseln zur Ableitung des Ergebnisses bentzen. Nehmen wir zum Beispiel an, wir wten nichts ber Artur oder ber Johann und wir wollten die einfache Tautologie beweisen, da Artur entweder der Vater von Johann ist oder dies nicht ist. Das Ziel ist also die Disjunktion V(Arlur,Johann) v ,V(Arlur,Johann). Die Negation dieses Satzes und deren Addition zu der Klauselmenge fhrt uns zu der nachfolgenden Resolutionsspur. Die zwei Klauseln knnen wir direkt miteinander resolvieren, um die leere Klausel zu erzeugen und damit das Ergebnis zu beweisen. 129. 4 Resolution 109 1. {.,V(Artur. Johann) } r 2. {V(Artur. Johann) } r 3. {} 1, 2 Auer der Beantwortung von Wahr/Falsch-Fragen ber den Inhalt von Datenbasen kann man die Resolution auch zum Beweis mathema- tischer Theoreme und der Korrektheit von Computerprogrammen bentzen. Beispiele hierzu finden Sie in Abschnitt 4.9. und in den bungen. 4.7 ENSETZUNGSFRAGEN In Abschnitt 4.6. sahen wir, wie man die Resolution zur Beant- wortung von Wahr/Falsch-Fragen (zum Beispiel Ist Artur einer der Eltern von Johann?) verwenden kann. In diesem Abschnitt zeigen wir, wie man die Resolution auch zur Beantwortung von Einsetzungs- fragen (eng1. fill-in-the-blank questions) (wie zum Beispiel Wer ist ein Elternteil von Johann?) bentzen kann. Eine Einsetzungsfrage ist ein Satz des Prdikatenkalkls, der freie Variablen enthlt, die die zu fllenden Leerstellen angeben. Die Aufgabe besteht nun darin, solche Bindungen fr die freien Variablen zu finden, da die Datenbasis denjengen Satz logisch impliziert, den man durch Einsetzen der Bindungen in den Original- satz erhlt. Um nach den Elternteilen von Johann zu fragen, wrde man beispielsweise die Frage P(x.Johann) formulieren. Mit der Da- tenbasis aus dem vorherigen Abschnitt sehen wir, da die Antwort auf diese Frage Artur ist, denn der Satz P(Artur.Johann) wird logisch durch diese Datenbasis impliziert. Ein Antwortliteral fr eine Einsetzungsfrage ~ ist ein Term der Form Ans(v ...v ), wobei v , ... ,v in ~ frei vorkommende Vari- 1 n 1 n ab1en sind. Zur Beantwortung von ~ bilden wir eine Disjunktion aus der Negation von ~ und des Antwortliterals und berfhren sie in 130. 110 4 Resolution die Klauselform. Zum Beispiel kombinieren wir die Negation von P(x,Johann) mit dem Antwortliteral Ans(x) , um die Disjunktion ,P(x,Johann) v Ans(x) Ans(x)} ergibt. zu .bilden, was die Klausel {,P(x,Johann), Die Resolution wenden wir wie in Abschnitt 4.4. beschrieben an, bentzen jetzt aber eine andere Abbruchbedingung. Anstatt zu war- ten bis die leere Klausel erzeugt wurde, stoppen wir die Prozedur, sobald sie eine Klausel abgeleitet hat, die nur ein Antwortliteral enthlt. Die folgende Resolutionsspur zeigt, wie wir die Antwort auf Wer ist Johanns Vater? berechnen. 1. {V(Artur, Johann)} /). 2. {V(Robert, IsabeU)} /). 3. {,V(x,y),E(x,y)} /). 4. {,E(z, Johann) , Ans(z)} r 5. {E(Artur, Johann)} 1, 3 6. {E(Robert, Isabell)} 2, 3 7. {, V(w, Johann) , Ans(w)} 3, 4 8. {Ans(Artur)} 4, 5 9. {Ans(Artur)} 1, 7 Wenn die Prozedur nur ein Antwortlitera1 erzeugt, dann sind die darin vorkommenden Terme die einzige Antwort auf die Frage. In einigen Fllen hngt das Ergebnis der Einsetzungsresolution von der Widerlegung ab, durch die es erzeugt wurde. Im allgemeinen knnen zu ein und derselben Frage verschiedene Widerlegungen entstehen. In einigen Fllen, wie in diesem hier, sind die Antworten dieselben, in anderen Fllen sind sie verschieden. Nehmen wir zum Beispiel an, wir wrden die Identitten sowohl des Vaters als auch der Mutter von Johann kennen und wir fragten Wer ist einer von Johanns Eltern? Die folgende Resolutionsspur zeigt, wie wir zwei Antworten zu dieser Frage ableiten knnen. 1. {V(Artur,Johann)} 2. {K(Ann,Johann)} 131. 4 Resolution 111 3. {.,V(x, y),E(x,y)} fl 4. {.,X(u, v),E(u, v)} fl 5. { .,E(z, Johann) , Ans(z)} r 6. {E(Artur, Johannann)} I, 3 7. {E(Ann, Johann) } 2, 4 8. (.,V(s,Johann), Ans(s)} 3, 5 9. ( .,X( t, Johann) , Ans(t)} 4, 5 10. (Ans(Artur)} 5, 6 11. (Ans(Ann)} 5, 7 10. (Ans(Artur)} I, 8 11. {Ans(Ann)} 2, 9 Leider knnen wir aber nicht feststellen, ob die in der Wider- legung erzeugten Antworten auch alle Mglichkeiten ausschpfen oder dies nicht tun. Wir knnen die Suche immer weiter fortsetzen, bis wir gengend Antworten gefunden haben. Wegen der Unentscheid- barkeit der logischen Implikation knnen wir aber trotzdem nicht allgemein wissen, ob wir auch alle mglichen Antworten gefunden haben. Ein anderer interessanter Aspekt der Einsetzungsresolution ist, da in einigen Fllen die Prozedur eine Klausel liefern kann, die mehr als ein Antwortliteral enthlt. Dies bedeutet dann, da zwar die Richtigkeit der einzelnen Antworten nicht garantiert ist, eine der Antworten aber korrekt sein mu. Die folgende Resolutionsspur verdeutlicht dies. Die Datenbasis enthlt in diesem Falle die Disjunktion, da entweder Artur oder Robert der Vater von Johann ist. Wir wissen aber nicht, welcher Mann es ist. Das Ziel ist nun, den Vater von Johann zu bestimmen. Durch die Resolution der Ziel-Klausel mit der Disjunktion aus der Datenbasis erhalten wir eine Klausel, die wiederum mit der Ziel- Klausel resolviert uns zwei Antwortliterale liefert. 1. (F(Artur, Johann) ,F(Robert, Johann)} 2. (.,F(x,Johann),Ans(x)} 132. 112 4 Resolution 3. {F(Robert,Johann),Ans(Artur)} 1, 2 4. {Ans(Artur),Ans(Robert)} 2, 3 In solchen Situationen knnen wir die Suche in der Hoffung fortsetzen, eine przisiere Antwort zu finden. Allerdings knnen wir wieder wegen der Unentscheidbarkeit der logischen Implikation nicht allgemein wissen, ob wir aufhren sollen oder ob wir sagen knnen, da es keine weiteren Antworten mehr gibt. 4.8 BEISPIELE AUS DER WELT DER SCHALTKREISE Einer der Vorteile bei der Beschreibung eines Schaltkreises mithilfe des Prdikatenkalkls ist der Einsatz automatisierter Deduk- tionsprozeduren wie der Resolution, um auf verschiedenste Arten ber Schaltkreise zu schlufolgern. Wir knnen beispielsweise das Verhalten eines Schaltkreises bei gegebenen Eingabewerten simulieren, wir knnen dessen Fehler diagnostizieren oder wir knnen Tests entwickeln, die gewhrleisten, da er korrekt arbeitet. Der erste Schritt bei der Durchfhrung einer dieser Aufgaben ist, die Umwandlung der Beschreibung des Schaltkreises in die Klauselform. Betrachten wir den in Abb.2.3. dargestellten Schalt- kreis. Die strukturelle Beschreibung des Schaltkreises lt sich leicht umwandeln, weil die Stze alle atomar sind. 1. {Xorg(Xl)} 2. {Xorg(X2)} 3. {Andg(Al)} 4. {Andg(A2)} 5. {Org(Ot)} 6. {Verbindg(EC1,Fl),EC1,X1)} 7. {Verbindg(E(2,Fl),E(2,X1)} 8. {Verbindg(EC1,Fl),E(l,A1)} 133. 4 Resolution 113 9. {Verbindg(E(2,Fl),E(2,Al} 10. {Verbindg(E(3,Fl),E(2,X2} 11. {Verbindg(E(3,Fl),E(1,A2} 12. {Verbindg(A(1,Xl),E(1,X2} 13. {Verbindg(A(1,Xl),E(2,A2} 14. {Verbindg(O(l,A2),E(l,Ol} 15. {Verbindg(O(1,Al),E(2,Ol} 16. {Verbindg(O(1, X2), A(1, Fl} 17. {Verbindg(O(1,Ol),A(2,Fl} Fr jeden Satz dieser Beschreibung existiert eine Klausel, da sich das Verhalten jeder einzelnen Komponente durch eine einfache Implikation beschreiben lt. Die Funktion (mit Namen) I bildet eine positive ganze Zahl und ein Gert auf den entsprechenden Ein- gang und die Funktion 0 bildet eine positive ganze Zahl und ein Gert auf den Ausgang des Gerts ab. Auerdem ist fr einen Ein- oder Ausgang und ein Signal die Relation V genau dann wahr, wenn der angegebene Ein- oder Ausgang dieses Signal trgt. 18. {,Andg(d), ,V(E(1, d), 1), ,V(E(2, d), 1), V(A(l, d), 1)} 19. {,Ang(d)"V(E(n,d),O), V(A(1,d),O)} 20. {,Org(d)"V(E(n,d),O), V(A(1,d), I)} 21. {,Org(d)"V(E(1,d),O)"V(E(2,d),O), V(A(1,d),O)} 22. {,Xorg(d), ,V(E( 1, d), y), ,V(E(2, d), z), y=z, V(A(1,d), I)} 23. {,Xorg(d)"V(E(1,d),z)"V(E(2,d),z), V(A(1,d),O)} 24. {,Verbindg(x,y)"V(x,z), V(y,z)} Wir mssen auch noch die Tatsache ausdrcken, da die zwei mglichen digitalen Werte nicht untereinander gleich sein knnen. Gbe es eine sehr viele oder gar unendliche viele mgliche Werte, so wrden wir dies durch eine prozedurale Auswertung lsen. Da hier aber nur zwei Werte vorliegen, so reichen die folgenden Klauseln aus. 25. {h~O} 26. {0*1} 134. 114 4 Resolution Von diesen Fakten ber den Schaltkreis ausgehend, knnen wir nun mit der Resolution dessen Verhalten simulieren. Wie man dies macht, wird im folgenden Resolutionsbeweis gezeigt. Die Stze der ersten drei Zeilen besagen, da die Eingabewerte des Schaltkreises I, 0 und 1 sind. Die Konklusion am Ende des Beweises sagt aus, da die Ausgabewerte des Gerts 0 und 1 sind. Al. {V(EU,FI),I)} A A2. {V(E(2,Fl),O)} A A3. {V(E(3,Fl),l)} A A4. {.,V(E(l,F1),z), V(EU, XI) , z)} 6, 24 AS. {V(EU, XI),l)} Al, A4 A6. {.,V(E(2, Fl),z), V(E(2, XI) ,z)} 7, 24 A7. {V(E(2, XI), O)} A2, A6 AB. {.,V(EU, X1), y), .,V(E(2, X1), z), y=z, I, 22 V(AU, XI),I)} A9. {.,V(E(2, X1), z), l=z, V(A(1, X1) ,1)} AS, AB AlO. {l=O, V(A(1,XI),l} A7, A9 All. {V(AU, X1), 1)} 2S, AlO A12. {.,V(AU,XI) ,z), V(E(1, X2), z)} 12, 24 AB. {V(EU, X2), I)} All, A12 A14. {.,V(E(3,Fl),z), V(E(1,X2),z)} 10, 24 AIS. {V(E(2,X2),1)} A3, A14 A16. {.,V(E(l, X2), z), .,V(E(2, X2), z), A2, 23 V(AU, X2), O)} A17. {.,V(E(2, X2),I), V(A(1, X2), O)} AB, A16 AlB. {V(AU,X2),O)} AlS, A17 A19. {.,V(E(3, FI), z), V(E(1, A2), z)} 11, 24 A20. {V(E(1, A2), I)} A3, A19 A2l. {.,V(A(1, X1), z), V(I, 2, A2), z)} 13, 24 A22. {V(E(2,A2),I)} All, A21 A23. {.,V(E(1, A2), 1), .,V(E(2, A2) ,I), 4, 1B V(A{1, A2), I)} A24. {.,V(E(2, A2), 1), V(A{1, A2), I)} A20, A23 135. 4 Resolution 115 A25. {V(A(1, A2), 1)} A22, A24 A26. {,V(A(1,A2),z), V(E(1,01),z)} 14, 24 A27. {V(E(1, 01), 1)} A25, A26 A28. {,V(E(n, 01),1), V(A(1, 01), 1)} 5, 20 A29. {V(A(1, 01),1)} A27, A28 A30. {,V(A(1, X2), z), V(A(l, Fl), z)} 16, 24 A3I. {V(A(1, Fl), O)} A18, A30 A32. {,V(A(1, 01), z), V(A(2, Fl), z)} 17, 24 A33. {V(A(2, F1), 1)} A29, A32 Wir knnen aber auch die Fehler der Komponenten des Scha1t- kreises diagnostizieren. In unserem Beispiel wollen wir einmal annehmen, da der ersten Ausgabwert des Schaltkreises eine 1 statt einer 0 sei. Irgendein Bauteil mu daher fehlerhaft sein. Entweder arbeitet ein Gatter nicht korrekt oder eine Verbindung ist falsch gelegt. Einfachheitshalber wollen wir annehmen, da alle Verbin- dungen fehlerfrei seien. Um Widersprche zu vermeiden, mssen die Typaussagen ber die Komponenten aus der Wissensbasis entfernt werden. Wenn wir von einer Aussage ber das Symptom (der Negation des eigentlich erwarteten Verhaltens) ausgehen, so knnen wir, wie nachstehend gezeigt, die Menge der verdchtigen Komponenten ableiten. B17 besagt somit, da entweder Xl oder X2 nicht wie ein XOR-Gatter arbeitet, d.h. mindestens eines von beiden ist also defekt. BI. {,V(A(1, Fl), O)} l!.. B2. {,Verbindg(x,A(1,Fl,.,V(x,O)} B1, 24 B3. {,V(A(1, X2), O)} 16, B2 B4. {,Xorg(X2), 0), ,V(E(1, X2), z), ,V(E(2, X2), z)} 23, B3 B 5. {,Xorg(X2), ,Verbindg(x, E(1, X2, 24, B4 ,V(x, z), ,V(E(2, X2), z)} B 6. {,V(Xorg(x2), ,V(A(1, X1), z), ,V(E(2, X2), z)} 12, B5 B 7. {,Xorg(X2), ,Xorg(Xl), ,V(E(1, X1), u), 22, B6 ,V(E(2, X1), v), lFV, ,V(E(2, X2) ,1)} B 8. {,Xorg(X2), ,Xorg(Xl), ,Verbindg(x, E( 1, Xl, 24, B7 136. 116 4 Resolution ,V(x, U) "V(E(2,XU, V), U=V, ,V(E(2, X2) ,l)} B 9. {,Xorg(X2),,Xorg(X1), ,V(E(1, F1), u), 6, B8 ,V(E(2,X1), V), U=V, ,V(E(2, X2) ,1)} BlO. {,Xorg(X2), ,Xorg(X1), ,V(E(2, Xl), v), Al, B9 1=v"V(E(2,X2),l)} Bll. {,Xorg(X2), ,Xorg(X1), ,Verbindg(x,E(2,Xl, 24, BlO ,V(x,v),l=v"V(E(2,X2),l)} Bl2. {,Xorg(X2)"Xorg(X1) "V(E(2, Fl), V), 7, B11 1=v"V(E(2,X2),l)} B13. {,Xorg(X2), ,Xorg(X1) ,1=0, A2, Bl2 ,V(E(2,X2),l)} B14. {,Xorg(X2), ,Xorg(Xl), ,V(E(2, X2) ,1)} 2S, B13 BlS. {,Xorg(X2), ,Xorg(Xl)" Verbindg(x, E(2, X2, 24, B14 ,V(x,l)} B16. {,Xorg(X2),,Xorg(Xl), ,V(E(3, Fl) ,1)} 10, B1S Bl7. {,Xorg(X2), ,Xorg(X1)} A3, B16 Bei der Diagnose digitaler Hardware nimmt man im allgemeinen an, da zu jedem Zeitpunkt ein Gert mindestens eine fehlerhafte Komponente enthlt. Die folgenden Klauseln sind eine zwar einfache, aber auch umstndliche Codierung dieser Annahme. Cl. {Xorg(Xl),Xorg(X2)} C2. {Xorg(Xl),Andg(Al)} C3. {Xorg(Xl), Andg(A2)} C4. {Xorg(Xl),Org(Ol)} CS. {Xorg(X2),And(Al)} C6. {Xorg(X2),Andg(A2)} C7. {Xorg(X2),Org(Ol)} C8. {Andg(Al),Andg(A2)} C9. {Andg(Al),Org(Ol)} C10. {Andg(A2), Org(01)} Unter der Voraussetzung, da mindestens ein Fehler vorliegt, und da ein Fehler garantiert in einer der Teilkomponente auf- 137. 4 Resolution 117 tritt, knnen wir diejenigen Teile aussondern, die nicht in dieser Teilmenge enthalten sind. Wissen wir zum Beispiel, die Aussage von B17, da entweder Xl oder X2 defekt ist, so knnen wir dann beweisen, da die Komponenten Al, A2 und 01 fehlerfrei sind. Die folgenden Klauseln zeigen, wie man dies beweisen kann. C11. {,Xorg(Xl)"Xorg(X2)} A C12. {Andg(Al), ,Xorg( X2)} C2, C11 Cl3. {Andg(Al)} CS, C12 C14. {Andg(A2), ,Xorg(X2)} C3, C11 C1S. {Andg(A2)} C6, C14 C16. {Org(Ol), ,Xorg(X2)} C4, C11 C17. {Org(Ol)} C7, C16 Und schlielich knnen wir auch noch Tests angeben, um mglicherweise fehlerhafte Teile einzugrenzen. Mit der Regel ber das Verhalten einer kritischen Komponente knnen wir eine Prognose des Verhaltens des Gesamtgertes ableiten, die dann die Teilmenge der verdchtigen Teile impliziert. Beispielsweise besagt Klausel 018, da das Signal am zweiten Ausgang des Gertes 1 sein mu, falls wir die gleichen Eingabewerte wie im vorherigen Beispiel verwenden und falls Xl ein XOR-Gatter ist. Diese Konklusion kannnun dazu be- ntzt werden, die verdchtigen Teile auszusondern. Die Eingabe- werte stellen wir wie oben ein und beobachten den Ausgabewert . Falls dieser nicht wie vorausgesagt 1 ist, so liegt dies an einer falschen Annahme. Die einzige Annahme, die wir vorausgesetzt hatten, war, da Xl korrekt arbeite. Da dies aber nicht beobachtet wurde, ist Xl also defekt. Dl. {,Xorg(Xl), ,V(E(1, Xl), y), 22 ,V(E(2,Xl),z),y=z,V(A(1,Xl),1)} D2. {,Xorg(Xl), ,V(E( 1, Xl), l), 2S, Dl ,V(E(2,Xl),0),V(A(1,Xl),1)} 03. {,Xorg(Xl), ,Verbindg(x, E(1, Xl), 24, 02 ,V(x,1)"V(E(2,Xl),0),V(A(1,Xl,1)} 04. {,Xorg(Xl), ,V(E(1, Fl), l), 6, D3 138. 118 4 Resolution ,V(E(2,Xl),O),V(A(I,Xl),l)} DS. {,Xorg(XI), ,V(E(1, Fl),I), 24, D4 ,Verbindg(x, E(2, Xl, ,V(x,O), V(ACl, XI), I)} D6. {,Xorg(XI), ,V(E(l, FI), 1), 7, DS ,V(E(2,Fl),0),V(A(1,Xl),I)} D7. {,Xorg(XI), ,V(E(1, Fl), 1), 24, D6 ,V(E(2, Fl), 0), ,Verbindg(A(1, X1), y), V(y,l)} D8. {,Xorg(X1), ,V(E(1, Fl), 1), 13, D7 ,V(E(2,Fl),0),V(E(2,A2),1)} D9. {,Xorg(X1), ,V(E(Fl), 1), 18, D8 ,V(E(2, F1), 0), ,Andg(Al), ,V(E(I,A2),I),V(A(I,A2),I)} D10. {,Xorg(XI), ,V(E(1, F1), 1),,V(E(2, Fl), 0), 3, D9 ,V(E(I,A2),I),V(A(I,A2),I)} D11. {,Xorg(X1), ,V(E(1, Fl), 1), .,V(E(2, Fl), 0), 24, D10 , Verbindg(E(3, F1), E( 1, A2, ,V(E(3, F1), 1), V(A(1, A2), 1)} D12. {,Xorg(X1), ,V(E(1, Fl), 1), .,V(E(2, Fl), 0), 11, D11 , V( E(3, Fl) , 1), , V( A( 1, A2) , 1) } D13. {,Xorg(X1), ,V(E( 1, F1), 1), .,V(E(2, Fl), 0), 24, D12 ,V(E(3,Fl),I)"Verbindg(A(I,A2),y),V(y,I)} D14. {,Xorg(X1), ,V(E( 1, Fl), 1), ,V(E(2, Fl), 0), 14, D13 ,V(E(3,Fl),1),V(E(3,F1),1)} DIS. {.,Xorg(X1), ,V(E( 1, F1), 1), 20, D14 .,V(E(2, Fl), 0), ,V(E( 1, 01),1), ,Org(01),V(A(1,01),1)} D16. {,Xorg(X1), ,V(E( 1, F1) ,1), ,V(E(2, Fl), 0), 5, DIS ,V(E(3,F1),1),V(A(1,01),1)} D17. {,Xorg(X1), ,V(E( 1, Fl), 1), ,V(2, Fl), 0), 24, D16 ,V(E(3, F1), 1), ...,Verbindg(A( 1, 01), y), V(y, 1)} D18. {,Xorg(X1), ...,V(E( 1, Fl), 1), .,V(E(2, Fl), 0), 17, D17 .,V(E(3,Fl),1),V(A(2,F1),I)} 139. 4 Resolution 119 Die Anwendung des Prdikatenkalkls in diesem Anwendungsbe- reich bietet mehrere Vorteile. Der naheliegendste ist, da eine einzige Designbeschreibung einer Schaltung fr die unterschied- lichsten Zwecke verwendet werden kann. Wie hier gezeigt wurde, knnen wir einen Schaltkreis simulieren, ihn diagnostizieren und fr alle Beschreibungen Fehlertests erstellen. Natrlich gilt dies auch fr alle anderen Sprachen, die eine deskriptive Semantik besitzen. Die Ausdruckskraft des Prdikatenkalkls erlaubt aber auch, Designbeschreibungen auf abstrakteren Stufen zu erstellen und sie fr diese Zwecke auch zu benutzen. Diese Aufgaben knnen wir mit abstrakteren Designbeschreibungen effizienter als auf der untersten Gatter-Ebene durchfhren. Wegen der Flexibilitt der Sprache und der Deduktionstechniken knnen wir letztendlich diese Aufgaben auch bei unvollstndigen Informationen ber die Struktur oder ber das Verhalten des Schaltungsdesigns durchfhren. 4-.9 BEISPELE AUS DER WELT DER HATHEMATIK Die Mathematik bietet zahlreiche Probleme, die sich mit Inferenz- methoden wie der Resolution lsen lassen. Als einfaches Beispiel betrachten wir die Aufgabe, zu zeigen, da die Schnittmenge zweier Mengen in jeder der beiden Mengen enthalten ist. Wir beginnen mit unseren Definitionen. Das erste der folgenden Axiome stellt die Definition der Schnittmengenfunktion mithilfe des Elementoperators dar. Ein Objekt liegt in der Schnittmenge zweier Mengen genau dann, ~enn es in beiden Mengen enthalten ist. Eine Menge ist eine Teilmenge einer anderen Menge genau dann, wenn jedes Element der ersten Menge ein Element der zweiten ist. VxVsVt xes A xet ~ xesnt VsVt (Vx xes ~ xet) ~ s~t Unser Ziel sei es, zu zeigen, da die Schnittmenge zweier Mengen in jeder der beiden Mengen enthalten ist. Wegen der Kommu- 140. 120 4 Resolution tativitt der Schnittmengenfunktion brauchen wir nur das Enthal- tensein in einer der beiden Mengen zu beweisen. 'v's'v'l srl!;;s Die folgende Ableitung zeigt den Beweis des Theorems. Die ersten drei Klauseln stammen aus der Definition der Schnittmenge. Die nchsten zwei sind aus der Definition der Teilmengenfunktion abgeleitet. Beachten Sie bitte die Anwendung der Skolemfunktion F. Die sechste Klausel resultiert aus der Negation der Ziel-Klausel. Dort setzen wir die Skolemkonstanten A und Bein. 1. {xfts, xtl!l, xesnl} 2. {xftsnl, xes} 3. {xftsnt,xel} 4. {FCs,l)es,s!;;l} 5. {FCs,l)ftS,s!;;l} 6. {AnB A} 7. {FCAnB,A)eAnB} 8. {FCAnB,A)ftA} 9. {FCAnB,A)eA} 10. {} t:. t:. t:. t:. t:. r 4, 6 5, 6 2, 7 8, 9 Der Beweis ist recht einfach. Die Klauseln in den Zeilen 7 und 8 wurden durch die Resolution der Ziel-Klausel mit den Klauseln von Zeile 4 und 5 abgeleitet. Die Klausel 7 resolviert dann mit Klausel 2 zu Klausel 9, die im Widerspruch steht mit der Kon- klusion aus Zeile 8. 4.10 KONSISTENZ UND VOLLSTNDIGKEIT* Die Resolution ist insofern konsistent, als sie jede Klausel, die aus einer Datenbasis angeleitet werden kann, auch logisch impliziert. Der Beweis ist wiederum recht einfach. 141. 4 Resolution 121 THECREM 4.1. (Ka-.lSlSTENZ (DER saJNONESSTHECREM) Gibt es eine Re- solutionsableitung einer Klausel 11> aus einer Datenbasis A von Klauseln, dann impliziert Alogisch 11>. BEWEIS: Der Beweis wird einfach durch Induktion ber die Lnge der Resolutionsschritte gefhrt. Fr die Induktion mssen wir zeigen, da jeder gegebene Resolutionsschritt korrekt ist. Angenommen, 11> und ~ seien beliebige Klauseln, die zu der neuen KauseI ((li> - {~ , 1 ... ,~}) u (~- bl/l , ... ,..,I/l }))o m 1 n resolvieren, wobei 0 der entsprechende Unifikator ist. Angenommen, ~ sei ein Literal, das durch Anwendung des Unifikators auf die Faktoren in 11> und ~ entsteht, d.h. ~ = ~ 0 = I/l o. Sei nun I eine beliebige Interpretation i i und [V) eine beliebige Variablenzuordnung, so da F 11> [V) und I F ~[V). Falls I F ~[V) , I dann gilt ~ ..,~[V) I und daher folgt F (11)0 - I {..,~})[V). Wenn F"'~ [V), dann gilt auch ~ ~[V) und somit auch I I F (11)0 - {~}) [V). Dann aber folgt F ((11>0 - {~}) u (~o - {..,~})) [V) I I und F ((11>0 - {~, ... ,~}) u (~- {..,I/l , ... ,..,I/l }))o[V). 0 1 1 m 1 n Als Spezialfall dieses Theorems sehen wir nun, da eine Daten- basis A die leere Klausel logisch impliziert und deshalb unerfllbar ist, wenn es eine Deduktion der leeren Klausel aus ihr gibt. Die Resolution ist nicht in dem im Kapitel 3 definierten Sinne vollstndig. Sie erzeugt von sich aus nicht jede Klausel, die logisch von einer gegebenen Datenbasis impliziert wird. Beispiels- weise wird die Tautologie {P,..,P} von jeder Datenbasis logisch impliziert, aber die Resolution leitet sie nicht aus der leeren Datenbasis ab. In der Resolution knnen wir auch keine Stze verwenden, die Gleichheits- oder Ungleichheitsrelationen enthalten. Ist zum Bei- spiel eine Datenbasis gegeben, die nur aus den Stzen P(A) und A=B besteht, so kann der Satz P(B) nicht abgeleitet werden. Dies liegt daran, da -- soweit es die Datenbasis betrifft -- die Relations- 142. 122 4 Resolution konstante = beliebig ist. Es ist ein zustzliches Axiomenschema ntig. um ihr die Standardinterpretation zuzuordnen. Andererseits ist die Prozedur aber fr Datenbasen. die Stze ohne Gleichheits- oder Ungleichheitsrelation enthalten. wider- legungsvollstndig. D.h . wenn eine unerfllbare Satzmenge gegeben ist. dann wird garantiert die leere Klausel abgeleitet. Wie schon in Abschnitt 4.6 beschrieben. knnen wir deshalb mit dieser Pro- zedur die logische Implikation nachweisen. indem wir die Negation der zu beweisenden Klausel zu der gegebenen Datenbasis hinzuad- dieren und so deren Unerfllbarkeit zeigen. Der Beweis der Widerlegungsvollstndigkeit ist etwas kompli- zierter und bedarf der Einfhrung mehrerer neuer Begriffe und Lemmata. Zuerst stellen wir deshalb eine spezielle Klasse von Grundinstanzen von Klausel vor. Danach zeigen wir dann. da die Resolution fr Grundklauseln im allgemeinen und fr unsere spe- ziellen Einsetzungen im Besonderen vollstndig ist. Abschlieend verwenden wir diese Ergebnisse. um das Vollstndigkeitstheorem allgemein zu beweisen. Enthlt eine Menge b. Objektkonstanten. so sei O(b.) die Menge aller in b. vorkommenden Objektkonstanten. Andernfalls sei O(b.) die Menge. die nur aus einer einzigen Objektkonstanten. zum Beispiel aus A. besteht. F(b.) sei die Menge aller in b. vorkommenden Funk- tionskonstanten. Das Herbranduniversum H(b.) ist dann die Menge aller aus den Elementen von O(b.) und F(b.) bildbaren zulssigen Grundterme. Die folgenden dienen als Beispiele. H( { {P(A. B)}. {Q(B), R(C)} }) = {A.B. C} H({{P(B)}.{Q(F(x),G(y))}}) = {B.F(B).G(B).F(F(B)),F(G(B)).G(F(B)).G(G(B)) ... } H({{P(x)}.{.,P(y)}}) = {A} Die Herbrandbasis einer Klauselmenge f1 ist die Menge aller Grundklauseln. in denen alle Variablen durch alle Elemente des Herbranduniversums von b. ersetzt worden sind. Eine Herbrandinter- pretation fr eine Klauselmenge b. ist eine Interpretation. die die 143. 4 Resolution 123 Grundterme auf sich selbst und die Grundatome auf wahr oder auf falsch abbildet. Genauer. eine Interpretation I ist eine Herbrand- interpretation von II genau dann. wenn sie die folgenden Bedin- gungen erfllt. (1) 111 ist genau das Herbranduniversum von ll. (2) I bildet jede Objektkonstante auf sich selbst ab. (3) Ist 1l ein n-ste11iges Funktionssymbol und sind T Terme. dann bildet I den Term ll(T T) auf n 1 n I I den Term ll(T . T ) ab. was gerade ll(T T ) ist. 1 n 1 n Beachten Sie. da diese Defini tion fr die Relationssymbole keine Einschrnkung enthlt. Wir knnen daher jede beliebige In- terpretation whlen. Fr jede erfllbare Herbrandbasis knnen wir eine Herbrandinterpretation bilden. die sie fplgendermaen erfllt: Weil die Herbrandbasis erfllbar ist. besitzt sie ein Mo- delI. Wir konstruieren nun unsere Herbrandinterpretation. indem wir diejenigen atomaren Stze wahr machen. die im Modell wahr sind. und diejenigen atomaren Stze falsch machen. die auch im Mo- dell falsch sind. Mit dieser Beobachtung knnen wir nun unser erstes Theorem beweisen. THE~ 4.2. (tERBRANDTHEO und ~ die leere Klausel nicht enthlt, so existiert mindestens eine Klausel, sagen wir ~, die mehr als ein Litera1 enthlt. Aus dieser Klausel whlen wir nun das Literal > aus und bilden eine neue Klausel ~ I = ~ - {>}. ~ I ist aussagekrftiger als ~. Daher mu auch die Menge (~ - {~}) U {~/} unerfllbar sein. Diese Menge enthlt ein berschssiges Li- teral weniger. Wegen der Induktionsvoraussetzung gibt es eine Re- solutionsableitung der leeren Klausel aus dieser Menge. Entspre- chend ist auch die Menge (~ - {~}) u {{>}} unerfllbar. Daher gibt es gem der Induktionsvoraussetzung auch eine Resolutionsablei- tung der leeren Klausel aus dieser Menge. Verwenden wir ~' fr die vorangegangene Widerlegung nicht, so gilt diese Widerlegung genau- so fr ~. Anderenfalls knnen wir sie wie folgt konstruieren: Zu- 145. 4 Resolution 125 erst fgen wir ~ und alle seine Vorgnger wieder zu ~' hinzu, so da diese Folge eine Widerlegung aus 6 bildet. Ist die leere Klau- sel immer noch ein Element dieser Folge, so sind wir fertig. An- derenfalls erzeugt die Addition von ~ zu der leeren Kausel die einfache Klausel {~}. Nun knnen wir eine Deduktion der leeren Klausel aus (6 - {~}) u {{~}} bis zum Ende dieser erweiterten De- duktion bilden. 0 Nachdem wir uns mit Grundklauseln befat haben, wenden wir uns nun dem allgemeinenen Fall der Resolution zu. Bevor wir aber das zentrale Ergebnis beweisen werden, zeigen wir zuerst, da eine De- duktion ohne Grundklausel auf eine mit Grundklauseln zurck- gefhrt werden kann. LEI'1'1A 4.1: (LFTt-K; LEI'1'1Al Sind ~ und 1{1 zwei Klauseln ohne ge- meinsame Variablen, sind ~' und ~' Grundinstanzen von ~ und 1{1, und ist X' eine Resolvente von~' und 1{1', so gibt es eine Resolvente X von ~ und 1{1 soda X' eine Substitutionsinstanz von X ist. BEWE5: Falls X' eine Resolvente von ~, und 1{1' ist, dann gibt es ein Literal ~' in ~, und ein Literal ,~' in 1{1' so da X' = (~' {~,} u (1{1' - {,~,}). Da nun ~' und 1{1' Grundinstanzen von 1{1 und ~ sind, so gibt es eine Substitution 9, mit ~, = ~9 und 1{1' = 1{19. Sei nun {~ , ... ,~} eine Literalmenge aus ~, die 9 auf ~' abbildet, 1 m und sei {~, ... ,~} eine Literalmenge aus 1{1, die 9 auf ,~, ab- I n bildet. Der allgemeinste Unifikator von {~ , ... ,~ }, der das Li- 1 m teral ~" erzeugt, sei 0". T sei der allgemeinste Unifikator von {~ , ... ,~ }, der das Literal ~" erzeugt. Sei 0 = O"UT die Ver- 1 n einigung der Substitutionen. Nach der Konstruktion und Definition des allgemeinen Unifikators mu nun ~' eine Instanz von ~" und ~' eine Instanz von ~" sein. Daher gibt es einen Unifikator von ~" und ~". Sei '( dieser allgemeinste Unifikator von ~" und ~". Nun bilden wir die Resolvente von ~ und 1{1, so da 146. 126 4 Resolution x = (4)0'1 - {I/I , ... ,1/1 }oD) u ("'0'1 - {,1/1 , ... ,.,1/1 }OD) 1 m 1 n Mit den von uns eingefhrten Definitionen knnen wir den Aus- druck fr X' wie folgt umschreiben. X' = (4)6 - {I/I , ... ,1/1 }6) U ("'6 - (,1/1 , ... ,.,1/1 }6) 1 m 1 n Da nun 1/1' eine Instanz von 1/1" und 1/1" ist und 6 weniger allgemein als 0'1 ist, so mu X' eine Instanz von X sein, womit das Lemma bewiesen wre. 0 Im folgenden Theorem verwenden wir das Lifting-Lemma, um zu zeigen, da alle Grunddeduktionen zu Deduktionen ohne Grund- klauseln erweitert - sozusagen "geliftet" - werden knnen. THECREM 4.4. (LIFTING THECREM) Ist t, I eine Menge von Grundinstan- zen von Klauseln aus t, und gibt es eine Resolutionsableitung einer Klausel X' aus t, I , so gibt es eine Resolutionsableitung einer Klausel X aus t" soda X' eine Substitutionsinstanz von X ist. BEWEIS: Wir brauchen nur eine Induktion ber die Lnge der Resolu- tionsableitungen durchzufhren. 0 Fassen wir alle diese Ergebnisse zusammen, so knnen wir allgemein die Widerspruchsvollstndigkeit der Resolutionsprozedur zeigen. THECREM 4.5. (VCl..LSTNDIGKEITSTHECREM) Ist eine Klauselmenge t, unerfllbar, so gibt es eine Resolutionsableitung der leeren Klausel aus t,. BEWEIS: Ist eine Klauselmenge t, unerfllbar, so folgt mit dem Her- brandtheorem, da es eine unerfllbare Menge von Herbrandinstanzen 147. 4 Resolution 127 der Klauseln aus ~ gibt. Mit dem Vollstndigkeitstheorem fr Grundklauseln folgt dann daraus, da eine Resolutionsableitung aus den Klauseln dieser Menge existiert. Mit dem Lifting-Theorem ergibt sich schlielich, da diese Deduktion zu einer Deduktion der leeren Klausel aus ~ umgewandelt werden kann. 0 Die Vollstndigkeit der Resolution ist eine angenehme Eigen- schaft, denn diese Prozedur bietet vom Aufwand her erhebliche com- putationelle Vorteile gegenber den in Kapitel 3 vorgestellten Techniken. Auerdem knnen wir diese Prozedur noch durch restriktive Strategien, die wir in KapitelS einfhren werden, effizienter gestalten. 4.11 RESOLUTION UND GLEICHHEIT Wie in dem vorangegangenen Abschnitt erwhnt, gilt die Wider- spruchsvollstndigkeit der Resolution nicht fr Datenbasen, die die Relationskonstante = enthalten, die ja meist als Gleichheits- relation interpretiert wird. Fr die Ersetzung der als gleich gel- tenden nicht-variablen Terme gibt es einfach kein Verfahren. Auch wenn diese logisch durch die Prmissen impliziert werden, ist es deshalb unmglich, irgendwelche Ergebnisse zu beweisen. In vielen Fllen knnen wir diese Schwierigkeit aber umgehen, indem wir unsere Stze so umndern, da diejenigen nicht-variablen Terme, die mglicherweise gleich sein knnten, auf der obersten Ebene des Literals erscheinen, in dem sie vorkommen. Diese Terme sind dann also nicht in andere Termen eingebettet. Als Beispiel fr die beschriebene Methode betrachten wir die folgende Definition der Fakultts-Funktion, Fakt. Das Problem bei dieser Definition von Fakt liegt darin, da der zweite Satz eingebettete nicht-variable Terme wie k-l und Fakt(k-l) enthlt. Obwohl 148. 128 4 Resolution diese Terme ableitbare Werte besitzen, ist die Resolution fr eine Substitution dieser Werte zu schwach. Fakt(O)=1 Fakt(k)=k*Fakt(k-l) Die Alternative besteht darin, die Definition wie folgt umzu- schreiben. Alle nicht-variablen Terme erscheinen auf der obersten Ebene der Literale, in denen sie vorkommen. Mit dieser Formu- lierung ist die Resolution leistungsfhig genug, die Ergebnisse abzuleiten, die in der vorigen Formulierung nicht ableitbar waren. Fakt(O)=l k-l=j 1 Fakt(j)=m 1 k*m=n = Fakt(k)=n Als nchstes Beispiel betrachten wir die folgende Ableitung des Wertes von Fakt(2). Die ersten zwei Zeilen enthalten die Klauseln unserer Definition. Die dritte Zeile ist das negierte Ziel. Um die Zeile 4 zu erhalten, setzten wir die Definition von Fakt aus Zeile 2 ein. Das erste Literal der Definition werten wir mit prozedura- ler Auswertung (PA) des ersten Literals von Zeile 4 aus und erhalten eine Klausel, die Fakt(1) enthlt. Dieser Vorgang wiederholt sich, und wir erhalten eine Klausel mit Fakt(O). Daraufhin bentzen wir die Definitionsbasis von Fakt. Nach zwei weiteren Schritten, in denen wieder prozedurale Auswertungen durchgefhrt werden, erhalten wir schlielich die Antwort. l. {Fakt(O)=l} !J. 2. {k - i'-"j, Fakt(j)*m, k*m*n, Fakt(k)=n} !J. 3. {Fakt(2)*n, Ans(n)} r 4. {2 -l*jl, Fakt(jl)*ml, 2*ml*n, Ans(n)} 2, 3 5. {Fakt(1)*ml, 2*ml*n, Ans(n)} 4, PA 6. {1-1*j2, Fakt(j2)*m2,l*m2*ml, 2*ml*, Ans(n)} 2, 5 7. {Fakt(O)*m2,1*m2*ml, 2*ml*n, Ans(n)} 6, PA 8. {1*l*ml, 2*ml*n, Ans(n)} 1, 7 9. {2*1*n, Ans(n)} 8, PA 10. { Ans(2)} 9, PA 149. 4 Resolution 129 Eine andere Mglichkeit, mit Stzen, die Gleichheitsprdikate enthalten, umzugehen ist, die Gleichheitsrelation zu axiomati- sieren und entsprechende Substitutionsaxiome bereitzustellen. Die ntigen Axiome fr die Gleichheit folgen hier. Wir wissen ja, da die Gleichheit reflexiv, symmetrisch und transitiv ist. Tlx x=x TlxTly x=y =9 y=x TlxTlyTiz x=z 1 y=z =9 X=Z Wir formulieren nun die Substitutionsaxiome, mit denen wir dann in jeder unserer Funktionen und Relationen Terme durch andere Terme ersetzen knnen. Die folgenden Axiome dienen als Beispiele. TlkTljTlm k=j 1 Fakl(j)=m =9 Fakt(k}=m TlkTijTlmTin j=m 1 k*m=n =9 k*j=n Wenden wir die Resolution auf diese Axiome an, so knnen wir Konklusionen ohne eingebettete Terme ableiten. Die nachfolgende Resolutionsableitung erlutert dies anhand unseres Beispiels Fa- kultt. Die ersten beiden Zeilen enthalten die Klauseln unserer Definition der Fakl-Funktion. Die Zeile 3 ist das Transitivitts- axiom fr die Gleichheit. Die Zeilen 4 und 5 sind die Klauseln fr unsere Substitutionsaxiome. Die Zeile 6 ist das negierte Ziel. 1. {Fakt(O}=1} II 2. {Fakt(k}=k*Fakl(k -1}} II 3. {Py, ,/*z, x=z} II 4. {k*j, Fakl(j}*m, Fakl(k}=m} II 5. {j*m, k*m*n, k*j=n} II 6. {Fakl(2}*n,Ans(n} } r 7. {Fakl(2}*y,,/*n, Ans(n}} 3, 6 8. {2*Fakt(2-1l*n, Ans(n) } 2, 7 9. {Fakl(2-1}*j1,2*j1*n,Ans(n}} 5, 8 10. {2 -1*ml, Fakl(ml}*j1, 2*j1*n, Ans(n}} 4, 9 11. {Fakl(1}*j1, 2*j1*n, Ans(n}} 10, PA 12. {Fakt( 1l*y, ,/*j1, 2*j1*n, Ans(n}} 3, 11 150. 130 4 Resolution 13. {1*Fakl(1-1)*j1,2*j1*n,Ans(n)} 2, 12 14. {Fakl(1-1)*j2, 1*j2*j1, 2*j1*n, Ans(n)} 5, 13 15. {1-1*m2, Fakt(m2)*j2, 1*jUj1, 2*j1*n, Ans(n)} 4, 14 16. {Fakt(O)*j2, 1*j2*j1, 2*j1*n, Ans(n)} 15, PA 17. {1*1*j1,2*j1*n, Ans(n)} 1, 16 18. {2*1*n, Ans(n)} 17, PA 19. {Ans(2)} 18, PA Bei der Anwendung dieses Methode mssen wir natrlich fr jede einzelne Funktion oder Relation, in der Substitutionen vorgenommen werden sollen, die Substitutionsaxiome einzeln angeben. Dies hat zwar den Vorteil, da wir den Inferenzproze implizit dadurch kon- trollieren knnen, da wir fr ganz bestimmte Funktionen und Rela- tionen Substitutionsaxiome bereitstellen, whrend andere ausge- lassen werden. Der Nachteil ist aber, da es meist sehr aufwendig ist, diese Axiome bei einer Vielzahl von Funktionen und Relationen zu formulieren. Obwohl keine dieser Techniken optimal ist, ist die Lage doch auch nicht hoffnungslos. Es gibt nmlich eine Inferenzregel, Para- modulation genannt, die, wenn man sie der Resolution hinzufgt, die Widerspruchsvo1lstndigkeit sogar in den Fllen garantiert, in denen Stze mit Gleichheit auftreten. Es gibt auch eine schwchere Version der Paramodulation, die sogenannte Demodulation, die effizienter und verstndlicher ist als die Paramodulation. Die Demodu- lation ist die Basis der Semantik von funktionalen Programmier- sprachen wie zum Beispiel LISP. Trotz deren sicherlich groen Be- deutung fr die KI haben wir uns entschlossen, diese Inferenz- regeln hier nicht zu behandeln, so da wir uns auf andere Aspekte innerhalb der logischen Begrndung der KI konzentrieren knnen. Allerdings setzen wir in manchen unserer Beispiele die Existenz einiger Methoden fr den Umgang mit Gleichheitsprdikaten voraus, und bilden daher auch Axiome mit beliebig eingebetteten Termen. 151. 4 Resolution 131 4.12 UTERATUR UNO HISTORISCHE BEJ-ERKUNGEN Das Resolutionsprinzip wurde von Robinson [Robinson 1965] vorgestellt und basiert auf frheren Arbeiten von Prawitz [Prawitz 1960) und anderen. Die Bcher von Chang und Lee [Chang 1973], Loveland [Loveland 1978], Robinson [Robinson 1979] und Wos u.a. [Wos 1984a] beschreiben Resolutionsbeweismethoden und -systeme. Eine ntzliche Sammlung mit Aufstzen ber das Theorembeweisen findet man bei Siekmann und Wrightson [Siekmann 1983a, Siekmann 1983b]. Man vergleiche auch die berblicksartikel von Loveland [Loveland 1983) und von Wos [Wos 1985]. Unsere Prozedur zur Umwandlung von Stzen in die Klauselform geht auf Arbeiten von Davis und Putnam zurck [Davis 1960]. Die Resolution kann auch auf Formeln und nicht nur auf Klauseln angewendet werden (vg1. [Manna 1979, Stickel 1982). Ein Unifikationsalgorithmus und ein Beweis fr die Korrektheit wird bei Robinson [Robinson 1965] vorgestellt. Seither sind verschiedene Variationen erschienen. Rau1ef u.a. [Rau1ef 1978] bieten einen berblick ber die Unifikation und ber Pattern Matching. Paterson und Wegmann [Paterson 1976] stellen einen in der Zeit (und im Speicherplatz) linearen Unifikationsalgorithmus vor. Die Unifikation hat immer mehr Bedeutung in der Computerwissenschaft und in der Computerlinguistik [Shieber 1986] gewonnen. Sie ist die der Computersprache PROLOG zugrundeliegende Operation [C1ocksin 1981, Sterling 1986]. Die Verwendung von Antwort1iteralen in der Resolution wurde erstmals von Green vorgeschlagen [Green 1969b] und detai1iert durch Luckham und Ni1sson [Luckham 1971] untersucht. Die Idee der prozedurale Auswertung ist sehr wichtig bei der Steigerung der Performanz von theorembeweisenden Systemen. Die Arbeiten von Wey- rauch [Weyrauch 1980] erklren diese Technik, die er selbst semantische Auswertung (eng1. semantic attachment) nennt, anhand des Begriffes eines partiellen Modelles eines Satzes. Semantisches Auswertung ist ein besonders gutes Beispiel fr die wichtige Brk- ke, die zwischen dem dek1arativen und dem prozedura1en Wissen bei komplexen KI-Systemen ntig ist. Stickel [Stickel 1985] zeigt, wie semantische Auswertungen mit dem zusammenhngt, was er selbst "Theorie-Resolution" ("theory resolution") nennt. Die Konsistenz wie auch die Vollstndigkeit der Resolution wurde ursprnglich von Robinson [Robinson 1965] gezeigt. Unser Be- weis der Vollstndigkeit der Resolution basiert auf dem Theorem von Herbrand [Herbrand 1930]. BUNGEN 1. Klauselform. berfhren Sie die folgenden Stze in die Klauselform. 152. 132 4 Resolution a. VxVy P(x,y) ~ Q(x,y) b. VxVy ,Q(x,y) ~ ,P(x,y) c. VxVy P(x,y) ~ (Q(x,y) ~ R(x,y d. VxVy P(x,y) A Q(x,y) ~ R(x,y) e. VxVy P(x,y) ~ Q(x,y) V R(x,y) f. VxVy P(x,y) ~ (Q(x,y) A R(x,y g. VxVy (P(,y) V Q(x, y A R(x, y) h. Vx3y P(x, y) ~ Q(x,y) i. ,Vx3y P(x,y) ~ Q(x,y) j. (,Vx P(x ~ (3x P(x 2. Unifikation. Prfen Sie, ob die Elemente der nachfolgenden Paare miteinander unifizieren oder nicht. Falls ja, geben Sie den allgemeinsten Unifikator an; falls nein, geben Sie eine kurze Begrndung. a. Farbe(Tweely, Gelb) Farbe(x,y) b. Farbe(Tweely, Gelb) Farbe(x,x) c. Farbe(Hul(Poslbole) ,Blau) Farbe(Hul(y),x) d. R(F(x),B) R(y,z) e. Ry),y,z) R(x, F(A), F( v f. Liebt(x, y) Liebl(y, x) 3. Resolution. Kopf, ich gewinne; Zahl, du verlierst. Zeigen Sie mit der Resolution, da ich gewinne. 4. Resolution. Wenn ein Kurs leicht ist, dann sind einige Studenten zufrieden. Ist ein Kurs zu Ende, dann ist kein Student zufrieden. Zeigen Sie mit der Resolution, da ein Kurs nicht leicht war, wenn er zu Ende ist. 5. Resolution. Viktor ist ermordet worden und Arthur, Bertram und Carleton sind verdchtig. Arthur sagt, er htte es nicht getan. Er sagt, da Bertram der Freund des Opfers gewesen sei, aber da Carleton das Opfer gehat habe. Bertram sagt, er wre am Mordtag nicht in der Stadt gewesen und auerdem htte er den Kerl gar nicht gekannt. Carleton sagt, da er unschuldig wre und da er Arthur und Bertram 153. 4 Resolution 133 zusammen mit dem Opfer kurz vor dem Mord gesehen habe. Klren Sie mit der Resolution das Verbrechen auf, wobei Sie davon ausgehen knnen, da --- auer dem Mrder --- alle die Wahrheit sagen. 6. Logische Axiome. Formulieren Sie eine Instanz fr jedes der in Kapitel 3 vorgestellten Axiomenschemata und zeigen Sie mit der Resolution die Gltigkeit Ihrer Instanz. 154. 5 Resolutionsstrategien KAPITEL 5 RESOLUTIONSSTRATEGIEN EINER DER NACHTEILE EINER unkontrollierten Anwendung der Resolu- tionsregel liegt in der Erzeugung zahlreicher berflssiger Infer- enzen. Einige Inferenzen sind redundant in dem Sinne, da ihre Konklusionen auch auf anderen Wegen ableitbar sind; andere Infer- enzen sind berflssig, weil sie das gewnschte Ergebnis gar nicht erst erzeugen. Als Beispiel betrachten wir die Resolutionsspur aus Abb. 5.1. Hier sind die Klauseln 9, 11, 14 und 16 redundant. Die Klau- seln 10 und 13 und die Klauseln 12 und 15 sind ebenfalls berflssig. All diese Redundanzen fhren dann bei spteren Deduktio- nen zu weiteren Redundanzen. Doppelt auftretende Klauseln knnen wir entfernen und so die Entstehung redundanter Konklusionen ver- hindern. Ihre alleinige Generierung ist aber schon ein Zeichen fr die Ineffizienz einer unbeschrnkten Anwendung des Resolutions- prinzips. Dieses Kapitel stellt nun eine Reihe von Strategien vor, mit denen sich derart unntige Arbeit vermeiden lt. Dabei ist es 135 155. 136 5 Resolutionsstratati.e l. {P,Q} II 2. (,P, R} II 3. ('Q,R} II 4. {, R} r 5. {Q,R} 1,2 6. {P,R} 1,3 7. (,P} 2,4 8. (,Q} 3,4 9. {R} 3,5 10. {Q} 4,5 11. {R} 3,6 12. {P} 4,6 13. {Q} 1,7 14. {R} 6,7 15. {P} 1,8 16. { R} 5,8 17 . {} 4,9 18. {R} 3,10 19. {} 8,10 20. {} 4,11 2l. {R} 2,12 22. {} 7,12 23. { R} 3,13 24. {} 8,13 25. {} 4,14 26. { R} 2,15 27. {} 7,15 28. {} 4,16 29. {} 4,18 30. {} 4,21 3l. {} 4,23 32. {} 4,26 Abb.5.1 Beispiel fr eine unbeschrnkte Resolution 156. S Resolutionsatrategien 137 wichtig im Gedchnis zu behalten, da wir uns hier nicht mit der Reihenfolge befassen, in der die Inferenzen vollzogen werden, sondern ganz allein nur mit der Grsse des Resolutionsgraphen und wie man diese Grsse durch das Entfernen unntiger Deduktionen verringern kann. 5.1 ELlI'1NATIONSSTRATEGIEN Die Eliminationsstrategie ist eine Restriktionstechnik, bei der Klauseln, die bestimmte Eigenschaften besitzen, eliminiert werden, bevor sie berhaupt erst verwendet werden. Da diese Klauseln fr die nachfolgende Deduktion dann gar nicht mehr verfgbar sind, verringert sich der Rechenaufwand. Ein in einer Datenbasis vorkommendes Literal heit genau dann pur, wenn es keine zu einer Instanz eines anderen Literals der Da- tenbasis komplementre Instanz besitzt. Eine Klausel, die ein pu- res Literal enthlt, ist fr eine Widerlegung unbrauchbar, weil dieses Literal ja niemals resolviert werden kann. Das Entfernen von Klauseln mit puren Literalen definiert eine Eliminationsstra- tegie, die als Eliminierung der puren Literale bekannt ist. Die nachfolgende Datenbasis ist unerfllbar. Bei dem entsprechenden Beweis knnen wir die zweite und dritte Klausel weg- lassen, weil beide das pure Literal S enthalten. {,P"Q,R} {,P,S} {,Q,S} {P} {Q} {,R} Beachten Sie bitte, da es mit der Resolution unmglich ist, Klauseln mit puren Literale abzuleiten, wenn die Datenbasis keine puren Literale enthlt. Im Endeffekt mssen wir also diese Stra- 157. 138 5 Resolutionsstrategie tegie bei einer Datenbasis nicht fter als ein Mal anwenden, und insbesonders mssen wir auch nicht jede einzelne erzeugte Klausel gesondert prfen. Eine Tautologie ist eine Klausel, die ein komplementres Paar von Literalen enthlt. Beispielsweise ist die Klausel {P(F(A, ,P(F(A} eine Tautologie. Die Klausel {P(x),Q(y)"Q(y),R(z)} enthlt zwar zustzliche Literale , ist aber ebenfalls eine Tauto- logie. Die An- oder Abwesenheit von Tautologien in einer Klauselmenge hat also keinen Einflu auf die Erfllbarkeit dieser Klauseln. Eine erfllbare Klauselmenge bleibt erfllbar , unabhngig davon, welche Tautologien wir hinzufgen. Eine unerfllbare Klauselmenge bleibt unerfllbar, auch wenn alle Tautologien aus ihr entfernt werden. Wir knnen deshalb die Tautologien aus einer Datenbasis entfernen, weil sie in weiteren Inferenzen nie Verwendung finden. Die entsprechende Eliminationsstrategie nennt man Eliminierung der Tautologien. Beachten Sie, da beim Entfernen der Tautologien die Literale in einer Klausel exakte Komplemente sein mssen. Wir knnen nicht einfach zwei nicht-identische Literale entfernen, nur weil sie in Bezug auf die Unifikation komplementr sind. Die Klauseln {,P(A), P(x)} , {P(A)} und {,P(B)} sind zwar unerfllbar; wrden wir aber die erste Klausel entfernen, so wrde die verbleibende Menge erfllbar . Bei der Subsumptionseliminierung hngt das Kriterium fr die Eliminierung von einer bestimmten Beziehung zwischen zwei Klauseln einer Datenbasis ab. Eine Klausel ~ subsumiert eine Klausel ~ genau dann, wenn es eine Substitution Ci' gibt mit ~Ci' S;;~. Zum Bei- spiel subsumiert die Klausel {P(x),Q(y)} die Klausel {P(A), Q(v), R(w)} , weil es eine Substitution {xlA,y/v} gibt, die die erste Klausel zu einer Teilmenge der zweiten macht. Wird ein Element einer Klauselmenge von einem anderen Element subsumiert, so bleibt nach der Eliminierung der subsumierten Klau- sel die Menge noch erfllbar, wenn sie es vorher auch schon war. 158. 5 Resolutionsstrategien 139 Subsumierte Klauseln drfen also entfernt werden. Weil der Resolu- tionsproze selbst Tautologien und subsumierte Klauseln erzeugen kann, mssen wir die Resolutionen bezglich Tautologien und Sub- sumptionen berprfen. 52 OE UNIT-RESOLUTION Eine Unit-Resolvente ist eine Resolvente, bei der mindestens eine der Elternklauseln eine sogenannte Unit-Klausel ist, d.h. eine Klausel, die nur ein einziges Literal enthlt. Eine Unit-Deduktion ist eine Deduktion, in der alle abgeleiteten Klauseln Unit-Resol- venten sind. Eine Unit-Widerlegung ist eine Unit-Deduktion der leeren Klausel {}. Als Beispiel fr eine Unit-Widerlegung betrachten wir den folgenden Beweis. Bei den ersten beiden Inferenzen werden aus der Ausgangsmenge die zweielementigen Klauseln mit den Unit-Klauseln resolviert. Diese bilden zwei neue Unit-Klauseln und werden dann mit der ersten Klausel zu zwei weiteren Unit-Klauseln resolviert. Zur Erzeugung eines Widerspruchs werden dann die Elemente dieser beiden Mengen alle einzeln miteinander resolviert. l. {P,Q} II 2. {,P,R} II 3. {,Q,R} II 4. bR} r 5. {,P} 2,4 6. {,Q} 3,4 7. {Q} 1,5 8. {P} 1,6 9. {R} 3,7 10. {} 6,7 11. {R} 2,8 12. {} 5,8 159. 140 5 ResolutionBstrategie Beachten Sie, da der Beweis nur eine Teilmenge aller mglichen Anwendungen der Resolutionsregel enthlt. Die Klauseln 1 und 2 knnen zum Beispiel knnen auch zu der Konklusion {Q,R} resolviert werden. Diese Konklusion -- und alle ihre Nachfolger -- wird aber nie erzeugt, weil keine ihrer Elternklauseln Teil einer Unit-K1au- seI ist. Die auf der Unit-Resolution basierenden Inferenzregeln lassen sich relativ leicht implementieren und sind auch ziemlich effi- zient. Es ist auch interessant, da bei der Resolution einer Klau- sel durch eine Unit-Klausel die Konklusion immer weniger Literale als ihre Elternklausel enthlt. Dies hilft uns, den Suchaufwand auf die Generierung der leeren Klausel zu beschrnken, was wiederum die Effizienz erhht. Leider sind die auf der Unit-Resolution basierenden Inferenz- regeln nicht vollstndig. Beispielsweise sind die Klauseln {P,Q} , {,P,Q} ,{P"Q} inkonsistent. Mit der allgemeinen Resolution lt sich die leere Klausel leicht ableiten. Mit der Unit-Resolution dagegen ist dies nicht mglich, weil keine der Ausgangsklauseln eine Unit-Klausel ist. Beschrnken wir uns andererseits aber auf Horn-Klauseln (d.h. auf Klauseln mit hchstens einem positiven Literal), so sieht die Lage schon sehr viel besser aus. In der Tat kann man zeigen, da es eine Unit-Widerlegung genau dann gibt, wenn die Menge der Horn- Klauseln unerfllbar ist. 5.3 DIE EINGABE-RESOLUTION Eine Eingabe-Resolvente (engl. input resolvent) ist eine Resol- vente, bei der mindestens eine der zwei Elternklauseln ein Element der Ausgangsdatenbasis (d. h. der "Eingabe" -Datenbasis) ist. Eine Eingabe-Deduktion (engl. input deduction) ist eine Deduktion, bei der alle abgeleiteten Klauseln Eingabe-Resolventen sind. Eine Ein- 160. 5 Resolutionsstrategien 141 gabe-Widerlegung (engl. input refutation) ist somit eine Ein- gabe-Deduktion der leeren Klausel {}. Als Beispiel betrachten wir die Klauseln 6 und 7 aus Abb. 5.1. Verwenden wir ohne irgendwelche Restriktionen die Resolution, so resolvieren diese Klauseln zu der Klausel 14. Hier liegt allerdings keine Eingabe-Resolution vor, weil keine der Elternklauseln in der Ausgangsdatenbasis enthalten ist. Die Resolution der Klauseln 1 und 2 ist dagegen eine Eingabe-, aber keine Unit-Resolution. Ungeachtet solcher Unterschiede lt sich zeigen, da die Unit- und die Eingabe-Resolution in ihrer in- ferentiellen Leistung einander quivalent sind, und da es zu jeder Menge, zu der eine Unit-Resolution existiert, auch eine Ein- gabe-Resolution gibt -- und umgekehrt. Eine Konsequenz aus dieser Tatsache ist, da zwar fr Horn- Klauseln die Eingabe-Resolution vollstndig, im allgemeinen aber unvollstndig ist. Die unerfllbare Menge von Propositionen {P, Q}, {.,P,Q}, {P,.,Q} diene hier wiederum als Beispiel fr eine De- duktion, bei der die Eingabe-Resolution fehlschlgt. Bei einer Eingabe-Widerlegung mu nmlich (insbesonders) eine der Eltern- klauseln von {} ein Element der Ausgangsdatenbasis sein. Um in unserem Beispiel aber die leere Klausel zu erzeugen, mssen wir entweder zwei einelementige Literalklauseln oder zwei Klauseln ableiten, deren Faktoren aus einem einzelnen Literal bestehen. Kei- nes der Elemente der Basismenge erfllt aber diese Kriterien, so da in diesem Fall auch keine Eingabe-Widerlegung vorliegt. 5.4 UNEARE RESOLUTION Die lineare Resolution (engl. linear resolution oder auch ances- try-filtered resolution) ist eine leicht verallgemeinerte Version der Eingabe-Resolution. Eine lineare Resolvente ist eine Resol- vente, bei der mindestens eine Elternklausel entweder in der Aus- 161. 142 5 Resolutionsstratesie {P,Q} (,P,Q) {P,,} {P} {Q} {} Abb.5.2 Resolutionskette einer linearen Deduktion gangsdatenbasis enthalten aber ein Nachfahre einer anderen Eltern- klausel ist. Eine lineare Deduktion ist eine Deduktion, bei der jede abgeleitete Resolvente eine lineare Resolvente ist. Eine lineare Widerlegung ist dann eine lineare Deduktion der leeren Klausel {}. Ihren Namen hat die lineare Resolution von der linearen Gestalt des Beweises, den sie erzeugt. Eine lineare Deduktion beginnt mit einer Klausel der Ausgangsdatenbasis (Start-Klausel oder top clause genannt) und erzeugt, wie in Abb. 5.2 dargestellt, eine lineare Resolutionskette. Ausgehend von der ersten Resolvente erhlt man jede weitere Resolvente aus der letzten Resolventen (auch direkter Vorfahre genannt) und aus einer weiteren Klausel (weiter entferntere Vorfahre genannt). Bei der linearen Resolution mu der weiter entferntere Vorfahre entweder in der Ausgangsdaten- basis enthalten, oder ein Nachfahre der letzten Resolventen sein. Bei einer Resolution ohne Restriktionen entstehen zahlreiche Redundanzen durch das Resolvieren von Konklusionen als Zwischen- ergebnisse aus frheren Zwischenergebnissen. Der Vorteil der line- 162. 5 Resolutionsstrategien 143 aren Resolution liegt nun darin, da sie unsinnige Inferenzen ver- hindert, weil sie bei jedem Schritt die Deduktion auf die Vor- fahren jeder Klausel und auf die Elemente der Ausgangsdatenbasis einschrnkt. Von der linearen Resolution wei man, da sie widerspruchsvoll- stndig ist. Auerdem mu nicht jede einzelne Klausel der Aus- gangsdatenbasis als Start-Klausel durchprobiert werden. Man kann zeigen, da, eine lineare Widerlegung mit ~ als Start-Klausel existiert, wenn eine Klauselmenge r erfllbar und r v {~} unerfllbar ist. Wissen wir also, da eine bestimmte Klauselmenge konsistent ist, so brauchen wir bei einer Widerlegung deren Elemente nicht zu verwenden. Eine Herge-Resolvente ist eine Resolvente, die der Literale , die von den Elternklauseln vererbt wurden und nach der Anwendung des allgemeinsten Unifikators indentisch sind, zu einem einzigen Literal "verschmolzen" werden. Die Vollstndigkeit der linearen Resolution bleibt auch dann erhalten, wenn nur Merge-Resolventen verwendet werden. Beachten Sie in dem Beispiel (Abb. 5.2), da hier die erste Resolvente (d.h. die Klausel {Q}) eine Merge-Resol- vente ist. 5.5 STTZI"ENGENRESOLUTION Untersuchen wir eine Resolutionsspur wie die aus Abb. 5.1, so zeigt sich, da viele Konklusionen aus Resolutionen zwischen Klau- seln abstammen, die in einem Bereich der Datenbasis enthalten sind, von dem bekannt ist, da er erfllbar ist. Zum Beispiel ist in Abb. 5.1 die Menge A erfllbar. Eine ganze Menge der Konklusi- onen des Protokolls erhalten wir durch das Resolvieren der Elemen- ten von A mit anderen Elementen von A. Diese Resolutionen knnen wir, ohne die Widerspruchsvollstndigkeit der gesamten Resolution zu beeinflussen, entfernen. 163. 144 S Resolutionsstrategie Eine Teilmenge r einer Menge A wird StOtzmenge (eng1. set of support) von A genannt genau dann, wenn A - r erfllbar ist. Ist eine Klauselmenge A mit Sttzmenge r gegeben, so ist eine StOtz- mengenresolution (engl. set of support resolution) eine Resolu- tion, bei der mindestens eine Elternklausel aus r stammt oder ein Nachfahre von r ist. Eine StOtzmengendeduktion (eng1. set of support deduction) ist eine Deduktion, bei der alle abgeleiteten Klauseln Resolventen der Sttzmenge sind. Eine StOtzmengenwider- legung (engl. set of support refutation) ist daher eine Deduktion der leeren Klausel {} aus der Sttzmenge. Die folgende Spur zeigt eine Sttzmengenwiderlegung von Abb. 5.1. Die Klausel {,R} resolviert mit {,P,R} und {,Q,R} zu {,P} und {,Q}. Diese resolvieren mit Klausel 1 zu {Q} und {P}, die dann zu der leeren Klausel resolvieren. 1. {P,Q} A 2. {,P,R} A 3. {,Q,R} A 4. {,R} r 5. {,P} 2,4 6. bQ} 3,4 7. {Q} 1,5 8. {P} 1,6 9. {R} 3,7 10. {} 6,7 11. {R} 2,8 12. {} 5,8 Diese Strategie htte natrlich wenig Sinn, wenn sich die Sttzmenge nicht sehr leicht bestimmen liee. Glcklicherweise gibt es auch verschiedene Mglichkeiten, dies ohne groen Aufwand zu tun. Zum Beispiel ist es in Situationen, in denen wir ver- suchen, Konklusionen aus einer konsistenten Datenbasis zu beweisen, naheliegend, die aus dem negierten Ziel abgeleiteten Klau- 164. 5 Resolutionsstrategien 145 seIn als passende Sttzmenge zu whlen. Sofern die Datenbasis natrlich selbst erfllbar ist, gengt diese Menge dann der Defini- tion. Bei der derart bestimmten Sttzmenge hat jede Resolution eine Verbindung mit dem bergeordneten Ziel, so da man die Proze- dur auch so auffassen kann, als arbeitete man sich "rckwrts" vorn Ziel weg. Dies ist besonders bei solchen Datenbasen sinnvoll, bei denen die Zahl der mglichen "vorwrts erreichbaren" Konklusionen sehr gro ist. Durch den ziel-orientierten Charakter dieser Wider- legungen sind diese oftmals verstndlicher als andere Widerle- gungsstrategien. 5.6 GEORDNETE RESOLUTION Eine geordnete Resolution (engl. ordered resolution) ist eine sehr restriktive Resolutionsstrategie , bei der jede einzelne Klausel in Form einer linear geordneten Menge gegeben ist. Eine Resolution wird nur fr das erste Literal jeder Klausel zugelassen, d.h. nur fr das in der Ordnung an niedrigster Stelle stehende Literal. In den Konklusionen behalten die Literale die Ordnung ihrer Eltern- klausein, wobei die Literale der negativen Elternklausel (d. i. die, die negierte Atom enthlt) nach denen der positiven Literale komm

[Michael r. genesereth,__nils_j._nilsson__(auth.),(book_zz.org)

Engineering

Transcript of [Michael r. genesereth,__nils_j._nilsson__(auth.),(book_zz.org)

Michael Bildhauer H˜ohere Mathematik f ˜ur Ingenieure ... · U N I V E R SI T A S S A R A V I E N S I S Michael Bildhauer H˜ohere Mathematik f ˜ur Ingenieure { Ein Viersemestriger

intio-NET ホスティングサービス SMTP-AUTH の設定手順...intio-NET ホスティングサービス SMTP-AUTH の設定手順 6 ii. メールソフトにOutlook をご利用の場合

Particle Physics Education R-ECFA meeting Germany Michael Kobel TU Dresden

· Facebook Blogs Webinare Chats/Onlineberatung Beispiele innovativer Marketingmaßnahmen Werbliche Ansätze, z.B. "Social Media" Nicht nur Facebook, sondern auth YouTube. Xing,

[Camillo Sitte (Auth.)] Der Städte-Bau Nach Seine(BookZZ.org)

LENA Photosensor R&D Marc Tippmann Lothar Oberauer, Michael Wurm, Gyorgy Korga, Quirin Meindl, Michael Nöbauer, Thurid Mannel, Martin Zeitlmair, German.

Röntgeninterferenz - A1-Collaboration · Röntgeninterferenz auf Basis der Ubergangsstrahlung¨ Vortrag: Michael Becker 15.01.07 Der komplexe Brechungsindex Löst man die Maxwell-Gleichungen

[W._F._Duisenberg_(auth.),_T._J._Kastelein,_S._K._( ).pdf

Megapulser Teil1-1 - Download Centerdownloads.cdn.re-in.de/250000-274999/250179-in-02-de...normalcn Diese Batterie tut 10 Monatc da 3esorgnss. r Batterieproblcme spricht, wurden. Auth

r .'l-'El-r ·:r::3TFALEN Präsidentin des Landtags VORL/.(': 16/ 4738 · 2017. 3. 3. · Aktulle St1die der De1isc u Gesellschft fir du hdewesu e. V. Dip1.-Sportwiss. Michael Weilandt,

Gerhard Göhler (Auth.), Gerhard Göhler, Kurt Lenk, Herfried Münkler, Manfred Walther (Eds.)-Politische Institutionen Im Gesellschaftlichen Umbruch_ Ideengeschichtliche Beiträge

Franz Ulrich (Auth.)-Die Ausbildung Der Höheren Verwaltungsbeamten in Preussen Und Ihre Stellung in Der Staatseisenbahnverwaltung-Springer Berlin Heidelberg (1893)

( ) Dipl.-Ing. Klaus Menny (auth.)-Strömungsmaschinen-Vieweg+Teubner Verlag (1985)

( ) Niels Bohr (Auth.)-Atomtheorie Und Naturbeschreibung-Springer Berlin Heidelberg (1931)

Verzeichnis der Veröffentlichungen: Michael C. Böhm€¦ · Verzeichnis der Veröffentlichungen: Michael C. Böhm 1978 1. M.C. Böhm und R. Gleiter, Tetrahedron Lett. 1179-1182

Teil 1 - Musterantrag - LSB Sachsen-Anhalt · 2018. 10. 9. · VO 13052013 hat for die ELER- Folge de r von In ELER- in den hat der dass des sirø und die Cross oSs auth eröffentlichung

SMTP Auth Outlook 2010 - support.aronet.swiss · SMTP Authentifizierung Outlook 2010 I N F O R M A T I K Anleitung - Outlook 2010 1. Schritt Starten Sie Ihr Outlook 2010, indem Sie

1995.05.15 - Nicholl v. E-470 Pub. Highway Auth._ 896 P.2d 859

Bruno, Raphael R.; Donner-Banzhoff, Norbert; Söllner, Wolfgang; Frieling, Thomas; Müller, Christian; Christ, Michael Interdisziplinäre Versorgung akuter.

MRS.NIDHI CHAUHAN.pdf.phdiagnostics.ae/sample reports/FIT SAMPLE REPORT.pdf · 05/10/2016 17:30 Result Age/Sex Auth Date Auth Time Food BLUEBERRY BUFFALO MILK Patient ID Patient Ref.