doc-src/Intro/intro.tex
 changeset 348 1f5a94209c97 parent 311 3fb8cdb32e10 child 873 0cfc734e3dbd
equal inserted replaced
347:cd41a57221d0 348:1f5a94209c97
    41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
    41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover.
    42 It has been instantiated to support reasoning in several object-logics:
    42 It has been instantiated to support reasoning in several object-logics:
    43 \begin{itemize}
    43 \begin{itemize}
    44 \item first-order logic, constructive and classical versions
    44 \item first-order logic, constructive and classical versions
    45 \item higher-order logic, similar to that of Gordon's {\sc
    45 \item higher-order logic, similar to that of Gordon's {\sc
    46 hol}~\cite{gordon88a}
    46 hol}~\cite{mgordon-hol}
    47 \item Zermelo-Fraenkel set theory~\cite{suppes72}
    47 \item Zermelo-Fraenkel set theory~\cite{suppes72}
    48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90}
    49 \item the classical first-order sequent calculus, {\sc lk}
    49 \item the classical first-order sequent calculus, {\sc lk}
    50 \item the modal logics $T$, $S4$, and $S43$
    50 \item the modal logics $T$, $S4$, and $S43$
    51 \item the Logic for Computable Functions~\cite{paulson87}
    51 \item the Logic for Computable Functions~\cite{paulson87}
    66 including a simple theorem prover.  Users must be familiar with logic as
    66 including a simple theorem prover.  Users must be familiar with logic as
    67 used in computer science; there are many good
    67 used in computer science; there are many good
    68 texts~\cite{galton90,reeves90}.
    68 texts~\cite{galton90,reeves90}.
    69
    69
    70 \index{LCF}
    70 \index{LCF}
    71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an
    71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an
    72 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    72 ancestor of {\sc hol}, Nuprl, and several other systems.  Isabelle borrows
    73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
    74 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    74 abstract type; tactics and tacticals support backward proof.  But {\sc lcf}
    75 represents object-level rules by functions, while Isabelle represents them
    75 represents object-level rules by functions, while Isabelle represents them
    76 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    76 by terms.  You may find my other writings~\cite{paulson87,paulson-handbook}
    77 helpful in understanding the relationship between {\sc lcf} and Isabelle.
    77 helpful in understanding the relationship between {\sc lcf} and Isabelle.
    87
    78
    88 \index{Isabelle!release history} Isabelle was first distributed in 1986.
    79 \index{Isabelle!release history} Isabelle was first distributed in 1986.
    89 The 1987 version introduced a higher-order meta-logic with an improved
    80 The 1987 version introduced a higher-order meta-logic with an improved
    90 treatment of quantifiers.  The 1988 version added limited polymorphism and
    81 treatment of quantifiers.  The 1988 version added limited polymorphism and
    91 support for natural deduction.  The 1989 version included a parser and
    82 support for natural deduction.  The 1989 version included a parser and
   140 \include{foundations}
   131 \include{foundations}
   141 \include{getting}
   132 \include{getting}
   142 \include{advanced}
   133 \include{advanced}
   143
   134
   144 \bibliographystyle{plain} \small\raggedright\frenchspacing
   135 \bibliographystyle{plain} \small\raggedright\frenchspacing
   145 \bibliography{string,atp,funprog,general,logicprog,theory}
   136 \bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
   146
   137
   147 \input{intro.ind}
   138 \input{intro.ind}
   148 \end{document}
   139 \end{document}