Computergestützte Logik und Mengenlehre: Anwendung der formalisierten Logik auf die Analyse

Bewertung: ⭐⭐⭐⭐⭐  (5,0 von 5)

Leserbewertungen

Derzeit gibt es keine Leserbewertungen. Die Bewertung basiert auf 2 Stimmen.

Originaltitel:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Inhalt des Buches:

Da Computersoftware immer komplexer wird, wird die Frage, wie ihre Korrektheit sichergestellt werden kann, immer wichtiger. Die in Computerprogrammen verkörperte formale Logik ist ein wichtiger Teil der Antwort auf dieses Problem.

Dieses Buch stellt die bahnbrechenden Arbeiten des verstorbenen Professors Jacob (Jack) T. Schwartz über Computerlogik und Mengenlehre und ihre Anwendung auf Techniken zur Verifikation von Beweisen vor, die im tnaNova-System gipfelten, einem Prototyp eines Computerprogramms zur Verifikation der Korrektheit mathematischer Beweise, die in der Sprache der Mengenlehre dargestellt sind. Das Buch verfolgt einen systematischen Ansatz und beginnt mit einem Überblick über die traditionellen Zweige der Logik, bevor es den Aufbau des tnaNova-Systems im Detail beschreibt. Dieses System wird dann verwendet, um einige der wichtigsten klassischen Ergebnisse über Unentscheidbarkeit und Unlösbarkeit abzuleiten. Der Leser benötigt keine großen Kenntnisse der formalen Logik, um dem Text zu folgen, obwohl ein gutes Verständnis von Standardprogrammiertechniken und eine Vertrautheit mit der Mathematik von Definitionen und Beweisszenarien vorausgesetzt wird.

Themen und Merkmale: mit einem Vorwort von Dr. Martin Davis, emeritierter Professor des Courant Institute of Mathematical Sciences, New York University; beschreibt ausführlich, wie eine spezifische Theorie erster Ordnung genutzt werden kann, um Schlussfolgerungen in Zweigen der Informatik und Mathematik zu modellieren und auszuführen; stellt ein einzigartiges System für die automatische Beweisüberprüfung in großen Softwaresystemen vor; integriert wichtige Fragen des Proof-Engineerings, die die Ziele großer Verifizierer widerspiegeln; enthält einen Anhang mit formalisierten Beweisen für Ordinalzahlen, für verschiedene Eigenschaften der transitiven Schließungsoperation, für endliche und transfinite Induktionsprinzipien und für das Zornsche Lemma.

Dieses bahnbrechende Werk ist eine unverzichtbare Lektüre für Forscher und fortgeschrittene Absolventen der Computerwissenschaften.

Weitere Daten des Buches:

• ISBN: 9780857298072
• Autor: T. Schwartz Jacob
• Verlag: Springer Nature
• Einband: Hardcover
• Erscheinungsjahr: 2011
• Seitenzahl: 416