Al risveglio dal sogno. La pratica della dimostrazione automatica - 9788840019109

Al risveglio dal sogno. La pratica della dimostrazione automatica: 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 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.
The 20th century marked the end of the dream has driven process a large axiomatic system that would make it possible to resolve any dispute in any branch of knowledge, through a simple calculation. The theorem of undecidability of Church, in fact, ruled that you cannot design an algorithm that determines, for any formula of first-order predicate language with ID, whether it is a logical truth or not. In view of this result, opened a new area of research, that of automated reasoning, that, also boosted by practical needs (such as checking of protocols), works to understand and expand what we can demonstrate through calculations, making interacting various heuristics. The lack of texts constitutes an obstacle to the dissemination of knowledge relating to this area of research, limiting potential fruitiness. This volume aims to fill that gap as regards the demonstrator "Z3" rich tool available for free on the net.