Manuale di logica pratica e di ragionamento automatico

Recensioni dei lettori

Il libro è molto apprezzato per il suo approccio completo e pratico all'automated theorem proving (ATP), in particolare per la sua dettagliata implementazione in OCaml. I lettori apprezzano la chiarezza e la piacevolezza della scrittura, anche se ci sono alcuni inconvenienti per quanto riguarda il suo utilizzo come riferimento.

⬤ Eccellente introduzione alla dimostrazione automatica dei teoremi con una chiara progressione dalle basi agli argomenti avanzati.
⬤ Implementazioni complete degli algoritmi in OCaml, che migliorano la chiarezza e la comprensione.
⬤ Stile di scrittura piacevole che rende l'argomento coinvolgente.
⬤ Adatto a costruire il proprio theorem prover automatizzato da zero.
⬤ Considerato un must per chi è interessato alle procedure decisionali automatizzate.

⬤ Copertura limitata dei moderni risolutori SMT.
⬤ L'uso di OCaml può essere considerato uno svantaggio rispetto a linguaggi più diffusi come C++ o Java.
⬤ Può essere dispendioso in termini di tempo cercare le implementazioni delle funzioni di base quando si usa il libro come riferimento piuttosto che come tutorial.

(basato su 5 recensioni dei lettori)

Titolo originale:

Handbook of Practical Logic and Automated Reasoning

Contenuto del libro:

Questo libro soddisfa la richiesta di un resoconto autonomo e ampio dei concetti, delle macchine e dell'uso del ragionamento automatico.

I fondamenti della logica matematica sono descritti insieme all'applicazione pratica, il tutto con un minimo di prerequisiti. L'approccio è costruttivo, concreto e algoritmico: una caratteristica fondamentale è che i metodi sono descritti con riferimento a implementazioni reali (per le quali viene fornito il codice) che i lettori possono utilizzare, modificare e sperimentare.

Questo libro è ideale per chi cerca una fonte unica per l'area generale del ragionamento automatico. Può essere utilizzato come riferimento o come luogo di apprendimento dei fondamenti, sia in combinazione con corsi avanzati che per lo studio autonomo.