1\chapter*{Preface}\markboth{Preface}{Preface} 2\label{intro} 3 4This volume contains the description of the \HOL\ system's logic. It 5is one of four volumes making up the documentation for \HOL: 6 7\begin{myenumerate} 8\item \LOGIC: a formal description of the higher order logic 9 implemented by the \HOL{} system; 10\item \TUTORIAL: a tutorial introduction to \HOL, with case studies; 11\item \DESCRIPTION: a detailed user's guide for the \HOL{} system; 12\item \REFERENCE: the reference manual for \HOL. 13\end{myenumerate} 14 15\noindent These four documents will be referred to by the short names (in 16small slanted capitals) given above. 17 18This document, \LOGIC, serves as a formal definition of higher order 19logic in terms of a set-theoretic semantics. This material was 20written by Andrew Pitts in 1991, and was originally part of 21\DESCRIPTION. Because this logic is shared with other theorem-proving 22systems (HOL~Light, ProofPower), and is similar to that implemented in 23Isabelle, where it is called Isabelle/HOL, it is now presented in its 24own manual. 25 26The \HOL\ system is designed to support interactive theorem proving in 27higher order logic (hence the acronym `\HOL'). To this end, the formal 28logic is interfaced to a general purpose programming language (\ML, for 29meta-language) in which terms and theorems of the logic can be denoted, 30proof strategies expressed and applied, and logical theories developed. 31The version of higher order logic used in \HOL\ is predicate calculus 32with terms from the typed lambda calculus (\ie\ simple type 33theory). This was originally developed as a foundation for mathematics 34\cite{Church}. The primary application area of \HOL\ was initially 35intended to be the specification and verification of hardware designs. 36(The use of higher order logic for this purpose was first advocated by 37Keith Hanna \cite{Hanna-Daeche}.) However, the logic does not restrict 38applications to hardware; \HOL\ has been applied to many other areas. 39 40Thus, this document describes the theoretical underpinnings of the 41\HOL{} system, and presents it abstractly. 42 43The approach to mechanizing formal proof used in \HOL\ is due to Robin 44Milner \cite{Edinburgh-LCF}, who also headed the team that designed 45and implemented the language \ML. That work centred on a system 46called \LCF\ (logic for computable functions), which was intended for 47interactive automated reasoning about higher order recursively defined 48functions. The interface of the logic to the meta-language was made 49explicit, using the type structure of \ML, with the intention that 50other logics eventually be tried in place of the original logic. The 51\HOL\ system is a direct descendant of \LCF; this is reflected in 52everything from its structure and outlook to its incorporation of \ML, 53and even to parts of its implementation. Thus \HOL\ satisfies the 54early plan to apply the \LCF\ methodology to other logics. 55 56The original \LCF\ was implemented at Edinburgh in the early 1970's, and is now 57referred to as `Edinburgh \LCF'. Its code was ported from Stanford Lisp to 58Franz Lisp by G\'erard Huet at {\small INRIA}, and was used in a French 59research project called `Formel'. Huet's Franz Lisp version of \LCF\ was 60further developed at Cambridge by Larry Paulson, and became known as `Cambridge 61\LCF'. The \HOL\ system is implemented on top of an early version of Cambridge 62\LCF\ and consequently many features of both Edinburgh and Cambridge \LCF\ were 63inherited by \HOL. For example, the axiomatization of higher order logic used 64is not the classical one due to Church, but an equivalent formulation 65influenced by \LCF. 66 67An enhanced and rationalized version of \HOL, called \HOL 88, was 68released (in 1988), after the original \HOL\ system had been in use 69for several years. \HOL 90 (released in 1990) was a port of \HOL 88 70to SML \cite{sml} by Konrad Slind at the University of Calgary. It has 71been further developed through the 1990's. \HOL{} 4 is the latest 72version of \HOL, and is also implemented in SML; it features a number 73of novelties compared to its predecessors. \HOL{} 4 is also the 74supported version of the system for the international \HOL\ community. 75 76We have retroactively decided to number \HOL{} implementations in the 77following way 78\begin{enumerate} 79\item \HOL88 and earlier: implementations based on a Lisp substrate, 80 with Classic ML. 81\item \HOL90: implementations in Standard ML, principally using the 82 SML/NJ implementation. 83\item \HOL98 (Athabasca and Taupo releases): implementations using 84 Moscow ML, and with a new library and theory mechanism. 85\item \HOL{} (Kananaskis releases) 86\end{enumerate} 87Therefore, with \HOL{}~4, we do away with the habit of associating 88implementations with year numbers. Individual releases within 89\HOL{}~4 will retain the \textit{lake-number} naming scheme. 90 91In this document, the acronym `\HOL' refers to both the interactive theorem 92proving system and to the version of higher order logic that the system 93supports; where there is serious ambiguity, the former is called `the \HOL\ 94system' and the latter `the \HOL\ logic'. 95 96 97%%% Local Variables: 98%%% mode: latex 99%%% TeX-master: "logic" 100%%% End: 101