Il XX secolo ha segnato la fine del sogno leibniziano di elaborare un grande sistema assiomatico che permettesse di risolvere ogni disputa, in qualunque ramo del sapere, attraverso un semplice calcolo. Il teorema d’indecidibilità di Church, infatti, ha stabilito che non è possibile progettare un algoritmo che stabilisca, per qualunque formula del linguaggio predicativo del primo ordine con l’identità, se essa sia una verità logica oppure no. A fronte di questo risultato, si è aperta una nuova area di ricerca, quella dell’automated reasoning, che, stimolata anche da esigenze di tipo pratico (quali la verifica di protocolli), lavora per capire ed ampliare quanto si riesce a dimostrare attraverso i calcoli, facendo interagire varie euristiche. La mancanza di testi che, oltre a spiegare in dettaglio l’alfabeto e la sintassi dei linguaggi “parlati” da singoli dimostratori automatici, accompagnino i lettori ad acquisire, attraverso esempi concreti, la capacità di formalizzare problemi per poi “interrogare” il dimostratore relativamente alla risposta, costituisce un ostacolo alla diffusione delle conoscenze relative a questa area di ricerca, limitandone la potenziale fruttuosità. Il presente volume si propone di colmare tale lacuna per quanto riguarda il dimostratore “Z3”, ricco strumento disponibile gratuitamente in rete.
Al risveglio dal sogno : la pratica della dimostrazione automatica / M.A.G. Franchella. - Milano : Unicopli, 2016 Oct. - ISBN 9788840019109. (BIBLIOTECA DI CULTURA FILOSOFICA)
Al risveglio dal sogno : la pratica della dimostrazione automatica
M.A.G. Franchella
2016
Abstract
Il XX secolo ha segnato la fine del sogno leibniziano di elaborare un grande sistema assiomatico che permettesse di risolvere ogni disputa, in qualunque ramo del sapere, attraverso un semplice calcolo. Il teorema d’indecidibilità di Church, infatti, ha stabilito che non è possibile progettare un algoritmo che stabilisca, per qualunque formula del linguaggio predicativo del primo ordine con l’identità, se essa sia una verità logica oppure no. A fronte di questo risultato, si è aperta una nuova area di ricerca, quella dell’automated reasoning, che, stimolata anche da esigenze di tipo pratico (quali la verifica di protocolli), lavora per capire ed ampliare quanto si riesce a dimostrare attraverso i calcoli, facendo interagire varie euristiche. La mancanza di testi che, oltre a spiegare in dettaglio l’alfabeto e la sintassi dei linguaggi “parlati” da singoli dimostratori automatici, accompagnino i lettori ad acquisire, attraverso esempi concreti, la capacità di formalizzare problemi per poi “interrogare” il dimostratore relativamente alla risposta, costituisce un ostacolo alla diffusione delle conoscenze relative a questa area di ricerca, limitandone la potenziale fruttuosità. Il presente volume si propone di colmare tale lacuna per quanto riguarda il dimostratore “Z3”, ricco strumento disponibile gratuitamente in rete.File | Dimensione | Formato | |
---|---|---|---|
franchellarisveglio.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
791.3 kB
Formato
Adobe PDF
|
791.3 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.