\chapter*{Prefazione}\markboth{Prefazione}{Prefazione}
\label{intro}

Questo volume contiene un tutorial sul sistema \HOL{}. E' uno di quattro
documenti che costituiscono la documentazione per \HOL{}:

\begin{myenumerate}
\item \LOGIC: una descrizione formale della logica di ordine superiore
  implementata dal sistema \HOL{}.
\item \TUTORIAL: un tutorial d'introduzione a \HOL, con dei casi di studio.
\item \DESCRIPTION: una guida utente dettagliata per il sistema \HOL{}.
\item \REFERENCE: il manuale di riferimento per \HOL.
\end{myenumerate}

\noindent Si farà riferimento a questi quattro documenti con i nomi abbreviati (in
maiuscoletto inclinato) dati di sopra.

Questo documento, \TUTORIAL, è pensato per essere il primo letto dai nuovi
utenti di \HOL. Esso fornisce un'introduzione da auto-didatta alla struttura
e all'uso del sistema. Il tutorial è pensato per dare una sensazione del
modo in cui \HOL{} è utilizzato `mettendo già le mani sul sistema',
ma non spiega in modo sistematico
tutti i principi sottostanti (questi sono spiegati da \DESCRIPTION{}
e \LOGIC{}). Dopo aver lavorato con il \TUTORIAL\ il lettore dovrebbe essere
in una posizione tale da poter consultare gli altri documenti.

\section*{Per iniziare}

Il Capitolo~\ref{install} spiega come ottenere e installare \HOL. Una volta che questo
è stato fatto, il potenziale utente \HOL{} dovrebbe iniziare a familiarizzare con i
seguenti argomenti:
%
\begin{enumerate}
\item Il meta-linguaggio di programmazione \ML, e come interagire con esso.
\item La logica formale supportata dal sistema \HOL{} (la logica di ordine
  superiore) e la sua manipolazione attraverso l'\ML.
\item La dimostrazione in avanti e le regole d'inferenza derivate.
\item La dimostrazione guidata dal goal, le tattiche, e i tatticali.
\end{enumerate}
%
I Capitoli 2 e 3 introducono questi argomenti.
Il Capitolo~\ref{chap:euclid} sviluppa poi un ampio esempio --- la dimostrazione
di Euclide dell'infinità dei numeri primi --- per illustrare come \HOL{} è usato
per dimostrare teoremi.

%Chapter~\ref{proof} then describes forward and goal
%directed proof in much greater detail.

Il Capitolo~\ref{parity} presenta un altro esempio pratico: la specifica
e la verifica di un semplice bit di parità sequenziale. L'intenzione è
quella di ottenere due cose: (i) presentare un'altra parte completa
di lavoro con \HOL; e (ii) dare un'idea di cosa significhi usare
il sistema \HOL{} per una dimostrazione complicata. Il Capitolo~\ref{chap:combin} è un
esempio più esteso: la dimostrazione della confluenza per la logica
combinatoria. Di nuovo, l'obiettivo è quello di presentare un pezzo completo di
lavoro non banale.

Il Capitolo~\ref{chap:proof-tools} da un esempio di implementazione di
uno strumento di dimostrazione custom. Questo dimostra la programmabilità di
\HOL: il modo in cui può essere implementata una tecnologia per risolvere
problemi specifici sulla base del kernel sottostante. Avendo a disposizione
strumenti molto potenti, è possibile creare prototipi molto rapidamente.

Il Capitolo~\ref{chap:more-examples} discute brevemente alcuni
degli esempi distribuiti con \holn{} nella directory \ml{examples}.

%\item Chapter~\ref{tool} shows how a special purpose proof tool (a
%  conjunction normaliser) can be implemented and optimised. It
%  illustrates methods for `tuning' proof generating programs and
%  discusses trade-offs between generality and efficiency.

%\item Chapter~\ref{binomial} is a proof of the Binomial Theorem in a
%  ring.  It is a medium sized worked example whose subject matter is
%  probably more widely known than any specific piece of hardware or
%  software. The small amount of algebra and mathematical notation
%  needed to state and prove the Binomial Theorem is presented; the
%  notation is expressed in \HOL{}, and the structure of the proof is
%  outlined.

%\end{itemize}

\vspace{1cm}

\noindent il \TUTORIAL{} è stato mantenuto breve in modo tale che i nuovi utenti di \HOL{} possano
riuscire ad andare il più velocemente possibile. A volte alcuni dettagli sono stati semplificati.
Si raccomanda non appena un argomento nel \TUTORIAL\ è stato
digerito, di studiare le parti rilevanti di
\DESCRIPTION\ e \REFERENCE.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End: