| 0.01 | | [autore] |
| 0.02 | | [collana] |
| 0.03 | | [frontespizio] |
| 0.04 | | [colophon] |
| 0.05 | | Indice |
| 0.07 | | Prefazione [ di Zohar Manna ] |
| 0.09 | | __ |
| 0.10 | | ____ |
| | | {titolo} |
| 1 | Capitolo 1. | Computabilità |
| 1 | | Introduzione |
| 2 | 1.1. | Gli automi finiti |
| 4 | 1.1.1. | Le espressioni regolari |
| 4 | | Esempio 1.1. |
| 7 | | Esempio 1.2. |
| 7 | 1.1.2. | Gli automi finiti |
| 8 | | Esempio 1.3. |
| 9 | 1.1.3. | I grafi di transizione |
| 10 | | Esempio 1.4. |
| 11 | 1.1.4. | Il teorema di Kleene |
| 13 | | Esempio 1.5 |
| 16 | | Esempio 1.6 |
| 17 | | Il teorema di equivalenza |
| 18 | | Esempio 1.7 |
| 20 | 1.2. | Le macchine di Turing |
| 22 | 1.2.1. | Le macchine di Turing |
| 23 | | Esempio 1.8 |
| 25 | 1.2.2. | Le macchine di Post |
| 26 | | Esempio 1.9 |
| 27 | | Esempio 1.10 |
| 30 | 1.2.3. | Le macchine finite con memorie di tipo pushdown |
| 32 | | Esempio 1.11 |
| 33 | | Esempio 1.12 |
| 37 | 1.2.4. | Non determinismo |
| 37 | | Esempio 1.13 |
| 39 | 1.3. | Le macchine di Turing come accettori |
| 40 | 1.3.1. | Insiemi ricorsivamente numerabili |
| 40 | | Esempio 1.14 |
| 41 | | Insiemi ricorsivi |
| 41 | | Esempio 15 |
| 43 | 13.3. | I linguaggi formali |
| 43 | | Esempio 1.16 |
| 43 | | Esempio 1.17 |
| 46 | 1.4. | Le macchine di Turing come generatori |
| 46 | | Esempio 1.18 |
| 48 | 1.4.1. | Le funzioni primitive ricorsive |
| 48 | | Esempio 1.19 |
| 51 | | Esempio 1.20 |
| 53 | 1.4.2. | Funzioni ricorsive parziali |
| 54 | | Esempio 1.21 |
| 56 | | Le macchine di Turing come algoritmi |
| 57 | 1.5.1. | Risolubilità di classi di problemi si/no |
| 59 | 1.5.2. | Il problema dell'arresto delle macchine di Turing |
| 62 | 1.5.3. | Il problema della parola per i sistemi semi-Thue |
| 62 | | Esempio 1.22 |
| 64 | 1.5.4. | Il problema della corrispondenza di Post |
| 64 | | Esempio 1.23 |
| 66 | | Esempio 1.24 |
| 68 | 1.5.5. | Risolvibilità di classi di problemi si/no |
| 69 | | Esempio 1.25 |
| 71 | | Note bibliografiche |
| 72 | | Problemi |
| 80 | Capitolo 2. | Calcolo dei predicati |
| 81 | | Introduzione |
| 84 | 2.1. | Notazioni di base |
| 84 | 2.1.1. | Sintassi |
| 86 | | Esempio 2.1 |
| 88 | | Esempio 2.2 |
| 88 | 2.1.2. | Semantica (interpretazioni) |
| 89 | | Esempio 2.3 |
| 92 | | Esempio 2.4 |
| 92 | | Esempio 2.5 |
| 93 | 2.1.3. | Fbf valide |
| 94 | | Esempio 2.6 |
| 94 | | Esempio 2.7 |
| 96 | | Esempio 2.8 |
| 99 | 2.1.4. | Equivalenza di fbf |
| 102 | | Esempio 2.9 |
| 103 | | Esempio 2.10 |
| 105 | 2.1.5. | Le forme normali delle fbf |
| 109 | 2.1.6. | Il problema della validità |
| 112 | 2.2. | La deduzione naturale |
| 115 | 2.2.1. | Le regole per i connettivi |
| 116 | | Esempio 2.12 |
| 116 | | Esempio 2.13 |
| 117 | | Esempio 2.14 |
| 117 | | Esempio 2.15 |
| 120 | | Esempio 2.16 |
| 120 | 2.2.2. | Le regole per i quantificatori |
| 122 | | Esempio 2.17 |
| 122 | | Esempio 2.18 |
| 123 | | Esempio 2.19 |
| 123 | | Esempio 2.20 |
| 124 | | Esempio 2.21 |
| 125 | | Esempio 2.22 |
| 125 | | Esempio 2.23 |
| 126 | | Esempio 2.24 |
| 127 | | Esempio 2.25 |
| 127 | 2.2.3. | Le regole per gli operatori |
| 128 | | Esempio 2.26 |
| 129 | | Esempio 2.27 |
| 130 | 2.3. | Il metodo di risoluzione |
| 131 | 2.3.1. | La forma di clausola |
| 134 | | Esempio 2.28 |
| 136 | 2.3.2. | Le procedure di Herbrand |
| 136 | | Esempio 2.29 |
| 139 | | Esempio 2.30 |
| 140 | | Esempio 2.31 |
| 140 | | Esempio 2.32 |
| 141 | | Esempio 2.33 |
| 142 | | Esempio 2.34 |
| 142 | | Esempio 2.35 |
| 142 | 2.3.3. | L'algoritmo di unificazione |
| 143 | | Esempio 2.36 |
| 146 | | Esempio 2.37 |
| 147 | 2.3.4. | La regola di risoluzione |
| 148 | | Esempio 2.38 |
| 150 | | Esempio 2.39 |
| 152 | | Note bibliografiche |
| 153 | | Problemi |
| 168 | Capitolo 3. | Verifica dei programmi |
| 168 | | Introduzione |
| 169 | 3.1 | I programmi in forma di diagrammi di flusso |
| 179 | 3.1.1. | La correttezza parziale |
| 183 | | Esempio 3.1 |
| 186 | | Esempio 3.2 |
| 189 | | Esempio 3.3 |
| 191 | 3.1.2. | La fine |
| 193 | | Esempio 3.4 |
| 195 | | Esempio 3.5 [ di Donald Ervin Knuth ] |
| 198 | 3.2. | I programmi in forma di diagramma di flusso con righe |
| 198 | 3.2.1. | La correttezza parziale |
| 199 | | Esempio 3.6 |
| 204 | 3.2.2. | La fine |
| 205 | | Esempio 3.7 |
| 207 | | Esempio 3.8 |
| 208 | | Esempio 3.9 |
| 212 | 3.3. | I programmi di tipo Algol |
| 212 | 3.3.1. | I programmi di tipo while |
| 214 | | Esempio 3.10 |
| 215 | | La correttezza parziale |
| 218 | | Esempio 3.11 |
| 220 | | Esempio 3.12 |
| 222 | 3.3.3. | La correttezza totale |
| 225 | | Esempio 3.13 |
| 229 | | Note bibliografiche |
| 231 | | Problemi |
| 249 | Capitolo 4. | Schemi di diagramma di flusso |
| 249 | | Introduzione |
| 250 | 4.1. | Nozioni basilari |
| 250 | 4.1.1. | Sintassi |
| 252 | | Esempio 4.1 |
| 253 | 4.1.2. | Semantica (interpretazioni) |
| 254 | | Esempio 4.2 |
| 254 | | Esempio 4.3 |
| 257 | 4.1.3. | Proprietà basilari |
| 257 | | Esempio 4.4 |
| 257 | | Esempio 4.5 [ di Michael Stewart 'Mike' Paterson ] |
| 261 | | Esempio 4.6 [ di Michael Stewart 'Mike' Paterson ] |
| 265 | | Esempio 4.7 |
| 266 | 4.1.4. | Le interpretazioni di Herbrand |
| 267 | | Esempio 4.8 |
| 269 | | Esempio 4.9 |
| 270 | 4.2 | I problemi di decidibilità |
| 273 | 4.2.1. | Irrisolvibilità delle proprietà basilari |
| 274 | | Esempio 4.10 |
| 277 | 4.2.2. | Gli schemi liberi |
| 277 | | Esempio 4.11 |
| 278 | | Esempio 4.12 |
| 282 | | Esempio 4.13 |
| 284 | 4.2.3. | Gli schemi ad albero |
| 284 | | Esempio 4.14 |
| 287 | | Esempio 4.15 |
| 290 | | Esempio 4.16 |
| 291 | | Gli schemi di Ianov |
| 294 | | Esempio 4.17 |
| 299 | | Esempio 4.18 |
| 303 | 4.3. | Formalizzazione del calcolo dei predicati |
| 303 | 4.3.1. | L'algoritmo |
| 304 | | Esempio 4.19 |
| 306 | | Esempio 4.19 (seguito) |
| 309 | | Esempio 4.19 (seguito) |
| 309 | | Esempio 4.20 |
| 310 | | Esempio 4.21 |
| 314 | | Esempio 4.21 (seguito) |
| 314 | 4.3.2. | Formalizzazione delle proprietà dei programmi in forma di diagrammi di flusso |
| 316 | | Esempio 4.22 |
| 318 | 4.3.3. | Formalizzazione delle proprietà degli schemi di diagramma di flusso |
| 320 | | Esempio 4.23 |
| 322 | | Esempio 4.24 [ di S. Barry Cooper ] |
| 324 | 4.4. | I problemi di traduzione |
| 326 | 4.4.1. | Gli schemi ricorsivi |
| 328 | | Esempio 4.25 |
| 329 | 4.4.2. | Gli schemi di diagrammi di flusso in rapporto agli schemi ricorsivi |
| 333 | | Esempio 4.26 |
| 340 | | Note bibliografiche |
| 341 | | Problemi |
| 360 | Capitolo 5. | La teoria del punto fisso dei programmi |
| 360 | | Introduzione |
| 361 | 5.1. | Funzioni e funzionali |
| 363 | 5.1.1. | Funzioni monotone |
| 363 | | Esempio 5.1 |
| 364 | | Esempio 5.2 |
| 365 | | Esempio 5.3 |
| 367 | | Esempio 5.4 |
| 369 | | Esempio 5.5 |
| 370 | 5.1.2. | Funzionali continui |
| 370 | | Esempio 5.6 |
| 372 | | Esempio 5.7 |
| 373 | 5.1.3. | I punti fissi dei funzionali |
| 373 | | Esempio 5.8 |
| 375 | | Esempio 5.9 |
| 375 | | Esempio 5.10 |
| 376 | | Esempio 5.11 |
| 377 | | Esempio 5.12 |
| 378 | 5.2. | I programmi ricorsivi |
| 379 | 5.2.1. | Regole di computazione |
| 380 | | Esempio 5.13 |
| 380 | | Esempio 5.14 |
| 385 | | Esempio 5.15 |
| 386 | 5.2.2. | Le regole di computazione del punto fisso |
| 386 | | Esempio 5.16 |
| 392 | | Esempio 5.17 [ di James H. Jr. Morris ] |
| 386 | 5.2.3. | Sistemi di definizioni ricorsive |
| 394 | | Esempio 5.18 |
| 394 | | Esempio 5.19 |
| 395 | | Esempio 5.20 |
| 395 | 5.3. | I metodi di verifica |
| 396 | 5.3.1. | Induzione computazionale per passi [ di Jacobus Willem 'Jaco' De Bakker ET Dana S. Scott ] |
| 396 | | Esempio 5.21 |
| 398 | | Esempio 5.22 |
| 399 | | Esempio 5.23 |
| 400 | | Esempio 5.24 |
| 401 | | Esempio 5.25 |
| 402 | | Esempio 5.26 |
| 403 | 5.3.2. | Induzione computazionale completa |
| 404 | | Esempio 5.27 [ di James H. Jr. Morris ] |
| 406 | 5.3.3. | Induzione del punto fisso |
| 407 | | Esempio 5.28 |
| 408 | | Esempio 5.29 |
| 409 | | Esempio 5.30 |
| 411 | | Esempio 5.31 |
| 411 | 5.3.4. | Induzione strutturale |
| 413 | | Esempio 5.32 |
| 414 | | Esempio 5.33 [ di J. M. Cadiou ] |
| 415 | | Esempio 5.34 [ di Rodney Martineau 'Rod' Burstall ] |
| 416 | | Esempio 5.35 [ di Ness ] |
| 417 | | Esempio 5.36 [ di E. A. Ashcroft ] |
| 419 | | Note bibliografiche |
| 420 | | Problemi |
| 433 | | Riferimenti bibliografici |
| 443 | | Indice analitico |
| 451 | | _ |
| 453 | | [tipografia] |
| 454 | | __ |
