1 Einleitung.- 1.1 Motivation.- 1.1.1 Logik als Analysewerkzeu.- 1.1.2 Logik als Repräsentations- und SchlußWerkzeu.- 1.1.3 Logik als Programmiersprach.- 1.2 Ausdruckskraft kontra Verarbeitung.- 1.3 Aufbau der Arbeit.- 2 Logische Grundbegriffe.- 2.1 Prädikatenlogik.- 2.1.1 Grundbegriffe der Prädikatenlogik.- 2.1.2 Prädikatenlogische Formeln in Klauselform.- 2.2 Herbrand-Interpretationen.- 2.3 Resolution.- 2.3.1 Einfache Resolution.- 2.3.2 Resolution mit Unifikation.- 2.3.3 Resolutionsstrategien.- 2.3.3.1 Elimination von Tautologien.- 2.3.3.2 "Set-of-support”-Resolution.- 2.3.3.3 P1-und N1-Resolution.- 2.3.3.4 Hyperresolution.- 2.3.3.5 Input-Resolution.- 2.3.3.6 Lineare Resolution.- 2.3.3.7 Einheits-Resolution.- 2.3.3.8 Subsumtions-Resolution.- 2.4 Antwortsubstitutionen.- 2.5 Semantik von Logik-Programmen.- 2.5.1 Modelltheoretische Semantik.- 2.5.2 Semantik des kleinsten Fixpunktes.- 3 Die deklarativ/prozedural-Kontroverse.- 3.1 PLANNER.- 3.2 CONNIVER.- 3.3 Aktorensysteme.- 3.4 Lehren aus dieser Diskussion.- 4 Logik-Programmierung.- 4.1 SLD-Resolution.- 4.1.1 SLD-Widerlegungen.- 4.1.2 SLD-Bäume.- 4.2 PROLOG.- 4.2.1 Suchstrategie von PROLOG.- 4.2.2 Nicht-logische Eigenschaften von PROLOG.- 4.2.2.1 Meta-logische Prädikate und Meta-Variablen.- 4.2.2.2 Die Operatoren CUT und FAIL.- 4.2.2.3 Die Operatoren ASSERT und RETRACT.- 4.2.3 Resümee.- 4.3 FWD-Beweise.- 4.3.1 FWD-Ableitungen.- 4.3.2 FWD-Graphen.- 4.3.3 SLD-Resolution versus FWD-Beweisen.- 4.4 Berechenbarkeitsaspekte.- 5 Die Grenzen der Ausdruckskraft.- 5.1 Konstruktivistische Aspekte.- 5.2 Dialogische Logik und Logik-Programmierung.- 5.2.1 Grundbegriffe der Dialogischen Logik.- 5.2.2 Dialogische Logik versus SLD-Resolution.- 5.2.3 Dialogische versus Klassische Logik.- 5.3 Negation.- 5.3.1 Closed World Assumption.- 5.3.2 Finite Failure und Negation as Failure.- 5.3.3 Vervollständigungen von Logik-Programmen.- 5.4 Resümee.- 6 Reason-Maintenance-Systeme.- 6.1 Grundbegriffe des Reason-Maintenance.- 6.2 Negation und Reason-Maintenance.- 6.2.1 Label-Propagierung.- 6.2.2 Behandlung von NOGOODS.- 6.2.3 Defaults und Trigger.- 6.3 Multiple Welten: DeKleers ATMS.- 6.3.1 ATMS-Entwurfsprinzipien.- 6.3.2 Eigenschaften von ATMS-Labeln.- 6.3.3 Grundfunktionen des ATMS.- 6.3.4 Disjunktionen und Defaults.- 7 Ein vereinheitlichender Ansatz: RISC.- 7.1 Unterstützung von S LD-Resolution.- 7.1.1 Kommunikation zwischen Beweissystem und RMS.- 7.1.2 Generierung von Lemmata.- 7.1.3 Vermeidung wiederholter Ableitungen.- 7.1.4 Relevante Prädikate.- 7.2 Veränderliche Theorien.- 7.2.1 Das Frame-Problem.- 7.2.2 Relevante Fehlschläge.- 7.2.3 NAI statt NAF.- 7.3 Hypothetisches Schließen.- 7.3.1 Variablenfreie Schlüsse.- 7.3.2 Allgemeine Behandlung.- 7.4 Ein Beispiel.- 7.5 Diskussion vergleichbarer Ansätze.- 7.5.1 Parsing und Lemmagenerierung.- 7.5.2 Gabbays theoretische Vorarbeiten.- 7.5.3 Ein dualer Ansatz: FORLOG.- 8 Zusammenfassung und Ausblick.
Eigentlich verdankt diese Arbeit ihren Ursprung zwei Provokationen. Die er ste Provokation stammt von D. G. Bobrow und ist eine Frage, mit der er eine seiner Veroffentlichungen iiberschrieben hat: "If PROLOG is the answer, what is the question?". Sie sollte mir die vergangenen drei Jahre nicnt mehr aus dem Kopf gehen. Heute mochte ich die Frage erweitern: " . . . and given the ques tion, is PROLOG the answer?". Die zweite Provokation hii. ngt mit J. deKleers Assumption Based Truth Maintenance System (ATMS) zusammen, genauer mit der Frage, welche Rolle ein dera. . rtiges Truth-Maintenance-System in einem Logik Programmiersystem spielen konnte. DeKleer selbst schatzt diese Rolle in per sonlichen Au6erungen relativ gering ein. Aus heutiger Sicht gebe ich deKleer zugleich recht und unrecht-recht, wenn er unter Logik-Programmierung im we sentlichen PROLOG versteht, und unrecht, wenn der Begriff weiter gefa6t wird. Trotz oder gerade aufgrund der provokanten Form der beiden erwahnten Aus sagen waren deKleer und Bobrow von zentraler Bedeutung fiir diese Arbeit. Ih nen gilt deshalb mein erster Dank. Sodann mochte ich Herrn Prof. Dr. G. Nees danken, der meinen wissenschaft lichen Werdegang seit meiner Studienzeit kritisch und wohlwollend begleitet hat. Nicht zuletzt seiner Fiirsprache ist es zuzuschreiben, da6 die vorliegende Ar beit durchein Promotionsstipendium der SIEMENS-AG, das Ernst-von-Siemens Stipendium, gefordert wurde. Ohne den damit verbundenen finanziellen Spiel raU1p· hatten viele wert volle Gesprache mit auslandischen Kollegen auf Tagungen und Studienreisen nicht stattfinden konnen. Besonderer Dank gebiihrt auch meinem Doktorvater Prof. Dr. H. Wedekind.
1 Einleitung.- 1.1 Motivation.- 1.2 Ausdruckskraft kontra Verarbeitung.- 1.3 Aufbau der Arbeit.- 2 Logische Grundbegriffe.- 2.1 Prädikatenlogik.- 2.2 Herbrand-Interpretationen.- 2.3 Resolution.- 2.4 Antwortsubstitutionen.- 2.5 Semantik von Logik-Programmen.- 3 Die deklarativ/prozedural-Kontroverse.- 3.1 PLANNER.- 3.2 CONNIVER.- 3.3 Aktorensysteme.- 3.4 Lehren aus dieser Diskussion.- 4 Logik-Programmierung.- 4.1 SLD-Resolution.- 4.2 PROLOG.- 4.3 FWD-Beweise.- 4.4 Berechenbarkeitsaspekte.- 5 Die Grenzen der Ausdruckskraft.- 5.1 Konstruktivistische Aspekte.- 5.2 Dialogische Logik und Logik-Programmierung.- 5.3 Negation.- 5.4 Resümee.- 6 Reason-Maintenance-Systeme.- 6.1 Grundbegriffe des Reason-Maintenance.- 6.2 Negation und Reason-Maintenance.- 6.3 Multiple Welten: DeKleers ATMS.- 7 Ein vereinheitlichender Ansatz: RISC.- 7.1 Unterstützung von S LD-Resolution.- 7.2 Veränderliche Theorien.- 7.3 Hypothetisches Schließen.- 7.4 Ein Beispiel.- 7.5 Diskussion vergleichbarer Ansätze.- 8 Zusammenfassung und Ausblick.
Inhaltsverzeichnis
1 Einleitung.- 1.1 Motivation.- 1.1.1 Logik als Analysewerkzeu.- 1.1.2 Logik als Repräsentations- und SchlußWerkzeu.- 1.1.3 Logik als Programmiersprach.- 1.2 Ausdruckskraft kontra Verarbeitung.- 1.3 Aufbau der Arbeit.- 2 Logische Grundbegriffe.- 2.1 Prädikatenlogik.- 2.1.1 Grundbegriffe der Prädikatenlogik.- 2.1.2 Prädikatenlogische Formeln in Klauselform.- 2.2 Herbrand-Interpretationen.- 2.3 Resolution.- 2.3.1 Einfache Resolution.- 2.3.2 Resolution mit Unifikation.- 2.3.3 Resolutionsstrategien.- 2.3.3.1 Elimination von Tautologien.- 2.3.3.2 ¿Set-of-support¿-Resolution.- 2.3.3.3 P1-und N1-Resolution.- 2.3.3.4 Hyperresolution.- 2.3.3.5 Input-Resolution.- 2.3.3.6 Lineare Resolution.- 2.3.3.7 Einheits-Resolution.- 2.3.3.8 Subsumtions-Resolution.- 2.4 Antwortsubstitutionen.- 2.5 Semantik von Logik-Programmen.- 2.5.1 Modelltheoretische Semantik.- 2.5.2 Semantik des kleinsten Fixpunktes.- 3 Die deklarativ/prozedural-Kontroverse.- 3.1 PLANNER.- 3.2 CONNIVER.- 3.3 Aktorensysteme.- 3.4 Lehren aus dieser Diskussion.- 4 Logik-Programmierung.- 4.1 SLD-Resolution.- 4.1.1 SLD-Widerlegungen.- 4.1.2 SLD-Bäume.- 4.2 PROLOG.- 4.2.1 Suchstrategie von PROLOG.- 4.2.2 Nicht-logische Eigenschaften von PROLOG.- 4.2.2.1 Meta-logische Prädikate und Meta-Variablen.- 4.2.2.2 Die Operatoren CUT und FAIL.- 4.2.2.3 Die Operatoren ASSERT und RETRACT.- 4.2.3 Resümee.- 4.3 FWD-Beweise.- 4.3.1 FWD-Ableitungen.- 4.3.2 FWD-Graphen.- 4.3.3 SLD-Resolution versus FWD-Beweisen.- 4.4 Berechenbarkeitsaspekte.- 5 Die Grenzen der Ausdruckskraft.- 5.1 Konstruktivistische Aspekte.- 5.2 Dialogische Logik und Logik-Programmierung.- 5.2.1 Grundbegriffe der Dialogischen Logik.- 5.2.2 Dialogische Logik versus SLD-Resolution.- 5.2.3 Dialogische versus Klassische Logik.- 5.3 Negation.- 5.3.1 Closed World Assumption.- 5.3.2 Finite Failure und Negation as Failure.- 5.3.3 Vervollständigungen von Logik-Programmen.- 5.4 Resümee.- 6 Reason-Maintenance-Systeme.- 6.1 Grundbegriffe des Reason-Maintenance.- 6.2 Negation und Reason-Maintenance.- 6.2.1 Label-Propagierung.- 6.2.2 Behandlung von NOGOODS.- 6.2.3 Defaults und Trigger.- 6.3 Multiple Welten: DeKleers ATMS.- 6.3.1 ATMS-Entwurfsprinzipien.- 6.3.2 Eigenschaften von ATMS-Labeln.- 6.3.3 Grundfunktionen des ATMS.- 6.3.4 Disjunktionen und Defaults.- 7 Ein vereinheitlichender Ansatz: RISC.- 7.1 Unterstützung von S LD-Resolution.- 7.1.1 Kommunikation zwischen Beweissystem und RMS.- 7.1.2 Generierung von Lemmata.- 7.1.3 Vermeidung wiederholter Ableitungen.- 7.1.4 Relevante Prädikate.- 7.2 Veränderliche Theorien.- 7.2.1 Das Frame-Problem.- 7.2.2 Relevante Fehlschläge.- 7.2.3 NAI statt NAF.- 7.3 Hypothetisches Schließen.- 7.3.1 Variablenfreie Schlüsse.- 7.3.2 Allgemeine Behandlung.- 7.4 Ein Beispiel.- 7.5 Diskussion vergleichbarer Ansätze.- 7.5.1 Parsing und Lemmagenerierung.- 7.5.2 Gabbays theoretische Vorarbeiten.- 7.5.3 Ein dualer Ansatz: FORLOG.- 8 Zusammenfassung und Ausblick.
Klappentext
Eigentlich verdankt diese Arbeit ihren Ursprung zwei Provokationen. Die er ste Provokation stammt von D. G. Bobrow und ist eine Frage, mit der er eine seiner Veroffentlichungen iiberschrieben hat: "If PROLOG is the answer, what is the question?". Sie sollte mir die vergangenen drei Jahre nicnt mehr aus dem Kopf gehen. Heute mochte ich die Frage erweitern: " . . . and given the ques tion, is PROLOG the answer?". Die zweite Provokation hii. ngt mit J. deKleers Assumption Based Truth Maintenance System (ATMS) zusammen, genauer mit der Frage, welche Rolle ein dera. . rtiges Truth-Maintenance-System in einem Logik Programmiersystem spielen konnte. DeKleer selbst schatzt diese Rolle in per sonlichen Au6erungen relativ gering ein. Aus heutiger Sicht gebe ich deKleer zugleich recht und unrecht-recht, wenn er unter Logik-Programmierung im we sentlichen PROLOG versteht, und unrecht, wenn der Begriff weiter gefa6t wird. Trotz oder gerade aufgrund der provokanten Form der beiden erwahnten Aus sagen waren deKleer und Bobrow von zentraler Bedeutung fiir diese Arbeit. Ih nen gilt deshalb mein erster Dank. Sodann mochte ich Herrn Prof. Dr. G. Nees danken, der meinen wissenschaft lichen Werdegang seit meiner Studienzeit kritisch und wohlwollend begleitet hat. Nicht zuletzt seiner Fiirsprache ist es zuzuschreiben, da6 die vorliegende Ar beit durchein Promotionsstipendium der SIEMENS-AG, das Ernst-von-Siemens Stipendium, gefordert wurde. Ohne den damit verbundenen finanziellen Spiel raU1p· hatten viele wert volle Gesprache mit auslandischen Kollegen auf Tagungen und Studienreisen nicht stattfinden konnen. Besonderer Dank gebiihrt auch meinem Doktorvater Prof. Dr. H. Wedekind.
