Inhaltsverzeichnis

Vorwort zur 1. Auflage ...... 1

Vorwort zur 2. überarbeiteten und erweiterten Auflage ..... 3

Kapitel I: Geschichte und Anwendungen (J. H. Siekmann) ..... 5

1 Einleitung ..... 5
2 Frühgeschichte ..... 6
3 Erste Deduktionssysteme ..... 12
4 Die Zeit nach 1965 ..... 15
5 Teilgebiete ..... 19
6 Anwendungen ..... 21
7 Schlußwort ..... 22
Literatur ..... 23 Kapitel II: Grundlagen und Beispiele (N. Eisinger, H. J. Ohlbach) ..... 25 1 Einführung ..... 25
2 Prädikatenlogik erster Stufe ..... 26 2.1 Syntax von PL1 ..... 27
2.2 Semantik von PL1 ..... 28
2.3 Normalformen in PL1 ..... 31
2.4 Beschränkungen und Modifikationen von PL1 ..... 33 3 Kalküle für die Prädikatenlogik erster Stufe ..... 35 3.1 Gentzen-Kalküle (Kalküle des natürlichen Schließens) ..... 37
3.2 Resolution ..... 39
3.3 Theorieresolution ..... 44 4 Repräsentation ..... 48 4.1 Tableaus ..... 49
4.2 Klauselgraphen ..... 52 4.2.1 Klauselgraphen als Datenstruktur und Indexierungshilfsmittel ..... 52
4.2.2 Klauselgraphen mit allgemeinen Reduktionsregeln ..... 56
4.2.3 Klauselgraphen mit spezifischen Reduktionsregeln ..... 59
4.2.4 Graphen als Repräsentation von Beweisen ..... 62
4.2.5 Extraktion von Widerlegungsbäumen aus Klauselgraphen ..... 67 4.3 Matrizen ..... 69 4.3.1 Zusammenhang zwischen Matrix- und Tableauverfahren ..... 72
4.3.2 Zusammenhang zwischen Matrix- und Resolutionsverfahren. ..... 73 4.4 Abstrakte Sichtweise der Repräsentationsschicht ..... 75 5 Steuerung ..... 79 5.1 Restriktionsstrategien ..... 79
5.2 Ordnungsstrategien ..... 81 6 Zwei konkrete Deduktionssysteme ..... 84 6.1 MKRP ..... 84
6.2 OTTER ..... 85 Literatur ..... 87 Kapitel III: Die Gleichheitsrelation ..... 91 1 Das Problem der Gleichheit (K. H. Bläsius, H. J. Ohlbach, A. Präcklein) ..... 91 1.1 Formalisierung der Gleichheit innerhalb der Prädikatenlogik ..... 92
1.2 Gleichheit als Teilproblem ..... 93
1.3 Teilgebiete der Gleichheitsbehandlung ..... 95 2 Allgemeine Gleichheitsverfahren (K. H. Bläsius, A. Präcklein) ..... 96 2.1 Untertermersetzung: Paramodulation ..... 96
2.2 Kontrolle Resolution - Gleichheit: E-Resolution ..... 99
2.3 Abstandsverringerung: RUE-Resolution ..... 101
2.4 Planen: Equality Graphs ..... 105
2.5 Schlußbemerkungen ..... 109
Literatur ..... 110 3 Unifikationstheorie (H.-J. Bürckert) ..... 112 3.1 Robinson-Unifikation ..... 112
3.2 Theorieunifikation ..... 113
3.3 Eigenschaften von Lösungsmengen ..... 115
3.4 Die Unifikationshierarchie ..... 116
3.5 Einige Resultate für spezielle Theorien ..... 118
3.6 Kombination von Theorien und universelle Unifikation ..... 119
3.7 Ein Beispiel: Unifikation in Booleschen Ringen ..... 123
3.8 Schlußbemerkungen ..... 124
Literatur ..... 124 4 Termersetzungssysteme (N. Eisinger, A. Nonnengart, A. Präcklein) ..... 126 4.1 Einführung ..... 126
4.2 Termersetzungsregeln ..... 128
4.3 Eigenschaften von Termersetzungssystemen ..... 129
4.4 Kritische Ausdrücke und kritische Paare ..... 131
4.5 Das Knuth-Bendix-Verfahren ..... 134
4.6 Knuth-Bendix-Vervollständigung modulo einer Äquivalenzrelation ..... 136
4.7 Das Knuth-Bendix-Verfahren als Beweisprozedur für Gleichungen ..... 138
4.8 Knuth-Bendix-Vervollständigung mit Theorieunifikation ..... 139
4.9 Das Knuth-Bendix-Verfahren als Beweisprozedur für Klauseln ..... 142
4.10 Das Knuth-Bendix-Verfahren als Induktionsbeweiser ..... 144
Literatur ..... 147 Kapitel IV: Deduktion als Berechnung (H.-J. Bürckert) ..... 151 1 Einführung: Logische Programme ..... 151
2 Resolution für Horn-Formeln ..... 154
3 Kompilation von logischen Programmen ..... 158
4 Theorieunifikation in logischen Programmen ..... 161
5 Sorten und Typen ..... 165
6 Logische Programme mit Constraints ..... 167
7 Schlußbemerkungen ..... 175
Literatur ..... 176 Kapitel V: Vollständige Induktion (D. Hutter) ..... 179 1 Einführung ..... 179
2 Grundlagen ..... 180
3 Aufbau einer Datenbasis ..... 183 3.1 Definition von Datenstrukturen ..... 183
3.2 Definition von Funktionen ..... 186 3.2.1 Eindeutigkeit und Vollständigkeit ..... 188
3.2.2 Terminierung ..... 189 4 Nachweis von Funktionseigenschaften (Lemmata) ..... 195 4.1 Verwendung der Induktionsschemata ..... 195 4.1.1 Erzeugung von Induktionsschemata ..... 196
4.1.2 Auswahl eines Induktionsschemas ..... 200
4.1.3 Induktion über beliebige Terme ..... 201 4.2 Spezielle Strategien für Induktionsbeweise ..... 203 4.2.1 Symbolische Auswertung ..... 203
4.2.2 Rippling ..... 205 4.3 Generalisierung ..... 207
4.4 Existenzbeweise ..... 209 5 Schlußbemerkungen ..... 211
Literatur ..... 211 Kapitel VI: Beweissysteme mit Logiken höherer Stufe (M. Kohlhase) ..... 213 1 Einführung in die Typtheorie ..... 213 1.1 Typen ..... 215
1.2 Syntax von PLW ..... 216
1.3 Semantik von PLW ..... 216
1.4 Existenzaxiome ..... 217
1.5 l-Kalkül ..... 218
1.6 Normalformen ..... 220
1.7 Beispiele ..... 222
1.8 Varianten und Erweiterungen der einfachen Typtheorie ..... 223 2 Beweisverfahren in der Typtheorie ..... 226 2.1 Unifikation in der Typtheorie ..... 226
2.2 Prä-Unifikation ..... 230
2.3 Beweisprüfer ..... 230
2.4 Automatische Beweisverfahren ..... 231
2.5 Huets Constrained Resolution ..... 232
2.6 Beispiele ..... 235 Literatur ..... 237 Kapitel VII: Modal- und Temporallogik (A. Nonnengart, H. J. Ohlbach) ..... 239 1 Modallogiken ..... 239 1.1 Einfache Modallogik ..... 239 1.1.1 Doxastische Interpretation ..... 240
1.1.2 Epistemische Interpretation ..... 241
1.1.3 Temporale Interpretation ..... 242 1.2 Formale Definition der einfachen Modallogik ..... 243 1.2.1 Syntax ..... 243
1.2.2 Semantik ..... 243 1.3 Relationale Übersetzung in Prädikatenlogik ..... 247
1.4 Korrespondenzeigenschaften ..... 249
1.5 Modallogik mit parametrisierten Modaloperatoren ..... 257
1.6 Funktionale Übersetzung in Prädikatenlogik ..... 258
1.7 Nachbarschaftssemantik ..... 267 2 Temporallogik ..... 270 2.1 Konstruktion der Grundlogik ..... 271
2.2 Topologie der Zeit ..... 277 2.2.1 Linearität ..... 277
2.2.2 Dichte Zeit ..... 278
2.2.3 Diskrete Zeit ..... 278
2.2.4 Endliche oder unendliche Zeit ..... 280 2.3 METATEM ..... 281 3 Zusammenfassung ..... 282
Literatur ..... 283 Anhang ..... 285 Weiterführende Literatur ..... 285
Stichwortverzeichnis ..... 287 Vorwort zur 1. Auflage

Die Fähigkeit, logische Schlüsse zu ziehen, ist eine wesentliche Grundlage intelligenten Verhaltens. Deshalb sind Schlußfolgerungs- oder Deduktionskomponenten fester Bestandteil vieler Systeme der Künstlichen Intelligenz (KI). Die Anwendungen für Deduktionssysteme gehen also über das automatische Beweisen mathematischer Theoreme – der ursprünglichen Motivation für die Entwicklung solcher Systeme – hinaus. Aus ihnen wurden logische Programmierspachen wie PROLOG entwickelt und sie werden inzwischen bei natürlich-sprachlichen Systemen ebenso verwendet wie in Expertensystemen oder für intelligente Robotersteuerung. Darüberhinaus haben auch die logikorientierten Methoden dieses Gebietes Eingang in die Grundlagenforschung fast aller KI-Gebiete gefunden.

Der Bedarf an einführenden Veranstaltungen und an Lehrmaterial zum Thema Deduktions-systeme wurde in den letzten Jahren immer wieder von Wissenschaftlern und Anwendern aus den unterschiedlichsten Gebieten der Künstlichen Intelligenz deutlich gemacht. Solche Anregungen, die besonders auf den KI-Konferenzen vorgebracht wurden, waren für uns Anlaß, ein Tutorium über Deduktionssysteme für die 1987er GWAI (German Workshop on Artificial Intelligence) vorzubereiten und dazu ein Buch mit einführenden Aufsätzen zu diesem Thema herauszugeben.

Dieses Buch richtet sich an alle Studenten, Wissenschaftler und Anwender mit Interesse an der Künstlichen Intelligenz und soll dem Leser einen leicht zugänglichen und trotzdem umfassenden Einblick in das Gebiet der Deduktionssysteme ermöglichen. Grundlegende Begriffe und Methoden der Duduktionsysteme werden vorgestellt und – unterstützt durch zahlreiche Beispiele und graphische Darstellungen – erläutert. Dabei erleichtert eine gewisse Vertrautheit mit der Prädikatenlogik das Verständnis. Trotz des einführenden Charakters gibt das Buch in vielen Fällen den aktuellen Forschungsstand wieder und weist auch für den Experten auf diesem Gebiet interessante und neue Aspekte auf.

Das Buch ist in fünf Kapitel unterteilt. Zur Einstimmung und Motivation bietet das erste Kapitel zunächst eine historische Übersicht über die automatische Deduktion und stellt verschiedene Anwendungsgebiete vor. Den Kern des Buches bildet das zweite Kapitel, in dem die wesentlichen Grundlagen des Gebietes unter Verwendung zahlreicher Beispiele erläutert werden. Geleitet von einem Schichtenmodell eines automatischen Deduktionssystems stellen die beiden Autoren relevante Logiken, wichtige Kalküle, Repräsentationsformen und Kontrollmechanismen vor. Kapitel III befaßt sich mit der Spezialbehandlung der Gleichheit. In Beiträgen über allgemeine Gleichheitsbehandlung, über Unifikationstheorie und über Termersetzungssysteme werden die Bedeutung der Gleichheit und damit verbundenene Probleme aufgezeigt sowie Lösungsansätze beschrieben. Kapitel IV stellt theoretische Grundlagen des logischen Programmierens vor und Kapitel V gibt eine Einführung in das automatische Beweisen mit vollständiger Induktion.

Die Kapitel III, IV und V sind relativ unabhängig voneinander und können in beliebiger Reihenfolge gelesen werden. Das gleiche gilt für die Abschnitte 2, 3 und 4 in Kapitel III. Empfohlen wird also eine Reihenfolge, die sich an folgendem Diagramm orientiert:

Automatische Deduktion hat in Deutschland eine gewisse Tradition: Bereits vor der Publikation des Resolutionsprinzips im Jahre 1965 arbeitete eine Gruppe unter der Leitung von Prof. Dr. G. Veenker in Bonn an automatischen Beweisverfahren. Seit Anfang der 70er Jahre existiert eine international bekannte Arbeitsgruppe unter Leitung von Dr. W. Bibel in München. Vor etwa zehn Jahren entstand die "Markgraf Karl Gruppe" in Karlsruhe, die später mit Prof. Dr. J. Siekmann nach Kaiserslautern wechselte. Die Autoren der Beiträge in diesem Buch sind bzw. waren Mitglieder dieser ebenfalls international anerkannten Arbeitsgruppe und haben an der Entwicklung des Markgraf Karl Systems mitgearbeitet, das als eines der leistungsfähigsten bestehenden Deduktionssysteme bekannt ist.

Bei allen Autoren möchten wir uns ganz herzlich für das Zustandekommen dieses Buches bedanken. Sie haben nicht nur mit ihren eigenen Aufsätzen, sondern auch durch viele Anregungen und gemeinsame Diskussionen am Entstehen des Buches mitgewirkt. Norbert Eisinger und Hans Jürgen Ohlbach haben mit ihrem gemeinsamen Beitrag den Grundstock für die übrigen Artikel und damit für das gesamte Buch gelegt. Desweiteren haben sie durch zahlreiche Hinweise wesentlichen Anteil an der für eine Aufsatzsammlung relativ einheitlichen Darstellung. Ihnen sei daher an dieser Stelle noch einmal besonders gedankt. Prof. Dr. J. Siekmann hat sich bereiterklärt, dem Buch mit einem einleitenden Kapitel den nötigen historischen Rahmen und einen Überblick über die verschiedenen Anwendungsbereiche für Deduktionssysteme zu geben. Dafür und für seine Kommentare zur Gestaltung des Buches und seine hilfreiche Kritik an den einzelnen Beiträgen danken wir ihm herzlich. Bedanken möchten wir uns außerdem – auch im Auftrag der Autoren – bei Susanne Biundo, Peter Borst, Richard Göbel, Birgit Hummel, Manfred Kerber, Achim Posegga, Robert Rehbold, Wolfgang Reif, Prof. Dr. Michael M. Richter, Ingrid Walter, Dr. Christoph Walther und Martin Weigele, die jeweils Teile der Manuskripte gelesen und wichtige Hinweise geliefert haben.

Konstanz und Kaiserslautern, im Juli 1987

Karl Hans Bläsius und Hans-Jürgen Bürckert

Vorwort zur 2. überarbeiteten und erweiterten Auflage

Nachdem die erste Auflage des vorliegenden Buches im Sommer 1991 vergriffen war und aufgrund des regen Interesses hat sich der Oldenbourg-Verlag entschlossen, eine weitere Auflage dieses Buches in Druck zu geben. Die Herausgeber und insbesondere die Autoren waren gerne bereit, für diese Neu-Auflage das Buch zu überarbeiten. Dabei wurden fast alle Kapitel von den jeweiligen Autoren (in einem Fall unter Hinzuziehen eines weiteren Autors (Abschnitte des Kapitels III)) einer intensiven Bearbeitung unterzogen und zum Großteil erweitert bzw. dem neueren Stand der Forschung angepaßt. Besonders erfreulich war, daß sich weitere Autoren fanden, die zwei neue Kapitel – über Logik höherer Stufe und über nicht-klassische Logik – beisteuerten. Auch damit folgt das Buch nun dem aktuelleren Stand der Forschung, der in den letzten Jahren seit der Erst-Auflage (1987) insbesondere in diesen beiden Bereichen zu neuen Resultaten im Hinblick auf die Operationalisierung dieser Logiken und ihre Anwendungen in der Künstlichen Intelligenz gebracht hat. Die beiden neuen Kapitel sind relativ unabhängig von den anderen, wenn sie auch ein gewisses vertieftes Verständnis der Prädikatenlogik erster Stufe voraussetzen – nicht zuletzt, weil sie in weniger bekannte Bereiche der formalen Logik führen.

Aufgrund einiger Kritiken und Rezensionen der ersten Auflage bzw. der englischen Übersetzung möchten wir an dieser Stelle nochmals darauf hinweisen, daß sich das Buch nicht an den Laien richtet, sondern gedacht war und ist als eine Einführung für KI-Forscher und KI-Anwender in die Methoden und formalen Grundlagen der Deduktionssysteme: die Darstellung der Umsetzungsmöglichkeiten und Operationalisierungstechniken für Logik und deduktive Inferenzen. Dabei sollte weniger Wert auf formale Tiefe der Darstellung gelegt, als vielmehr versucht werden, die Materie auch für Leser verständlich aufzubereiten, die weniger versiert sind in mathematischer Logik oder die auf die (beweis-)technischen Hintergründe verzichten wollen, aber sich einen Überblick über die Methoden und Möglichkeiten automatischer Deduktionssysteme verschaffen möchten. Es liegt wohl in der Natur der Sache, daß einige der Kapitel zum tieferen Verständnis der Darlegungen ein zumindest grobes Wissen und Verständnis der Grundlagen der mathematischen Logik erfordern, die wir bei dem angesprochenen Leserkreis allerdings zumindest in Grundzügen erwarten dürften: Die meisten KI-Lehrbücher vermitteln ein ausreichendes Grundwissen in mathematischer Logik.

Wir möchten uns bei allen Autoren dafür bedanken, daß sie die Mühen der Überarbeitung auf sich genommen haben – insbesondere auch den beiden neu hinzugekommen Autoren.

Trier und Saarbrücken, im Januar 1992

Karl Hans Bläsius und Hans-Jürgen Bürckert