main.tex

\documentclass[10pt]{scrartcl}

\input{preamble}

\title{A Programmer's Guide to Proving Theorems with HOL4}
\author{Anonymous}
\date{}

\begin{document}
\maketitle{}

\paragraph*{Summary}
Interactive theorem proving is a method to perform trustworthy, rigorous
mathematical proofs checked by computers.
From a programmer's point of view, learning an ITP system is similar to
learning a new programming language.
The main difference is that an ITP system allows to first implement a function,
and then prove theorems about it.
This guide is written for experienced programmers, that have seen pen-and-paper
proofs before, but never worked with an ITP system.
If you ever wanted to replace that nice, cozy thought of \emph{this function
should work as I intend it to} with the high-assurance of a rigorous
mathematical proof, this guide is for you\footnote{If you are asking yourself the question how this is even possible, the same reasoning applies.}.
%
\input{intro}
%
\input{repl}
%
\input{example1}
%
\input{libraries}
%
\input{HOL4tactics}
%
\input{tipsTricks}
%
\clearpage
\appendix
\input{script}
%
\printbibliography
%
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: