\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\exclspace}{\hspace{.45pt}}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large comparing mathematical provers}

Freek Wiedijk \\
University of Nijmegen
\medskip

MKM 2003 \\
University of Bologna \\
Bertinoro

2003 02 18, 11:30
\end{slide}

\begin{slide}
\sectiontitle{the project}
\slidetitle{it's like collecting stamps}
comparison book: same program in many programming languages \\
\adviwait
\textcolor{slidegreen}{comparison of provers: same small proof in many systems}

concept \\
\dashskip ask `native speakers' of each system for a `natural' proof \\
\adviwait
\dashskip question \& answer section about each system
\adviwait

main goal: show how different these systems can be
\medskip
\adviwait

current state: 118 page report
\begin{itemize}
\item[$\bullet$] web page: \textcolor{slidered}{\texttt{http://www.cs.kun.nl/\char`\~freek/comparison/}}
\adviwait
\item[$\bullet$] will be: local Nijmegen report; maybe LNAI
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the lemma}
two canonical examples to explain the concept of `proof'
\begin{itemize}
\item[$\bullet$]
{\tiny\strut}\rlap{infinity of primes}\phantom{irrationality of $\sqrt{2}$} \quad (Euclid)
\item[$\bullet$]
\advirecord{sqrt2}{irrationality of $\sqrt{2}$}\adviplay{sqrt2} \quad (Pythagoras)
\end{itemize}
\medskip
\adviwait

\adviplay[slidered]{sqrt2}
second is more interesting: real number library!
\bigskip
\adviwait

the two variants of the theorem

\dashskip {\tiny\strut}\rlap{full result:}\phantom{basic lemma:} \quad $\sqrt{2} \not\in {\mathbb Q}$

\dashskip basic lemma: \quad $m^2 = 2 n^2 \iff m = n = 0$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the systems}
\slidetitle{ICT versus math}
QED manifesto (1994):
proof checking for mathematics

\begin{quote}
\textsl{QED is the very tentative title of a project to build a \\
computer system that effectively represents all important \\
mathematical knowledge and techniques.}
\end{quote}
\adviwait

current proof assistants \\
\dashskip mostly designed and used for verification of hardware/software \\
\adviwait
\dashskip focus here: suitability for formalization of \textcolor{slidered}{mathematics}
\medskip

\textcolor{slidegreen}{systems one should seriously consider for the QED dream}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the 15 provers}
\vbox to 0pt{
\vspace{-\bigskipamount}
\def\xxx#1{{\tiny\strut}\rlap{#1}\phantom{Isabelle/Isar} \qquad}
\xxx{HOL} John Harrison \\
\xxx{Mizar} Andrzej Trybulec \\
\xxx{PVS} Bart Jacobs \\
\xxx{Coq} Laurent Th\'ery \\
\xxx{\advirecord{q1}{Otter/Ivy}\adviplay{q1}} Michael Beeson \\
\xxx{Isabelle/Isar} Markus Wenzel \\
\xxx{Alfa/Agda} Thierry Coquand \\
\xxx{\advirecord{q2}{ACL2}\adviplay{q2}} Ruben Gamboa \\
\xxx{PhoX} Christophe Raffalli \\
\xxx{IMPS} William Farmer \\
\xxx{\advirecord{q3}{Metamath}\adviplay{q3}} Norman Megill \\
\xxx{Theorema} Markus Rosenkranz \\
\xxx{\advirecord{q4}{Lego}\adviplay{q4}} Conor McBride \\
\xxx{NuPRL} Paul Jackson \\
\xxx{$\Omega$mega} Christoph Benzm\"uller
\vss
}
\adviwait
\adviplay[slidered]{q1}\adviwait\adviplay{q1}
\adviplay[slidered]{q2}\adviwait\adviplay{q2}
\adviplay[slidered]{q3}\adviwait\adviplay{q3}
\adviplay[slidered]{q4}
\vfill
\end{slide}

\begin{slide}
\slidetitle{systems that didn't make the list}
only one system from each evolutionary path
\begin{center}
\begin{tabular}{rcccl}
ALF, Half & $\to$ & \textcolor{slidegray}{Agda} && \\
Nqthm & $\to$ & \textcolor{slidegray}{ACL2} && \\
&& \textcolor{slidegray}{IMPS} & $\to$ & MathScheme \\
&& \textcolor{slidegray}{Lego} & $\to$ & Oleg, Plastic \\
&& \textcolor{slidegray}{NuPRL} & $\to$ & MetaPRL
\end{tabular}
\end{center}
\medskip
\adviwait

other systems

{\tiny\strut}\hspace{.36em}%
\begin{tabular}{ll}
KIV, B method & (more for ICT than for math) \\
\adviwait
Twelf, Typelab & (more for logic than for math) \\
\adviwait
TPS & (not for a structured body of math)
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the proofs}
\slidetitle{files}
different kinds
\begin{itemize}
\item[]
\textbf{input files} \\
definitions \& statements \\
proof scripts
\item[]
\textbf{output files} \\
pretty printed with mathematical symbols \\
generated natural language \\
proof objects ($\lambda$-terms)
\end{itemize}
\medskip
\adviwait

comparison focuses on the files that the user interacts with
\adviwait

comparison presents relevant fragments of the other files
\vfill
\end{slide}

\begin{slide}
\slidetitle{three examples}
\medskip

\begin{center}
\advirecord{otter}{\textbf{otter.in}}
\bigskip
\bigskip

\advirecord{hol}{\textbf{hol.ml}}
\bigskip
\bigskip

\advirecord{mizar}{\textbf{mizar.miz}}
\end{center}
\adviplay{otter}\adviplay{hol}\adviplay{mizar}
\adviwait\adviplay[slidered]{otter}
\adviwait\adviembed{advi otter.dvi}\adviwait[1]
\adviplay{otter}\adviplay[slidered]{hol}
\adviwait\adviembed{advi hol.dvi}\adviwait[1]
\adviplay{hol}\adviplay[slidered]{mizar}
\adviwait\adviembed{advi mizar.dvi}\adviwait[1]
\adviplay{mizar}
\vfill
\end{slide}

\begin{slide}
\slidetitle{15 statements}
\vbox to 0pt{
\vspace{-\bigskipamount}
\small
$\bullet$\enskip \advirecord{s1}{\texttt{\char`\~rational(sqrt(\char`\&2))}}\adviplay{s1} \\
$\bullet$\enskip \advirecord{s2}{\texttt{sqrt 2 is irrational}}\adviplay{s2} \\
$\bullet$\enskip \advirecord{s3}{\texttt{NOT Rational?(sqrt(2))}}\adviplay{s3} \\
$\bullet$\enskip \advirecord{s4}{\texttt{(irrational (sqrt (S (S O))))}}\adviplay{s4} \\
$\bullet$\enskip \advirecord{s5}{\texttt{m(a,a) = m(2,m(b,b))}}\adviplay{s5} \\
$\bullet$\enskip \advirecord{s6}{\textsl{sqrt}$\;($\textsl{real}$\;($\textsl{2::nat}$))$ $\not\in$ $\mathbb{Q}$}\adviplay{s6} \\
$\bullet$\enskip \advirecord{s7}{$\mbox{\textsl{prime}}\;p\,\rightarrow\,\mbox{\textsl{noether}}\,A\,\left ( \mbox{\textsl{multiple}}\;p \right )\,\rightarrow\,\mbox{\textsl{isNotSquare}}\;p$}\adviplay{s7} \\
$\bullet$\enskip \advirecord{s8}{\texttt{(implies (equal (* x x) 2) (and (realp x) (not (rationalp x))))}$\hspace{-2em}$}\adviplay{s8} \\
$\bullet$\enskip \advirecord{s9}{\texttt{/\char`\\m,n\ :\ N (m\char`\^\ N2 = N2 * n\char`\^\ N2 -> m = N0 \char`\&\ n = N0)}}\adviplay{s9} \\
$\bullet$\enskip \advirecord{s10}{\texttt{not \char`\#(sqrt(2),qq)}}\adviplay{s10} \\
$\bullet$\enskip \advirecord{s11}{\texttt{\char`\$p \char`\|- ( sqr \char`\`\ 2\char`\_10 ) e/ QQ}}\adviplay{s11} \\
$\bullet$\enskip \advirecord{s12}{$\displaystyle\neg{\sf rat}\big[{\sqrt{p}}\big]$}\adviplay{s12} \\
$\bullet$\enskip \advirecord{s13a}{\texttt{\char`\{b\char`\|nat\char`\}\char`\{a\char`\|nat\char`\}(Eq (times two (times a a)) (times b b))-\char`\>}}\adviplay{s13a} \\
\phantom{$\bullet$\enskip }\advirecord{s13b}{\texttt{\ \ \ \ \ \ \ \ \ \ \ \ \ \ (Eq a zero /\char`\\\ Eq b zero)}}\adviplay{s13b} \\
$\bullet$\enskip \advirecord{s14}{$\neg\texttt{(}\exists\texttt{u:}{\mathbb Q}\texttt{.\ u *}$\boldmath{$_{q}$}$\texttt{ u = 2 / 1)}$}\adviplay{s14} \\
$\bullet$\enskip \advirecord{s15}{\texttt{(not (rat (sqrt 2)))}}\adviplay{s15}
\vss
}
\vfill
\adviwait
\adviplay[slidered]{s1}\adviwait\adviplay{s1}
\adviplay[slidered]{s2}\adviwait\adviplay{s2}
\adviplay[slidered]{s3}\adviwait\adviplay{s3}
\adviplay[slidered]{s4}\adviwait\adviplay{s4}
\adviplay[slidered]{s5}\adviwait\adviplay{s5}
\adviplay[slidered]{s6}\adviwait\adviplay{s6}
\adviplay[slidered]{s7}\adviwait\adviplay{s7}
\adviplay[slidered]{s8}\adviwait\adviplay{s8}
\adviplay[slidered]{s9}\adviwait\adviplay{s9}
\adviplay[slidered]{s10}\adviwait\adviplay{s10}
\adviplay[slidered]{s11}\adviwait\adviplay{s11}
\adviplay[slidered]{s12}\adviwait\adviplay{s12}
\adviplay[slidered]{s13a}\adviplay[slidered]{s13b}\adviwait\adviplay{s13a}\adviplay{s13b}
\adviplay[slidered]{s14}\adviwait\adviplay{s14}
\adviplay[slidered]{s15}
\end{slide}

\begin{slide}
\sectiontitle{the diagram}
\slidetitle{three important dimensions}
\begin{enumerate}
\item \textbf{size of the library}
\medskip
\item \textbf{mathematical nature, abstractness}
\medskip
\item \textbf{level of automation}
\end{enumerate}
\vfill
\end{slide}

\begin{slide}
\slidetitle{size of the library}
development of library is much more work than development of system \\
$\to$ should be main activity of the project!
\medskip
\adviwait

the only way to get a good system: exercise it in developing a library!
\adviwait

\vfill
\textcolor{slidegreen}{(strong player: Mizar)}
\end{slide}

\begin{slide}
\slidetitle{mathematical}
\begin{itemize}
\item[$\bullet$] de Bruijn criterion = small kernel
\adviwait
\item[$\bullet$] logical framework
\adviwait
\item[$\bullet$] constructive versus classical
\adviwait
\item[$\bullet$] first order, higher order, set/type theory
\adviwait
\item[$\bullet$] dependent types
\end{itemize}
\adviwait

\vfill
\textcolor{slidegreen}{(strong player: Coq)}
\end{slide}

\begin{slide}
\slidetitle{automation}
\begin{itemize}
\item[$\bullet$] batch checker, LCF style tactic prover, automated theorem prover
\adviwait
\item[$\bullet$] Poincar\'e principle = user automation of calculations
\adviwait
\item[$\bullet$] open architecture
\adviwait
\item[$\bullet$] decision procedures
\adviwait
\item[$\bullet$] proof search
\end{itemize}
\adviwait

\vfill
\textcolor{slidegreen}{(strong player: PVS)}
\end{slide}

\begin{slide}
\slidetitle{a Herzsprung-Russell diagram of proof checking}

\setlength{\unitlength}{.5mm}
\begin{picture}(145,130)(-40,-20)
\thinlines
\put(-30,-10){\vector(0,1){108}}\put(-35,104){\makebox(0,0)[l]{\textcolor{slidegreen}{\textsl{more automation}}}}
\put(-30,-10){\vector(1,0){128}}\put(65,-13){\makebox(0,0)[t]{\textcolor{slidegreen}{\textsl{more mathematical}}}}
\put(-20,90){\circle{6}}\put(-20,90){\makebox(0,0)[l]{\ ACL2}}
\put(42,80){\circle{10}}\put(42,80){\makebox(0,0)[l]{\ PVS}}
\put(74,74){\circle{10}}\put(74,74){\makebox(0,0)[l]{\ Isabelle}}
\put(62,72){\circle{10}}\put(62,72){\makebox(0,0)[l]{\ HOL}}
\put(54,70){\circle{6}}\put(54,70){\makebox(0,0)[l]{\ $\Omega$mega}}
\put(16,68){\circle*{2}}\put(16,68){\makebox(0,0)[l]{\ Otter}}
\put(20,66){\circle{6}}\put(20,66){\makebox(0,0)[l]{\ Theorema}}
\put(24,62){\circle{10}}\put(24,62){\makebox(0,0)[l]{\ IMPS}}
\put(70,60){\circle{10}}\put(70,60){\makebox(0,0)[l]{\ NuPRL}}
\put(78,58){\circle{10}}\put(78,58){\makebox(0,0)[l]{\ Coq}}
\put(58,41){\circle{6}}\put(58,41){\makebox(0,0)[l]{\ PhoX}}
\put(82,39){\circle{6}}\put(82,39){\makebox(0,0)[l]{\ Lego}}
\put(66,10){\circle{20}}\put(66,10){\makebox(0,0)[l]{\ Mizar}}
\put(86,1){\circle{6}}\put(86,1){\makebox(0,0)[l]{\ Agda}}
\put(90,-1){\circle{6}}\put(90,-1){\makebox(0,0)[l]{\ Metamath}}
\end{picture}
\vspace{-2em}
\vfill
\end{slide}

\end{document}