Mathematische Logik Mit Informatik-Anwendungen

ISBN-13: 9783540082026 / Niemiecki / Miękka / 1977 / 326 str.

E. Bergmann; H. Noll

Opis

Dieses Buch ist aus Skripten der Autoren zu ihrer Vorlesung "Mathe matische Logik (fUr Informatiker)" entstanden. Diese sechssttindige Lehrveranstaltung, die seit dem Sommersemester 1974 jahrlich an der Technischen Universitat Berlin im Fachbereich Informatik ab gehalten wird, will Informatik-Studenten etwa yom 4. Semester an mit Logik-Methoden vertraut machen und gleichzeitig einen" Bei trag zur Mathematik-Ausbildung fUr Informatiker leisten. Dement sprechend handelt es sich urn einen einfUhrenden Text fUr "krasse" Anfanger in der Logik, der mit elementaren Mathematik -Kenntnissen lesbar ist und an Informatik-Voraussetzungen nur einfachste Kon zepte von Programmiersprachen benotigt. Anliegen des Buches, das sich gleichermaBen an Mathematik- und Informatik-Studenten wen det, ist es, einerseits eine mathematisch zufriedenstellende Darstellung der Anfangsgrtinde der Pradikatenlogik der ersten Stufe zu geben, andererseits aber auch Anwendungen dieser Logik innerhalb der Informatik einheitlich in die Logik-Darstellung einzubeziehen. Der Versuch, ein Buch tiber Logik mit Informatik-Anwendungen zu schreiben, ist nicht ohne Probleme, da die Auswahl der Verbin dungen von Logik und Informatik eine subjektive Entscheidung bleibt, so daB tiber den hier vorliegenden Text hinaus Raum fUr andere Bertihrungspunkte und fUr eine intensivere Gestaltung der hier im Text angefUhrten Anwendungen besteht. Man kann dabei z. B. an engere Verbindungen zur theoretischen Informatik denken oder an eine systematische Abhandlung der angesprochenen Anwen dungsgebiete. Dieser Text will dazu anregen, Informatik und Lo gik so aufeinander zu beziehen, daB Logik als Hilfsmittel fUr die Informatik angesehen werden darf, d. h. als eine fruchtbare, Infor matik-Ergebnisse hervorbringende Methode.

Spis treści

1. Vorbemerkungen.- § 1. Einleitung.- § 2. Verwendete Notation.- 2. Einführung und Motivation.- § 3. Programmiersprachen und elementare Konzepte der mathematischen Logik.- § 4. Umgangssprache und die Gestalt der Syntax einer mathematischen Logik.- 4.1. Exkurs: Satz — Aussage — Sachverhalt.- 4.2. Die Zerlegung von Sätzen der natürlichen Sprache in Teilsätze.- 4.3. Exkurs: Extension und Intension.- 4.4. Die Definition der extensionalen Junktoren.- 4.5. Die Feinstruktur von Aussagen.- 4.6. Schreibvarianten der Kalkülzeichen.- Übungen zu § 4.- § 5. Das weitere Vorgehen.- 3. Syntax und Semantik der Prädikatenlogik.- § 6. Syntax und Semantik.- 6.1. Die Syntax der Sprache.- 6.2. Beweise und Definitionen induktiv über den Aufbau der Terme und Formeln.- 6.3. Strukturen und Deutungen.- 6.4. Ein kleines Beispiel für eine Sprache mit Deutung.- Übungen zu § 6.- § 7. Prädikatenlogische Wahrheit.- 4. Eigenschaften der Prädikatenlogik.- § 8. Aussagenlogik im Rahmen der Prädikatenlogik.- 8.1. Erste Gesetze.- 8.2. Ersetzung und Spezialisierung.- 8.3. Weitere Gesetze.- 8.4. Formeln mit aussagenlogischem Aufbau.- Übungen zu § 8.- § 9. Gesetze über Quantoren und Substitution.- 9.1. Gebundene und freie Variable.- 9.1.1. Definitionen.- 9.1.2. Das Koinzidenztheorem.- 9.2. Die Substitution.- 9.2.1. Definitionen.- 9.2.2. Die Bedeutung der Substitution: das Überführungstheorem.- 9.2.3. Die gebundene Umbenennung.- 9.3. Quantorengesetze.- 9.4. Normalformen.- 9.4.1. Pränexe Normalformeln.- 9.4.2. Universelle Normalformeln.- 9.4.3. Konjunktive Normalformeln.- Übungen zu § 9.- § 10. Logisches Schließen als „Rechnen“: Folgern — Ableiten.- 10.1. Problemstellung.- 10.2. Der semantische Folgerungsbegriff.- 10.3. Das syntaktische Ableiten.- 10.3.1. Einführung.- 10.3.2. Ableitungsregeln und eine Axiomenmenge für die Prädikatenlogik.- 10.3.3. Exkurs: Theorien.- 10.3.4. Skizze zum Verhältnis der eingeführten Begriffe zueinander.- 10.3.5. Gesetze über ableitbare Formeln.- 10.3.6. Eine Präzisierung des informellen Beweisens.- 10.4. Die syntaktische Widerspruchsfreiheit.- Übungen zu § 10.- § 11. Der Vollständigkeitssatz.- 11.1. Herausarbeiten der wesentlichen Schwierigkeiten des Beweises.- 11.2. Exkurs: syntaktisch vollständige und maximal syntaktisch widerspruchsfreie Formelmengen.- 11.3. Der Beweis.- 11.4. Konsequenzen aus dem Vollständigkeitssatz.- 11.5. Prädikatenlogik mit Gleichheit.- 11.6. Spezielle Vollständigkeitsresultate.- § 12. Entscheidbarkeitsfragen.- 12.1. Bemerkungen zur Entwicklung des Entscheidungsproblems.- 12.2. Die Entscheidbarkeit der quantorenfreien Formeln (Aussagenlogik).- 12.3. Die Unentscheidbarkeit der Prädikatenlogik.- 12.4. Die Semi-Entscheidbarkeit der Ableitungsmengen.- 12.5. Ein Anwendungsbeispiel aus der Theorie der Programmierung: das Terminationsproblem von Programmen.- 12.5.1. Exkurs zum Forschungsgebiet Semantik von Programmiersprachen.- 12.5.2. Die Termination von Programmen.- Übungen zu § 11 und § 12.- 5. Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip).- § 13. Einleitung.- § 14. Die Klauselform der Prädikatenlogik und Herbrand-Strukturen (eine Umformulierung der klassischen Logik).- 14.1. Folgerungen und Nichterfüllbarkeit.- 14.2. Zur universellen Normalform.- 14.3. Die Klauselform der Prädikatenlogik.- 14.4. Herbrand-Strukturen und der Satz von Herbrand.- Übungen zu § 14.- § 15. Herbrand-Prozeduren.- § 16. Das Resolventenprinzip.- 16.1. Syntaktisches Ableiten in der Klausellogik.- 16.2. Der Vereinheitlichungsalgorithmus.- 16.3. Die Resolventenregel.- 16.4. Das Liften.- 16.5. Die Vollständigkeit der Resolventenregel.- 16.6. Split-Resolventen und volle Resolventen.- Übungen zu § 16.- § 17. Beweisverfahren des Resolventenprinzips.- 17.1. Beweisverfahren.- 17.2. Zur Effizienz (Verfeinerungen der Resolventenregel).- Übungen zu § 17.- § 18. Der konstruktive Charakter von Resolventenableitungen (Greenscher Antworten-Extraktionsprozeß).- 18.1. Motivation.- 18.2. Eine Verschärfung des Resolventensatzes.- 18.3. Resultate in Ableitungen.- 18.4. Ein Verfahren zur Berechnung von Resultaten mit Beispielen für dessen Anwendung.- Übungen zu § 18.- § 19. Prädikatenlogik als Programmiersprache.- 6. Die Methode der Formalisierung: zwei Beispiele.- § 20. Informationswiedergewinnung als Anwendungsbeispiel.- Übungen zu § 20.- § 21. Exkurs: das Formalisieren.- § 22. Die Formalisierung der Wertzuweisung.- Übungen zu § 22.- 7. Probleme mit der Logik.- § 23. Grenzen der mathematischen Logik.- 23.1. Strukturen als „Wirklichkeit“.- 23.2. Zur Definition von Wahrheit.- 23.3. Der methodische Zirkel.- 23.4. Hinweise auf nichtbehandelte Sonderlogiken.- 23.5. Was ist semantisch, was syntaktisch?.- 23.6. Fazit.- § 24. Bemerkungen zur Geschichte der Logik.- 24.1. Warum werden in diesem Buch Probleme der Geschichte der Logik aufgegriffen?.- 24.2. Welche Möglichkeiten bestehen, die Geschichte der Logik adäquat zu behandeln?.- 24.3. Zum Verhältnis von Logik zu Mathematik (und Philosophie).- 24.4. Zu innermathematischen Gründen, die zur Herausbildung der mathematischen Logik führten.- 24.5. Epilog.- Schlußbemerkungen.- A. Beweise von Eigenschaften über Zustandsabänderungen.- B. Der Beweis des Koinzidenztheorems.- C. Beweise von Eigenschaften der Substitution.- Cl. Beweis von Lemma 9.12.- C2. Charakterisierung der Komposition von Substitutionen.- C3. Der Beweis des Überführungstheorems Satz 9.16.- D. Der Satz von der universellen Normalform.- E. Semantische und syntaktische Beweisführung.- F. Beispiele für die Verwendung von Ableitungen.- F1. Beispiel für eine längere Ableitung.- F2. Das Theorem über neue Konstanten.- G. Hilfsmittel für den Vollständigkeitssatz.- G1. Der Lindenbaumsche Ergänzungssatz.- G2. Der Beweis von Satz 11.17.- H. Hilfsmittel aus der Theorie der Berechenbarkeit.- H1. Liste der verwendeten Definitionen und Sätze aus der Theorie der berechenbaren Wortfunktionen.- H2. Die Äquivalenz von Aufzählbarkeit und Semi-Entscheidbarkeit.- H3. Die Aufzählbarkeit der nicht erfüllbaren Formeln.- I. Eine „strikte“Syntax.- J. Zerlegungssatz für allgemeinste Vereinheitlicher.- Literaturangaben.- Hinweise zu weiterführender Literatur.- Verzeichnis häufig verwendeter Symbole.- Namen- und Sachverzeichnis.