Zur Logik der Logik-Programmierung: Ein konstruktiver Ansatz

ISBN-13: 9783540507208 / Niemiecki / Miękka / 1988 / 246 str.

Clemens Beckstein

Opis

Thema der Arbeit ist das zentrale Problem logischer Programmiersprachen: ein optimales Gleichgewicht zwischen sprachlicher Ausdruckskraft und effizienter Realisierbarkeit eines entsprechenden Beweissystems zu finden. Nach einer Zusammenstellung der fur das Verstandnis der Arbeit notigen logischen Grundbegriffe folgt eine Analyse bzw. Besprechung von KI-Programmiersprachen, die im Umkreis der logischen Verarbeitungsmodelle angesiedelt sind. Sodann wird Prolog mit seiner Theorie dargestellt und einer grundsatzlichen Kritik unterzogen. Eine genauere Untersuchung der logisch bedenklichen Prolog-Konstrukte (insbesondere Negation as Failure) weist dabei den Weg zu einer konstruktiven Interpretation und Verallgemeinerung der Prolog zugrundeliegenden Logik. Im Anschluss an eine Schilderung der Grundlagen des Reason-Maintenance wird ein entsprechendes Beweissystem (RISC) entwickelt. Es gestattet die Verarbeitung eines Teils der intuitionistischen Konsequenzlogik, der weitaus ausdrucksstarker als die herkommliche Hornklausellogik ist. Durch die Unterstutzung eines Reason-Maintenance-Systems kann dabei das Grundprinzip der SLD-Resolution weitgehend beibehalten und eine effiziente Verarbeitung erreicht werden. Die Arbeit endet mit einer Skizze von Anwendungsgebieten, fur die RISC pradestiniert zu sein scheint."

Spis treści

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.