\documentclass[a4]{seminar} \usepackage{advi} \usepackage{advi-graphicx} \usepackage{color} \usepackage{amssymb} %\usepackage[all]{xypic} \usepackage{alltt} \usepackage{url} \slideframe{none} \definecolor{slideblue}{rgb}{0,0,.5} \definecolor{slidegreen}{rgb}{0,.5,0} \definecolor{slidered}{rgb}{1,0,0} \definecolor{slidegray}{rgb}{.5,.5,.5} \definecolor{slidedarkgray}{rgb}{.4,.4,.4} \definecolor{slidelightgray}{rgb}{.8,.8,.8} \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}} \def\lightgray#1{\textcolor{slidelightgray}{#1}} \def\darkgray#1{\textcolor{slidedarkgray}{#1}} \newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut} \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} \newcommand{\toolong}{$\hspace{-6em}$} \begin{document}\sf \renewcommand{\sliderightmargin}{0mm} \renewcommand{\slideleftmargin}{20mm} \renewcommand{\slidebottommargin}{6mm} \def\eps{eps} \def\webad#1#2#3{\vspace{-1.4em}\vbox to 0pt{\vspace{20em}\hspace{0em}\footnotesize\rlap{\gray{google \fbox{{\tiny\strut}\blue{\advirecord{x1}{#1}}\adviplay[slideblue]{x1}} $\,\mapsto$ {\small $\langle\hspace{.5pt}$}\texttt{http://\blue{\advirecord{x2}{#2}}\adviplay[slideblue]{x2}#3}{\small $\hspace{.5pt}\rangle$}}}\vss}} \setcounter{slide}{-1} \begin{slide} \slidetitle{\Large do not take natural language \textsl{too} seriously} \green{Freek Wiedijk} \\ Radboud University Nijmegen \smallskip \red{Seminar Formal Mathematics} \\ University of Bonn \smallskip 2007\hspace{2pt}04\hspace{1.5pt}17, 13\hspace{.5pt}:\hspace{.7pt}00 \end{slide} \begin{slide} \slidetitle{programming languages} \strut\rlap{\textbf{C\exclspace:}}\hfill\red{\texttt{i++;}}\hfill\strut \adviwait \strut\rlap{\textbf{Cobol\exclspace:\hfill}}\hfill\green{\texttt{ADD 1 TO i.}}\hfill\strut \advirecord{c1}{\textbf{HyperTalk\exclspace:}} \begin{alltt}\footnotesize \advirecord{c2}{function delimitedSum theList, listDelimiter put the itemDelimiter into storedDelim \gray{-- save itemDelimiter for restore}\toolong if listDelim is empty then put comma into listDelimiter \gray{-- like 'sum'} else set the itemDelimiter to char 1 of value(listDelimiter) \gray{-- {\scriptsize{UN}}like 'sum'}\toolong put 0 into sumOfItems repeat with i = 1 to number of items in theList add value(item i of theList) to sumOfItems \gray{-- try to convert to a number}\toolong end repeat set the itemDelimiter to storedDelim \gray{-- restore itemDelimiter} return sumOfItems end delimitedSum} \end{alltt} \adviwait \blue{\textsl{making a programming language looks like natural language is a silly idea}}\adviwait\adviplay{c1}\adviplay[slidegreen]{c2} \vspace{-11pt} \vfill \end{slide} \begin{slide} \slidetitle{formulas} \vspace{-1.55\bigskipamount} \vbox to 0pt{ \vspace{12em} \hfill\hspace{.5em}\advirecord{a5}{\includegraphics[width=15em]{/home/freek/talks/bonn/cardano2.eps}}\hfill\strut \vss } \vspace{-1.18\bigskipamount} \vbox to 0pt{ \vspace{11em} \hfill\hspace{0em}\advirecord{a2}{\includegraphics[width=28em]{/home/freek/talks/bonn/cardano1.eps}}\hfill\strut \vspace{-8em} \advirecord{a2a}{\hrule height 9em width 30em} \vss } \gray{solutions of \advirecord{a6}{\rlap{$x^3 + px = q$\exclspace:}}\advirecord{a7}{$x^3 + 6x = 20$\exclspace:}\adviplay{a6}} \textbf{modern style\exclspace:} \vspace{1\bigskipamount} $$\advirecord{a4}{{\root 3\of{\sqrt{108} + 10}} - {\root 3\of{\sqrt{108} - 10}}}$$ \vspace{-5\bigskipamount} $$\advirecord{a1}{x = {\root 3\of{{q\over 2} \pm \sqrt{\left({q\over 2}\right)^2 + \left({p\over 3}\right)^3}}} - {\root 3\of{- {q\over 2} \pm \sqrt{\left({q\over 2}\right)^2 + \left({p\over 3}\right)^3}}}}\adviplay[slidered]{a1}$$ \vspace{-.5\bigskipamount} \smallskip \adviwait \textbf{ancient style}$\;$\gray{(Gerolamo Cardano, \textsl{Ars magna}, N\"urnberg, 1545)}\textbf{\exclspace:} \adviplay{a2} \adviwait \adviplay[white]{a2a} \begin{quote}\small \advirecord{a3}{Cube the third part of the number of unknowns, to which you add the square of half the number of the equation, and take the root of the whole, that is, the square root, which you will use, in the one case adding the half of the number which you just multiplied by itself, in the other case subtracting the same half, and you will have a binomial and apotome respecitvely; then subtract the cube root of the apotome from the cube root of the binomial, and the remainder from this is the value of the unknown.}\adviplay[slidegreen]{a3} \end{quote} \adviwait \adviplay[white]{a1} \adviplay[white]{a3} \adviplay[white]{a6} \adviplay[slidered]{a4} \adviplay{a5} \adviplay[slidegray]{a7} \vspace{-16pt} \vfill \end{slide} \begin{slide} \slidetitle{formal mathematics} \gray{Bertrand's postulate\exclspace:} \textbf{HOL Light\exclspace:} \begingroup \def\\{\char`\\} \begin{alltt}\small \red{!n. ~(n = 0) ==> ?p. prime p /\\ n <= p /\\ p <= 2 * n} \end{alltt} \endgroup \vspace{-\bigskipamount} $$\advirecord{b}{ \forall n.\, n\ne 0 \Rightarrow \exists p.\, \mathop{\sf prime\,} p \mathrel{\land} n \le p \mathrel{\land} p \le 2 \cdot n }$$%\adviplay[slidegray]{b}$$ \textbf{Mizar\exclspace:} \begin{alltt}\small \green{for n being Element of NAT st n>=1 holds ex p being Prime st n