Formalisieren und Beweisen: Logik für Informatiker

ISBN-13: 9783528047573 / Niemiecki / Miękka / 1990 / 262 str.

Dirk Siefkes

Opis

Gregory Bateson -Biologe, Anthropologe, Psychiater, Systemtheoretiker -erziihlt in der Ein leitung zu seinem Buch Geist und Natur1 eine Geschichte: Ein Mann gibt in seinen Computer die Frage ein: "Wirst Du jemals denken wie ein Mensch? Rechne mal nach " Der Computer rechnet und rechnet und gibt schlieBlich aus: Dabei flillt mir eine Geschichte ein. Die Geschichte dieses Buches handelt von Menschen. "Fangt doch jeden Abschnitt mit einem Beispiel an," schlug Ralf-Detlef Kutsche vor, als er mir 1982 zusammen mit Peter Padawitz, Simone Pribbenow und Andreas Schulze half, die Lehrveranstaltung Logik for Informatiker durchzufiihren. "Fragen und Aufgaben regen besser zum Arbeiten an als Begriffe und Satze. " Deswegen beginnt jeder Tell dieses Buches mit einer Geschichte, die als Arbeitsmaterial dient: Die Einfuhrung mit dem Problem des Affen mit der Banane, die Aussagenlogik mit der Ballwurf logeiei, die Offene Pradikatenlogik mit dem Architektenbeispiel und die volle Priidikatenlogik mit der Geometrie Euklids. Deswegen endet jeder Abschnitt mit Aufgaben und Fragen, die wesentlich furs Verstehen sind. Deswegen sieht man beim Blattem so wenig Beweise: Ich ent wickle einen Beweis lieber aus einer Fragestellung und formuliere das Ergebnis als Satz, statt mit dem Satz zu beginnen. Deswegen sind die Themen des Buches Formalisieren und Verstehen, Tlitigkeiten, und nicht Logik und I nformatik, Gebiete. Ich behandle in dem Buch im wesentlichen die klassischen Grundthemen der mathematischen Logik: logische Folgerung, Ableitung, Vollstandigkeit, logische Theorie, Axiomensystem Es geht mir aber nicht darum, diese Begriffe und ihre Eigenschaften darzustellen.

Spis treści

Einführung.- 1 Aussagenlogik.- 1A Formeln schreiben und benutzen.- 1A1 Aussagen, Verknüpfungen und Wahrheitsfunktionen.- 1A2 Aussagenlogische Formeln.- 1A3 Formalisieren.- 1A4 Induktives Definieren und Beweisen.- 1A5 Belegungen und Wahrheitswerte.- 1A6 Wahrheitswerte bestimmen.- 1A7 Syntax und Semantik.- 1A8 Die Wertfunktion.- 1A9 Formalisieren auf große und kleine Weise.- 1B Allgemeingültige Formeln und logisches Folgern.- 1B1 Logische Folgerung.- 1B2 Eigenschaften der logischen Folgerung.- 1B3 Beziehungen zu anderen Begriffen.- 1B4 Allgemeingültige Formeln und Beweisprinzipien.- 1B5 Der Ersetzungssatz.- 1B6 Widersprüchlichkeit und Unerfüllbarkeit.- 1B7 Logische Folgerung und Widersprüchhchkeit.- 1B8 Endlichkeits- und Kompaktheitssatz.- 1C Entscheidungsverfahren und Normalformen.- 1C1 Entscheidungsverfahren mit Wahrheitstafeln und ihr Aufwand.- 1C2 Konjunktive und disjunktive Normalformen.- 1C3 Entscheidungsverfahren mit Normalformen.- 1C4 Klauseln, Gentzen- und Hornformeln.- 1D Ableiten.- 1D1 Ableiten an Beispielen.- 1D2 Ableitungsregeln, Ableiten, Ableitungen.- 1D3 Korrektkeit.- 1D4 Die Schnittregel.- 1D5 Vollständigkeit.- 1D6 Wozu Vollständigkeitsbeweise?.- 1D7 Die Schnittregel ist vollständig fürs Widerlegen von Hornformeln.- 1D8 Die Schnittregel ist vollständig fürs Widerlegen von Gentzenformeln.- 1D9 Widerlegungen in Ableitungen umformen.- 1D10 Die Schnittregel ist fast vollständig.- 1D11 Die Schnittregel vervollständigen.- 1D12 Entscheiden durch Ableiten.- 2 Offene Prädikatenlogik.- 2A Situationen strukturieren und durch Formeln beschreiben.- 2A1 Strukturieren und Struktur.- 2A2 Symbole, Signatur, Interpretation.- 2A3 Terme bilden.- 2A4 Formeln bilden.- 2A5 Variablenfreie Terme und Formeln auswerten.- 2A6 Einsetzen, Substitution.- 2A7 Gültige Formeln und Modelle.- 2A8 Auswerten mit Zuweisungen.- 2A9 Aussagenlogik in der Prädikatenlogik.- 2B Mit Formeln und Strukturen umgehen.- 2B1 Erfüllbare Formeln und logische Folgerung.- 2B2 Erzeugte Strukturen.- 2B3 Herbrandstrukturen.- 2B4 Logik variablenfreier Formeln.- 2B5 Formeln mit Variablen aussagenlogisch interpretieren.- 2B6 Eigenschaften von Formeln mit Variablen.- 2B7 Normalformen.- 2B8 Umbenennen und Einsetzen.- 2B9 Axiome für Architektenstrukturen.- 2C Strukturieren, Formalisieren, Axiomatisieren.- 2C1 Die Gleichheit aromatisieren.- 2C2 Modelle der Gleichheitsaxiome.- 2C3 Prädikatenlogik mit Gleichheit.- 2C4 Axiome und Theorien.- 2C5 Das Architektenbeispiel axiomatisieren.- 2D Ableiten.- 2D1 Ableitungsregeln in der offenen Prädikatenlogik.- 2D2 Schneiden und Einsetzen ist widerlegungsvollständig.- 2D3 Vollständigkeit fürs Widerlegen in die Prädikatenlogik hochheben.- 2D4 Vollständigkeit fürs Ableiten.- 2D5 Theorembeweiser.- 2D6 Endlichkeitssätze.- 2D7 Der Resolutionskalkül.- 2D8 Logisches Programmieren.- 3 Prädikatenlogik.- 3A Quantorenlogik.- 3Al Formeln mit Quantoren.- 3A2 Freie und gebundene Variablen.- 3A3 Einsetzen, Substitution.- 3A4 Auswerten.- 3A5 Erfüllbar, allgemeingültig, folgt logisch.- 3A6 Formeln aussagenlogisch interpretieren.- 3A7 Formeln abschließen oder öffnen.- 3A8 Weitere Eigenschaften von Quantorenformeln.- 3B Finitisieren und mechanisieren.- 3B1 Pränexe Normalform.- 3B2 Skolemisieren.- 3B3 Theorembeweiser.- 3B4 Der Satz von Herbrand.- 3B5 Logisches Programmieren.- 3B6 Herbrandstrukturen.- 3B7 Der Satz von Löwenheim und Skolem.- 3B8 Endlichkeits- und Kompaktheitssatz.- 3C Geometrie und Zahlen axiomatisieren.- 3C1 Mehr Axiome für die Euklidische Geometrie.- 3C2 Alle minimalen Geraden sind isomorph.- 3C3 Alle minimalen Ebenen sind isomorph.- 3C4 Vollständige Axiome, entscheidbare Theorien.- 3C5 Kategorische Axiome für die natürlichen Zahlen.- 3C6 Die natürlichen Zahlen sind nicht kategorisch axiomatisierbar.- 3C7 Das Induktionsschema.- 3C8 Die Peano-Axiome sind vollständig.- 3C9 Peano-Axiome mit Ordnung.- 3C10 Peano-Axiome für Ordnung und Addition.- 3C11 Peano-Axiome für Addition und Multiplikation.- 3D Stärken und Schwächen.- 3D1 Termination von Programmen ist nicht entscheidbar.- 3D2 Berechnungen formalisieren.- 3D3 Die Wörtertheorie ist nicht entscheidbar.- 3D4 Berechnungen axiomatisieren.- 3D5 Die Prädikatenlogik ist unentscheidbar.- 3D6 Nicht beweisbare wahre Sätze.- 3D7 Wahrheit ist nicht formalisierbar.- 3D8 Die natürlichen Zahlen sind nicht axiomatisierbar.- 3D9 Die natürlichen Zahlen als Grundlage der Mathematik.- 3D10 Die Logik erweitern.- 3D 11 Formalisieren.- Anhang Unvollständiger Dialog über Vollständigkeit.- Die Lehrveranstaltung Logik für Informatiker.- Verzeichnisse.- Personenverzeichnis.- Symbolverzeichnis.- Begriffsverzeichnis.