"La logica intuizionistica è qui presentata come parte della logica classica familiare che consente l'estrazione meccanica di programmi dalle dimostrazioni. Per rendere il materiale più accessibile, vengono presentate prima le tecniche di base per la logica proposizionale; la Parte II contiene estensioni alla logica dei predicati. Questo materiale fornisce un'introduzione e uno sfondo sicuro per leggere la letteratura di ricerca in logica e informatica, nonché monografie avanzate. Si presuppone che i lettori abbiano familiarità con le nozioni di base della logica del primo ordine.". "Un espediente per rendere questo libro breve è stato l'invenzione di nuove dimostrazioni di diversi teoremi. La presentazione è basata sulla deduzione naturale. Gli argomenti includono l'interpretazione della programmazione della logica intuizionistica mediante lambda-calcolo semplicemente digitato (isomorfismo di Curry-Howard), traduzione negativa della logica classica in logica intuizionistica, normalizzazione delle deduzioni naturali, applicazioni alla teoria delle categorie, modelli di Kripke, semantica algebrica e topologica, metodi di ricerca di prove e teorema di interpolazione. Il testo si è sviluppato dal materiale di diversi corsi tenuti alla Stanford University nel 1992-1999.
caricamento...
