1\chapter*{Prefazione}\markboth{Prefazione}{Prefazione} 2\label{intro} 3 4Questo volume contiene la descrizione della logica del sistema \HOL. E' 5uno di quattro volumi che compongono la documentazione per \HOL: 6 7\begin{myenumerate} 8\item \LOGIC: una descrizione formale della logica di ordine superiore 9 implementata dal sistema \HOL{}. 10\item \TUTORIAL: un tutorial d'introduzione a \HOL, con dei casi di studio. 11\item \DESCRIPTION: una guida utente dettagliata per il sistema \HOL{}. 12\item \REFERENCE: il manuale di riferimento per \HOL. 13\end{myenumerate} 14 15\noindent Si far� riferimento a questi quattro documenti con i nomi abbreviati (in 16maiuscoletto inclinato) dati di sopra. 17 18Questo documento, \LOGIC, serve come una definizione formale della logica 19di ordine superiore in termini di una semantica a modelli. Questo materiale fu 20scritto da Andrew Pitts nel 1991, ed era originariamente parte di 21\DESCRIPTION. Poich� questa logica � condivisa con altri sistemi di dimostrazione 22di teoremi (HOL~Light, ProofPower), ed � simile a quella implementata in 23Isabelle, in cui � chiamata Isabelle/HOL, ora � presentata nel suo 24proprio manuale. 25 26Il sistema \HOL\ � sviluppato per supportare la dimostrazione interattiva di teoremi nella 27logica di ordine superiore(da qui l'acronimo `\HOL'). A questo scopo, la logica 28formale � interfacciata da un linguaggio di programmazione di uso generale (\ML, per 29meta-linguaggio) in cui si possono denotare i termini e i teoremi della logica, 30esprimere ed applicare le strategie di dimostrazione, e sviluppare teorie logiche. 31La versione della logica di ordine superiore usata in \HOL\ � un calcolo dei predicati 32con i termini del lambda calcolo tipizzato (cio� la teoria semplice dei 33tipi). Questa fu originariamente sviluppata come una fondazione per la matematica 34da \cite{Church}. La principale area di applicazione di \HOL\ fu inizialmente 35intesa essere la specifica e la verifica dei dispositivi di hardware. 36(L'uso della logica di ordine superiore a questo scopo fu inizialmente sostenuto da 37Keith Hanna \cite{Hanna-Daeche}.) Comunque, le applicazioni della logica non 38si riducono all'hardware; \HOL\ � stato applicato in molte altre aree. 39 40Cos�, questo documento descrive le basi teoriche del 41sistema \HOL{}, e lo presenta astrattamente. 42 43L'approccio di meccanizzare le dimostrazioni formali usato in \HOL\ � dovuto a Robin 44Milner \cite{Edinburgh-LCF}, che ha anche diretto il team che ha progettato 45e implementato il linguaggio \ML. Quel lavoro era centrato su un sistema 46chiamato \LCF\ (logica per le funzioni computabili), che era inteso per 47il ragionamento interattivo automatizzato circa funzioni di ordine superiore definite 48ricorsivamente. L'interfaccia della logica al meta-linguaggio era reso 49esplicito, usando la struttura di tipi dell'\ML, con l'intenzione che alla fine 50altre logiche sarebbe state provate al posto della logica originaria. Il 51sistema \HOL\ � un discendente diretto di \LCF; questo � riflesso in 52ogni cosa dalla sua struttura e aspetto alla sua incorporazione dell'\ML, 53e persino a parti della sua implementazione. Cos� \HOL\ soddisfa il 54piano iniziale di applicare la metodologia \LCF\ ad altre logiche. 55 56L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si 57riferisce ad esso come all'`\LCF di Edimburgo'. Il suo codice fu portato dallo Stanford Lisp 58al Franz Lisp da G\'erard Huet presso l'{\small INRIA}, e fu usato in un progetto di ricerca 59francese chiamato `Formel'. La versione Franz Lisp dell'\LCF\ di Huet fu 60ulteriormente sviluppata a Cambridge da Larry Paulson, e divenne conosciuta come il 61`Cambridge \LCF'. Il sistema \HOL\ � implementato sulla base di una prima versione del Cambridge 62\LCF\ e di conseguenza molte delle caratteristiche sia dell'Edinburgh che del Cambridge \LCF\ furono 63ereditate da \HOL. Per esempio, l'assiomatizzazione della logica di ordine superiore utilizzata 64non � quella classica dovuta a Church, ma una formulazione equivalente 65influenzata da \LCF. 66 67Una versione avanzata e razionalizzata di \HOL, chiamata \HOL 88, fu 68rilasciata (nel 1988), dopo che il sistema \HOL\ originario era stato in uso 69per molti anni. \HOL 90 (rilasciato nel 1990) fu un porting di \HOL 88 70in SML \cite{sml} da parte di Konrad Slind presso l'Universit� di Calgary. Esso � stato 71ulteriormente sviluppato nel corso degli anni 1990. \HOL{} 4 � l'ultima 72versione di \HOL, e anch'esso � implementato in SML; � dotato di un numero 73di novit� rispetto ai suoi predecessori. \HOL{} 4 � anche la 74versione del sistema supportata per la comunit� internazionale \HOL. 75 76Abbiamo deciso di numerare le implementazioni di \HOL{} retroattivamente nel 77modo seguente 78\begin{enumerate} 79\item \HOL88 e precedenti: implementazioni basate su un substrato Lisp, 80 con l'ML Classico. 81\item \HOL90: implementazioni in Standard ML, che usano principalmente 82 l'implementazione SML/NJ. 83\item \HOL98 (distribuzioni Athabasca e Taupo): implementazioni che usano 84 il Moscow ML, e con una nuova libreria e un nuovo meccanismo di teoria. 85\item \HOL{} (distribuzioni Kananaskis) 86\end{enumerate} 87Di conseguenza, con \HOL{}~4, facciamo a meno dell'abitudine di associare 88le implementazioni con i numeri degli anni. Le distribuzioni individuali all'interno 89di \HOL{}~4 conservano lo schema di nome \textit{lake-number}. 90 91In questo documento, l'acronimo `\HOL' si riferisce sia al sistema di dimostrazione 92interattiva di teoremi sia alla versione di logica di ordine superiore che il sistema 93supporta; dove c'� una seria ambiguit�, il primo � chiamato `il sistema 94\HOL' e la seconda `la logica \HOL'. 95 96%%% Local Variables: 97%%% mode: latex 98%%% TeX-master: "logic" 99%%% End: 100