Deduktionssysteme: Automatisierung des logischen Denkens
Herausgegeben von K.H. Bläsius und H.-J. Bürckert
mit Beiträgen von
Prof. Dr. K.H. Bläsius
Dr. H.-J. Bürckert
Dr. N. Eisinger
Dr. D. Hutter
M. Kohlhase
A. Nonnengart
Dr. H.J. Ohlbach
A. Präcklein
Prof. Dr. J.H. Siekmann
2., völlig überarbeitete und erweiterte Auflage 1992
R. Oldenbourg Verlag München Wien 1992
Die Deutsche Bibliothek - CIP-Einheitsaufnahme
Deduktionssysteme : Automatisierung des logischen Denkens /
hrsg. von K.H. Bläsius und H.-J. Bürckert. Mit Beitr. von K.
H. Bläsius ... - 2., völlig überarb. und erw. Aufl. - München ;
Wien : Oldenbourg, 1992
ISBN 3-486-22033-0
NE: Bläsius, Karl H. [Hrsg.]
Author(s): K.H. Bläsius und H.-J. Bürckert
Edition: 2
Publisher: R. Oldenbourg
Year: 1992
Language: German
Pages: 287
City: München
Tags: Logic, Logic Programming, Prolog, Deduction Systems
__1 .. Vorwort zur 1. Auflage
__3 .. Vorwort zur 2. überarbeiteten und erweiterten Auflage
__5 .. Kapitel I: Geschichte und Anwendungen (J. H. Siekmann)
__5 ... 1 Einleitung
__6 ... 2 Frühgeschichte
_12 ... 3 Erste Deduktionssysteme
_15 ... 4 Die Zeit nach 1965
_19 ... 5 Teilgebiete
_21 ... 6 Anwendungen
_22 ... 7 Schlußwort
_23 ... Literatur
_25 .. Kapitel II: Grundlagen und Beispiele (N. Eisinger, H.J. Ohlbach)
_25 ... 1 Einführung
_26 ... 2 Prädikatenlogik erster Stufe
_27 ...... 2.1 Syntax von PL1
_28 ...... 2.2 Semantik von PL1
_31 ...... 2.3 Normalformen in PL1
_33 ...... 2.4 Beschränkungen und Modifikationen von PL1
_35 ... 3 Kalküle für die Prädikatenlogik erster Stufe
_37 ...... 3.1 Gentzen-Kalküle (Kalküle des natürlichen Schließens)
_39 ...... 3.2 Resolution
_44 ...... 3.3 Theorieresolution
_48 ... 4 Repräsentation
_49 ...... 4.1 Tableaus
_52 ...... 4.2 Klauselgraphen
_52 ......... 4.2.1 Klauselgraphen als Datenstruktur und Indexierungshilfsmittel
_56 ......... 4.2.2 Klauselgraphen mit allgemeinen Reduktionsregeln
_59 ......... 4.2.3 Klauselgraphen mit spezifischen Reduktionsregeln
_62 ......... 4.2.4 Graphen als Repräsentation von Beweisen
_67 ......... 4.2.5 Extraktion von Widerlegungsbäumen aus Klauselgraphen
_69 ...... 4.3 Matrizen
_72 ......... 4.3.1 Zusammenhang zwischen Matrix- und Tableauverfahren
_73 ......... 4.3.2 Zusammenhang zwischen Matrix- und Resolutionsverfahren
_75 ...... 4.4 Abstrakte Sichtweise der Repräsentationsschicht
_79 ... 5 Steuerung
_79 ...... 5.1 Restriktionsstrategien
_81 ...... 5.2 Ordnungsstrategien
_84 ... 6 Zwei konkrete Deduktionssysteme
_84 ...... 6.1 MKRP
_85 ...... 6.2 OTTER
_87 ... Literatur
_91 .. Kapitel III: Die Gleichheitsrelation
_91 ... 1 Das Problem der Gleichheit (K.H. Bläsius, H.J. Ohlbach, A. Präcklein)
_92 ...... 1.1 Formalisierung der Gleichheit innerhalb der Prädikatenlogik
_93 ...... 1.2 Gleichheit als Teilproblem
_95 ...... 1.3 Teilgebiete der Gleichheitsbehandlung
_96 ... 2 Allgemeine Gleichheitsverfahren (K.H. Bläsius, A. Präcklein)
_96 ...... 2.1 Untertermersetzung: Paramodulation
_99 ...... 2.2 Kontrolle Resolution - Gleichheit: E-Resolution
101 ...... 2.3 Abstandsverringerung: RUE-Resolution
105 ...... 2.4 Planen: Equality Graphs
109 ...... 2.5 Schlußbemerkungen
110 ...... Literatur
112 ... 3 Unifikationstheorie (H.-J. Bürckert)
112 ...... 3.1 Robinson-Unifikation
113 ...... 3.2 Theorieunifikation
115 ...... 3.3 Eigenschaften von Lösungsmengen
116 ...... 3.4 Die Unifikationshierarchie
118 ...... 3.5 Einige Resultate für spezielle Theorien
119 ...... 3.6 Kombination von Theorien und universelle Unifikation
123 ...... 3.7 Ein Beispiel: Unifikation in Booleschen Ringen
124 ...... 3.8 Schlußbemerkungen
124 ...... Literatur
126 ... 4 Termersetzungssysteme (N. Eisinger, A. Nonnengart, A. Präcklein)
126 ...... 4.1 Einführung
128 ...... 4.2 Termersetzungsregeln
129 ...... 4.3 Eigenschaften von Termersetzungssystemen
131 ...... 4.4 Kritische Ausdrücke und kritische Paare
134 ...... 4.5 Das Knuth-Bendix-Verfahren
136 ...... 4.6 Knuth-Bendix-Vervollständigung modulo einer Äquivalenzrelation
138 ...... 4.7 Das Knuth-Bendix-Verfahren als Beweisprozedur für Gleichungen
139 ...... 4.8 Knuth-Bendix-Vervollständigung mit Theorieunifikation
142 ...... 4.9 Das Knuth-Bendix-Verfahren als Beweisprozedur für Klauseln
144 ...... 4.10 Das Knuth-Bendix-Verfahren als Induktionsbeweiser
147 ...... Literatur
151 .. Kapitel IV: Deduktion als Berechnung (H.-J. Bürckert)
151 ... 1 Einführung: Logische Programme
154 ... 2 Resolution für Horn-Formeln
158 ... 3 Kompilation von logischen Programmen
161 ... 4 Theorieunifikation in logischen Programmen
165 ... 5 Sorten und Typen
167 ... 6 Logische Programme mit Constraints
175 ... 7 Schlußbemerkungen
176 ... Literatur
179 .. Kapitel V: Vollständige Induktion (D. Hutter)
179 ... 1 Einführung
180 ... 2 Grundlagen
183 ... 3 Aufbau einer Datenbasis
183 ...... 3.1 Definition von Datenstrukturen
186 ...... 3.2 Definition von Funktionen
188 ......... 3.2.1 Eindeutigkeit und Vollständigkeit
189 ......... 3.2.2 Terminierung
195 ... 4 Nachweis von Funktionseigenschaften (Lemmata)
195 ...... 4.1 Verwendung der Induktionsschemata
196 ......... 4.1.1 Erzeugung von Induktionsschemata
200 ......... 4.1.2 Auswahl eines Induktionsschemas
201 ......... 4.1.3 Induktion über beliebige Tenne
203 ...... 4.2 Spezielle Strategien für Induktionsbeweise
203 ......... 4.2.1 Symbolische Auswertung
205 ......... 4.2.2 Rippling
207 ...... 4.3 Generalisierung
209 ...... 4.4 Existenzbeweise
211 ... 5 Schlußbemerkungen
211 ... Literatur
213 .. Kapitel VI: Beweissysteme mit Logiken höherer Stufe (M. Kohlhase)
213 ... 1 Einführung in die Typtheorie
215 ...... 1.1 Typen
216 ...... 1.2 Syntax von PLΩ
216 ...... 1.3 Semantik von PLΩ
217 ...... 1.4 Existenzaxiome
218 ...... 1.5 ℷ-Kalkül
220 ...... 1.6 Normalformen
222 ...... 1.7 Beispiele
223 ...... 1.8 Varianten und Erweiterungen der einfachen Typtheorie
226 ... 2 Beweisverfahren in der Typtheorie
226 ...... 2.1 Unifikation in der Typtheorie
230 ...... 2.2 Prä-Unifikation
230 ...... 2.3 Beweisprüfer
231 ...... 2.4 Automatische Beweisverfahren
232 ...... 2.5 Huets Constrained Resolution
235 ...... 2.6 Beispiele
237 ... Literatur
239 .. Kapitel VII: Modal- und Temporallogik (A. Nonnengart, H.J. Ohlbach)
239 ... 1 Modallogiken
239 ...... 1.1 Einfache Modallogik
240 ......... 1.1.1 Doxastische Interpretation
241 ......... 1.1.2 Epistemische Interpretation
242 ......... 1.1.3 Temporale Interpretation
243 ...... 1.2 Formale Definition der einfachen Modallogik
243 ......... 1.2.1 Syntax
243 ......... 1.2.2 Semantik
247 ...... 1.3 Relationale Übersetzung in Prädikatenlogik
249 ...... 1.4 Korrespondenzeigenschaften
257 ...... 1.5 Modallogik mit parametrisierten Modaloperatoren
258 ...... 1.6 Funktionale Übersetzung in Prädikatenlogik
267 ...... 1.7 Nachbarschaftssemantik
270 ... 2 Temporallogik
271 ...... 2.1 Konstruktion der Grundlogik
277 ...... 2.2 Topologie der Zeit
277 ......... 2.2.1 - Linearität
278 ......... 2.2.2 - Dichte Zeit
278 ......... 2.2.3 - Diskrete Zeit
280 ......... 2.2.4 - Endliche oder unendliche Zeit
281 ...... 2.3 - METATEM
282 ... 3 Zusammenfassung
283 ... Literatur
285 .. Anhang
285 ... Weiterführende Literatur
287 ... Stichwortverzeichnis
