\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\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}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large mathematical ontology}

Freek Wiedijk \\
University of Nijmegen

MoWGLI \& Authomath meeting \\
DFKI, Saarbr\"ucken \\
2004 03 23, 10:00
\end{slide}

\begin{slide}
\slidetitle{different things that can be investigated}
two aspects of \textbf{encoded mathematics} inside a computer
\begin{eqnarray*}
\mbox{meta level = `form'} &\Rightarrow& \mbox{computer science\quad\advirecord{a1}{\green{$\leftarrow$ focus of MoWGLI$\hspace{-1em}$}}} \\
\mbox{object level = `meaning'} &\Rightarrow& \mbox{\advirecord{a2}{mathematics}\adviplay{a2}}
\adviwait
\adviplay{a1}
\adviwait
\adviplay[slidered]{a2}
\adviwait
\end{eqnarray*}

%computer science questions don't interest me:
%\begin{itemize}
%\item[]
%encode things whatever ad-hoc way you want
%\item[]
%don't need automated support for rendering, searching, distributing, \dots$\hspace{-5em}$
%\end{itemize}

formal versus informal mathematics
\begin{eqnarray*}
\mbox{`informal terms'} &\Rightarrow& \mbox{not well-understood mathematics} \\
\noalign{\vspace{-\smallskipamount}}
&& \mbox{\advirecord{a4a}{many formulas in computer algebra}} \\
\noalign{\vspace{-\smallskipamount}}
&& \mbox{\advirecord{a4b}{many formulas in physics}} \\
\noalign{\smallskip}
\mbox{`formal terms'} &\Rightarrow& \mbox{mathematics with a clear semantics} \\
&& \mbox{\advirecord{a3}{formal mathematics}}
\adviwait
\adviplay[slidegreen]{a4a}
\adviplay[slidegreen]{a4b}
\adviwait
\adviplay[slidered]{a3}
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a common formal library?}
systems for formal mathematics \adviwait\dots \\
{\dots} with a \green{significant formal library}, in which everything is proved
\begin{itemize}
\item[$\bullet$] \advirecord{b1}{Coq}\adviplay{b1}
\item[\advirecord{b2a}{$\bullet$}] \advirecord{b2}{C-CoRN}
\item[$\bullet$] \advirecord{b3}{Mizar}\adviplay{b3}
\item[$\bullet$] \advirecord{b4}{HOL}\adviplay{b4}
\item[$\bullet$] \advirecord{b5}{IMPS}\adviplay{b5}
\item[$\bullet$] NuPRL
\item[$\bullet$] Isabelle
\item[$\bullet$] PVS
\adviwait
\adviplay{b2a}
\adviplay{b2}
\adviwait
\adviplay[slidered]{b1}
\adviplay[slidered]{b2}
\adviplay[slidered]{b3}
\adviplay[slidered]{b4}
\adviplay[slidered]{b5}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{relating formal libraries}

\green{six libraries about finite sets}

\red{Coq} standard library, Jean-Christophe's \red{fsets} library for Coq, \\
Dan Synek's contrib to \red{C-CoRN}, \& the libraries of \red{Mizar}, \red{HOL}, \red{IMPS}

\bigskip
\adviwait

\textbf{find the common statements}

\begin{itemize}
\item[$\bullet$]
database with for each system the lemmas about finite sets$\hspace{-1em}$
\item[$\bullet$]
pointers relating `the same' statements in different systems
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{relating formal libraries (continued)}
\textbf{the empty set has zero elements}
\smallskip

\green{Coq: standard library} \\
\red{\texttt{cardinal\char`\_Empty}$\,$:}
\begingroup\small
\verb|forall m:nat, cardinal U (Empty_set U) m -> 0 = m|$\hspace{-5em}$
\endgroup

\green{Coq: fsets library} \\
\red{\texttt{cardinal\char`\_1}$\,$:}
\begingroup\small
\verb|(s:t)(Empty s) -> (cardinal s)=O|
\endgroup

\green{Mizar} \\
\red{\texttt{CARD\char`\_2:19}$\,$:}
\begingroup\small
\verb|0 = Card {}|
\endgroup \\
\red{\texttt{CARD\char`\_4:17}$\,$:}
\begingroup\small
\verb|X = {} iff Card X = 0|
\endgroup

\green{HOL} \\
\red{\texttt{CARD\char`\_CLAUSES}$\,$:}
\begingroup\small
\verb|CARD ({}:A->bool) = 0|
\endgroup

\green{IMPS} \\
\red{\texttt{EMPTY-INDIC-HAS-F-CARD-ZERO-REWRITE}$\,$:}
\begingroup\small
\verb|f_card{empty_indic{ind_1}}=0|$\hspace{-5em}$
\endgroup
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{term language for common statements of the systems}
\adviwait
\textbf{what features should this term language have?}
\adviwait
\begin{itemize}
\item[$\bullet$]
higher order \adviwait = first class binders \adviwait \quad\green{(excludes Mizar)} \adviwait
\item[$\bullet$]
subtypes \adviwait \quad\green{(excludes Coq, HOL, IMPS)} \adviwait
\item[$\bullet$]
coercions \adviwait \quad\green{(excludes Mizar, HOL, IMPS)} \adviwait
\item[$\bullet$]
dependent types \adviwait \quad\green{(excludes HOL, IMPS)} \adviwait
\item[$\bullet$]
overloading \adviwait \quad\green{(excludes Coq, HOL, IMPS)} \adviwait
\item[$\bullet$]
a global `set' type \adviwait \quad\green{(excludes HOL, IMPS)} \adviwait
\item[$\bullet$]
partial operations \adviwait \quad\green{(excludes Mizar, HOL)} \adviwait
\end{itemize}
\smallskip

having \red{none of these features} is too poor \\
\adviwait
but it is not nice to exclude a system to be able to have a feature$\,$!
\vfill
\end{slide}

\begin{slide}
\slidetitle{division in the real numbers is already non-trivial}
$$\red{{1\over 0} = 0}\mbox{\rlap{\quad ?}}\adviwait\medskip$$
\begin{center}
\begin{tabular}{rl}
Coq standard library & \green{independent} \rlap{(= not provable \& negation not provable)}\\
%\adviwait
C-CoRN & \green{not well-formed} \\
%\adviwait
Mizar & before: independent; now: \green{provably true}$\qquad$ \\
%\adviwait
HOL & \green{provably true} \\
%\adviwait
IMPS & \green{provably false} \\
%\adviwait
PVS & \green{not well-formed}
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a nice plan}
\begin{enumerate}
\item
\red{term language} \\
define a term signature \\
define when a term over this signature is `well-formed'
\adviwait
\item
\red{map this term language to the $n$ systems} \\
define a mapping of the well-formed terms to Coq \\
define a mapping of the well-formed terms to C-CoRN \\
define a mapping of the well-formed terms to Mizar \\
\dots
\adviwait
\end{enumerate}
\medskip

\textbf{coherence:} \\
\green{a well-formed statement should be provable in system X
iff it is \\ provable in system Y}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a nice plan (continued)}
\begin{itemize}
\item[3.]
\red{create a small database of sample statements in this term language} \\
statements from a trivial domain \green{(finite sets)} \\
statements from an algebraic domain \green{(basic theory of vector spaces)} \\
statements from an analytic domain \green{(theory of natural \rlap{logarithm)}}
\adviwait
\item[4.]
\red{prove the mapped version of each sample statement in each \rlap{system}} \\
prove statement A in system X \\
prove statement B in system X \\
\dots \\
prove statement A in system Y \\
prove statement B in system Y \\
\dots
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{between systems: not only statements but also proofs}
\red{proofs in the style of the Mizar system} \\
block structured proof language

\textbf{statements connected by tactics}
\bigskip
\adviwait

\green{leave out the tactics, just keep the statements} \\
proofs that are meaningful across systems$\,$!

\red{`formal proof sketches'}
\bigskip
\adviwait

\blue{closely related to
Laurent Th\'ery's \blue{Color Your Proof} system}
\vfill
\end{slide}

\begin{slide}
\slidetitle{section 4.1 of Abramowitz \& Stegun}
\adviwait
\adviembed{xvieww /home/freek/math/4.1/0067.jpg /home/freek/math/4.1/0068.jpg /home/freek/math/4.1/0069.jpg}%
\adviwait[1]%
57 formulas

can be rendered with a signature of 45 symbols \\
(this signature is similar to that of Content MathML)
\medskip
\adviwait

but: \red{what does it mean?}
\medskip

\begin{quote}
\green{
\begin{tabular}{l}
\texttt{eq(ln(0),minus(infinity))} \\
\texttt{eq(e,approx(27182818284,10))} \\
\texttt{eq(integral([z]div(1,z),z),ln(z))} \\
\dots
\end{tabular}
}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{summary}
\red{what I want is formal mathematics that is not bound to just one system}
\medskip
\adviwait

the three things I've talked about:
\medskip

\begin{itemize}
\item[$\bullet$]
relate libraries about the same subject in different systems \\
\green{(the example of the finite sets libraries)}
\medskip
%\adviwait
\item[$\bullet$]
define a term language for a \red{common core} of formal statements \\
\green{(the nice plan with four parts)}
\medskip
%\adviwait
\item[$\bullet$]
make a version of \green{section 4.1 of Abramowitz \& Stegun} where all terms have a well-defined formal semantics
\end{itemize}
\vfill
\end{slide}


\end{document}