1\chapter*{Riconoscimenti}\markboth{Riconoscimenti}{Riconoscimenti} 2 3La maggior parte di \HOL\ � basato su codice scritto da---in ordine 4alfabetico---% 5Hasan Amjad, 6Richard Boulton, 7Anthony Fox, 8Mike Gordon, 9Elsa Gunter, 10John Harrison, 11Peter Homeier, 12G\'erard Huet (e altri presso l'istituto INRIA), 13Joe Hurd, 14Ramana Kumar, 15Ken Friis Larsen, 16Tom Melham, 17Robin Milner, 18Lockwood Morris, 19Magnus Myreen, 20Malcolm Newey, 21Michael Norrish, 22Larry Paulson, 23Konrad Slind, 24Don Syme, 25Thomas T\"urk, 26Chris Wadsworth, 27e 28Tjark Weber. 29Molti altri hanno fornito parti del sistema, correzione di bug, ecc. 30 31\subsection*{Edizione attuale} 32 33L'edizione attuale di tutti e quattro i volumi (\LOGIC, \TUTORIAL, 34\DESCRIPTION\ e \REFERENCE) � stata preparata da Michael Norrish e 35Konrad Slind. Altri contributi a questi volumi sono venuti da Hasan 36Amjad, che ha sviluppato una libreria di controllo del modello, e ha scritto le sezioni 37che ne descrivono l'uso; Jens Brandt, che ha sviluppato e documentato una 38libreria per i numeri razionali; Anthony Fox, che ha formalizzato e 39documentato nuove teorie dei gruppi riguardanti i word e le librerie associate; Mike 40Gordon, che ha documentato le librerie per i BDD e SAT; Peter Homeier, 41che ha implementato e documentato la libreria quoziente; Joe Hurd, che 42ha aggiunto materiale sulla ricerca della dimostrazione nel primo ordine; e Tjark Weber, che ha scritto 43le librerie per le Teorie Modulo Soddisfacibilit�~(SMT) e le Formule Booleane 44Quantificate~(QBF). 45 46\medskip 47 48Il materiale nella terza edizione costituisce un'approfondita rielaborazione 49ed estensione delle edizioni precedenti, l'unico pezzo essenzialmente non 50alterato � la semantica di Andy Pitts (in \LOGIC), il che riflette il fatto 51che, nonostante il sistema \HOL\ abbia subito uno sviluppo e un miglioramento 52continuo, la logica di \HOL\ � rimasta inalterata dalla sua prima edizione 53(1988). 54 55\newpage 56 57\subsection*{Seconda edizione} 58 59La seconda edizione di \REFERENCE\ � stato uno sforzo congiunto da parte del gruppo 60\HOL\ di Cambridge. 61 62\subsection*{Prima edizione} 63 64I tre volumi \TUTORIAL, \DESCRIPTION\ e \REFERENCE\ sono stati 65prodotti presso il Cambridge Research Center della SRI International con il 66supporto del DSTO Australia. 67 68Il progetto di documentazione di \HOL\ fu gestito da Mike Gordon, che 69scrisse anche parti di \DESCRIPTION\ e \TUTORIAL\ usando del materiale basato su 70uno scritto originario che descriveva il sistema \HOL\footnote{M.J.C.\ Gordon, `HOL: 71 a Proof Generating System for Higher Order Logic', in: {\it VLSI 72 Specification, Verification and Synthesis\/}, edito da G.\ 73 Birtwistle e P.A.\ Subrahmanyam, (Kluwer Academic Publishers, 74 1988), pp.\ 73--128.} e {\sl The ML Handbook\/}\footnote{{\sl The 75 ML Handbook}, scritto inedito presso l'Inria da parte di Guy Cousineau, Mike 76 Gordon, G\'erard Huet, Robin Milner, Larry Paulson and Chris 77 Wadsworth.}. Altri che hanno contribuito a \DESCRIPTION\ includono Avra Cohn, 78che ha scritto del materiale su teoremi, regole, conversioni e tattiche, 79e ha anche composto l'indice (che fu battuto a macchina da Juanito Camilleri); 80Tom Melham, che ha scritto le sezioni che descrivono le definizioni di tipo, 81il concreto pacchetto dei tipi, e le tattiche di `risoluzione'; e Andy Pitts, 82che ha ideato la semantica a modelli insiemistici della logica di \HOL\ e ha scritto 83il materiale che la descrive. 84 85Il documento originario usava macro \LaTeX\ fornite da Elsa 86Gunter, Tom Melham e Larry Paulson. La battitura di tutti e tre 87i volumi fu gestita da Tom Melham. La copertina fu disegnata da Arnold 88Smith, che us� una fotografia di una `lanterna da neve' presa da 89Avra Cohn (nel cui giardino risiede l'oggetto originale). John Van 90Tassel ha composto l'immagine \LaTeX\ della lanterna. 91 92Molte altre persone oltre a quelle elencate di sopra hanno contribuito nello sforzo della 93documentazione di \HOL\, sia fornendo materiale, sia inviando elenchi di errori nella prima 94edizione. Grazie a tutti coloro che hanno aiutato, e grazie al DSTO e all'SRI per il loro 95generoso supporto. 96 97 98 99 100