Logica computazionale e teoria degli insiemi: Applicazione della logica formalizzata all'analisi

Recensioni dei lettori

Attualmente non ci sono recensioni dei lettori. La valutazione si basa su 2 voti.

Titolo originale:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Contenuto del libro:

Man mano che il software per computer diventa più complesso, la questione di come assicurarne la correttezza diventa sempre più critica. La logica formale incarnata nei programmi per computer è una parte importante della risposta a questo problema.

Questo testo imperdibile presenta il lavoro pionieristico del compianto professor Jacob (Jack) T. Schwartz sulla logica computazionale e sulla teoria degli insiemi e la sua applicazione alle tecniche di verifica delle prove, culminata nel sistema tnaNova, un prototipo di programma informatico progettato per verificare la correttezza delle prove matematiche presentate nel linguaggio della teoria degli insiemi. Con un approccio sistematico, il libro inizia con una rassegna dei rami tradizionali della logica prima di descrivere in dettaglio il progetto alla base del sistema tnaNova. Questo sistema viene poi utilizzato per ricavare alcuni dei principali risultati classici sull'indecidibilità e l'irrisolvibilità. Per seguire il testo non è necessaria una grande conoscenza della logica formale, anche se si presuppone una buona comprensione delle tecniche di programmazione standard e una certa familiarità con la matematica delle definizioni e degli scenari di prova.

Temi e caratteristiche: con una prefazione del dott. Martin Davis, professore emerito del Courant Institute of Mathematical Sciences della New York University; descrive in modo approfondito come una specifica teoria del primo ordine possa essere sfruttata per modellare ed eseguire ragionamenti in rami dell'informatica e della matematica; presenta un sistema unico per la verifica automatica delle prove in sistemi software su larga scala; integra importanti questioni di ingegneria delle prove, che riflettono gli obiettivi dei verificatori su larga scala; include un'appendice che mostra prove formalizzate degli ordinali, di varie proprietà dell'operazione di chiusura transitiva, dei principi di induzione finiti e transfiniti e del lemma di Zorn.

Quest'opera innovativa è una lettura essenziale per i ricercatori e i laureati in informatica.