Mathematische Logik mit Informatik-Anwendungen

Inhaltsverzeichnis

• 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 „strikte“Syntax.
• J. Zerlegungssatz für allgemeinste Vereinheitlicher.
• Literaturangaben.
• Hinweise zu weiterführender Literatur.
• Verzeichnis häufig verwendeter Symbole.
• Namen- und Sachverzeichnis.