Inhalt

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.- § 5. Das weitere Vorgehen.- 3. Syntax und Semantik der Prädikatenlogik.- § 6. Syntax und Semantik.- § 7. Prädikatenlogische Wahrheit.- 4. Eigenschaften der Prädikatenlogik.- § 8. Aussagenlogik im Rahmen der Prädikatenlogik.- § 9. Gesetze über Quantoren und Substitution.- § 10. Logisches Schließen als Rechnen: Folgern Ableiten.- § 11. Der Vollständigkeitssatz.- § 12. Entscheidbarkeitsfragen.- 5. Logische Grundlagen des maschinellen Beweisens (Resolventenprinzip).- § 13. Einleitung.- § 14. Die Klauselform der Prädikatenlogik und Herbrand-Strukturen (eine Umformulierung der klassischen Logik).- § 15. Herbrand-Prozeduren.- § 16. Das Resolventenprinzip.- § 17. Beweisverfahren des Resolventenprinzips.- § 18. Der konstruktive Charakter von Resolventenableitungen (Greenscher Antworten-Extraktionsprozeß).- § 19. Prädikatenlogik als Programmiersprache.- 6. Die Methode der Formalisierung: zwei Beispiele.- § 20. Informationswiedergewinnung als Anwendungsbeispiel.- § 21. Exkurs: das Formalisieren.- § 22. Die Formalisierung der Wertzuweisung.- 7. Probleme mit der Logik.- § 23. Grenzen der mathematischen Logik.- § 24. Bemerkungen zur Geschichte der Logik.- 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 universellenNormalform.- 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 strikteSyntax.- J. Zerlegungssatz für allgemeinste Vereinheitlicher.- Literaturangaben.- Hinweise zu weiterführender Literatur.- Verzeichnis häufig verwendeter Symbole.- Namen- und Sachverzeichnis.