Read more
Questo libro contiene un'introduzione alla logica dei predicati del primo ordine ed alla deduzione automatica. Particolare enfasi e' posta sugli algoritmi che permettono la meccanizzazione completa della deduzione per alcuni frammenti della logica. I frammenti considerati non hanno soltanto interesse teorico ma sono rilevanti per le applicazioni dei metodi formali (ad esempio la verifica della correttezza dei programmi) e l'intelligenza artificiale (ad esempio la rivisitazione di problemi di planning come problemi di soddisfacibilita' Booleana).
Il libro inizia con l'introdurre la sintassi e la semantica della logica dei predicati del primo ordine e passa a considerare alcuni semplici ma interessanti problemi di verifica che possono essere espressi come problemi di soddisfacibilita' (ad esempio si codifica la correttezza di un semplice optimizing compiler che tenta di evitare la ricomputazione di espressioni algebriche). Per la sua semplicita', il libro considera il metodo dei Tableaux come prima tecnica di deduzione automatica per la logica dei predicati del primo ordine. Si vede un suo adattamento alle logiche descrittive che, di recente, hanno ricevuto un grande interesse per il ruolo che possono giocare nel semantic web.
Successivamente, il libro considera una serie di frammenti della logica dei predicati del primo ordine di particolare rilevanza per le applicazioni insieme alle relative tecniche per la deduzione automatica che permettono di ottenere procedure di decisione (ovvero algoritmi capaci di stabilire la soddisfacibilita' di una qualsiasi formula appartenente al frammento): logica Booleana ed algoritmo DPLL, formule senza quantificatori con eguaglianza e metodo di Herbrand, vincoli senza quantificatori dell'aritmetica ed algoritmo di Gauss e Fourier-Motzkin. Il libro passa quindi a considerare metodi generali basati su risoluzione e superposizione per la deduzione automatica nella logica dei predicati del primo ordine e descrive come questi possono essere utilizzati per derivare procedure di decisione per alcuni frammenti.
Il libro propone l'applicazione delle tecniche di deduzione automatica viste precedentemente al debugging ed alla verifica di alcuni semplici programmi. Infine, si considerano logiche temporali (che possono essere viste come estensioni della logica dei predicati del primo ordine) nelle quali e' naturale descrivere la dinamica dei programmi e dei sistemi informatici.
List of contents
Cap. 1 Logica dei predicati del primo ordine con uguaglianza
Cap. 2 Tableaux semantici e logiche descrittive
Cap. 3 Il problema della soddisfacibilit booleana
Cap. 4 Il metodo di Herbrand e la sua meccanizzazione
Cap. 5 Il problema della soddisfacibilit per formule senza quantificatori con uguaglianza
Cap. 6 Risoluzione e superposizione per la logica dei predicati del primo ordine
Cap. 7 L aritmetica lineare
Cap. 8 Metodi di combinazione
Cap. 9 La modellizzazione logica di alcuni programmi C e il loro debugging
Cap.10 Introduzione alla logica temporale e al model-checking
