Poiché il software del computer diventa sempre più complesso, la questione di come garantirne la correttezza diventa sempre più critica. La logica formale incorporata nei programmi per computer è una parte importante della risposta a questo problema. Questo testo imperdibile presenta il lavoro pionieristico del defunto professor Jacob (Jack) T. Schwartz sulla logica computazionale e sulla teoria degli insiemi e la sua applicazione alle tecniche di verifica delle dimostrazioni, culminando nel sistema ÆtnaNova, un prototipo di programma per computer progettato per verificare la correttezza delle dimostrazioni matematiche presentate nel linguaggio della teoria degli insiemi. Adottando un approccio sistematico, il libro inizia con un'indagine dei rami tradizionali della logica prima di descrivere in dettaglio il disegno alla base del sistema ÆtnaNova. I principali risultati classici sull'indecidibilità e sull'irrisolvibilità vengono quindi riformulati per questo sistema. Ai lettori non è richiesta una grande conoscenza della logica formale per seguire il testo, ma si presuppone una buona comprensione delle tecniche di programmazione standard e una familiarità con le definizioni e le dimostrazioni matematiche che riflettono i consueti livelli di rigore.
caricamento...
