\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}
\definecolor{slideorange}{rgb}{1,.5,0}
\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}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\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{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\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}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut ProofWeb$\,$: logic education through the web}

Cezary Kaliszyk, \red{Freek Wiedijk}, Femke van Raamsdonk \\
%\smallskip
%
Radboud University Nijmegen \& Free University Amsterdam \\
{\small SURF F}oundation
\smallskip

\green{{\small FORMED}} \\ %$\,$: formal methods in computer science education } \\
{\small ETAPS} 2008, Budapest, Hungary \\
%\smallskip
%
{2008\hspace{3pt}03\hspace{3pt}29, 15\hspace{1pt}:\hspace{1.8pt}20}

\end{slide}

\begin{slide}
\slidetitle{teaching logic with the computer}

logic course for math/computer science students$\,$:

\begin{itemize}
\item[]
propositional logic \\
predicate logic \\
\red{\advirecord{a3}{predicate logic with equality}}
\end{itemize}
\adviplay{a3}
%\adviwait
\adviplay[slidered]{a3}
\adviwait
\bigskip

\blue{practising natural deduction proofs}
\begin{itemize}
\item[$\bullet$]
\textbf{on paper}

\advirecord{a1}{\textsl{students does not learn to be precise}}
\item[$\bullet$]
\textbf{with the computer}

\advirecord{a2}{\textsl{student does not learn to do it all himself}}
\end{itemize}
\smallskip
\adviwait
\adviplay{a1}
\adviwait
\adviplay{a2}
\adviwait
\green{both necessary: complement each other}

\vspace{-7pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{features}
\begin{itemize}
\item[$\bullet$] \red{built on top of serious proof system: Coq}
\begin{itemize}
\item
students work with an industrial strength system
\adviwait
\item
proofs look exactly like in a traditional textbook
\adviwait

\vbox to 0pt{
\vspace{1em}
\hfill\includegraphics[width=6em]{book.eps}\hspace{-3em}
\vss}
\vspace{-1.4em}
\green{compatible with: Huth \& Ryan, Login in Computer Science}
\end{itemize}
\smallskip
\adviwait
\item[$\bullet$] \red{web-based}
\begin{itemize}
\item
students don't need to install anything
\item
students can access their work from anywhere
\item
teacher has at all times full info on student's work
\end{itemize}
\smallskip
\adviwait
\item[$\bullet$] comes with a manual explaining the system
\item[$\bullet$] comes with a set of graded exercises
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq}
\begin{flushleft}
\red{proof assistant} based on constructive logic

developed at {\small INRIA}, France \\
1984 until today
\end{flushleft}
\adviwait
\bigskip

used for impressive proofs$\,$:
\begin{itemize}
\item[$\bullet$]
\blue{four color theorem}, Georges Gonthier
\adviwait
\item[$\bullet$]
\blue{verified C compiler}, Xavier Leroy
\end{itemize}
\adviwait
\bigskip
\green{power of Coq also makes ProofWeb attractive for education}

\vfill
\end{slide}

\def\lstrut{{\strut}}
\def\Lstrut{{\normalsize\strut}}
\def\mbar{\multicolumn{1}{|l}{}}

\begin{slide}
\slidetitle{natural deduction \advirecord{b3}{(Fitch style)}}
%\adviwait
\adviplay[slideblue]{b3}%
%\adviwait
\vspace{-2em}
\vbox to 0pt{
\begin{center}\footnotesize
\strut\hspace{-8em}%
\white{\advirecord{b1}{\begin{tabular}{rlllllllllll}
\cline{2-10}
\Lstrut 1 & \mbar &&&& $\exists x (P(x) \lor \neg Q(a))$ & assumption &&&& \mbar \\
\cline{3-9}
\Lstrut 2 & \mbar & \mbar &&& $Q(a)$ & assumption &&& \mbar & \mbar \\
\cline{4-8}
\Lstrut 3 & \mbar & \mbar & \mbar & $b$ & $P(b) \lor \neg Q(a)$ & assumption && \mbar & \mbar & \mbar \\
\cline{5-7}
\Lstrut 4 & \mbar & \mbar & \mbar & \mbar & $P(b)$ & assumption & \mbar & \mbar & \mbar & \mbar \\
\Lstrut 5 & \mbar & \mbar & \mbar & \mbar & $\exists x\, P(x)$ & $\exists$i 4 & \mbar & \mbar & \mbar & \mbar \\
\cline{5-7}
& \mbar & \mbar & \mbar &&&&& \mbar & \mbar & \mbar \\
\noalign{\vspace{-1.8\smallskipamount}}
\cline{5-7}
\Lstrut 6 & \mbar & \mbar & \mbar & \mbar & $\neg Q(a)$ & assumption & \mbar & \mbar & \mbar & \mbar \\
\lstrut 7 & \mbar & \mbar & \mbar & \mbar & $\bot$ & $\neg$e 6,2 & \mbar & \mbar & \mbar & \mbar \\
\Lstrut 8 & \mbar & \mbar & \mbar & \mbar & $\exists x\, P(x)$ & $\bot$e 7 & \mbar & \mbar & \mbar & \mbar \\
\cline{5-7}
\Lstrut 9 & \mbar & \mbar & \mbar && $\exists x\, P(x)$ & $\lor$e 3,4---5,6---8 && \mbar & \mbar & \mbar \\
\cline{4-8}
\Lstrut 10 & \mbar & \mbar &&& $\exists x\, P(x)$ & $\exists$e 1,3---9 &&& \mbar & \mbar \\
\cline{3-9}
\Lstrut 11 & \mbar &&&& $Q(a) \to \exists x\, P(x)$ & $\to$i 2---10 &&&& \mbar \\
\cline{2-10}
\Lstrut \advirecord{b6}{12} &&&&& \advirecord{b4}{$\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\, P(x)$} & \advirecord{b5}{$\to$i 1---11}
\end{tabular}}}%
\hspace{-7.5em}\strut
\end{center}
\vss}%
\vspace{-1.4em}
\vbox to 0pt{
\begin{center}\footnotesize
\tt
\strut\hspace{-8em}%
\advirecord{b7}{\begin{tabular}{rlllllll}
\cline{2-7}
1 & \mbar &&& \green{H1:} & $\exists$x, (P x $\lor$ $\neg$Q a) & assumption & \\
\cline{3-7}
2 & \mbar & \mbar && \green{H2:} & Q a & assumption \\
\cline{4-7}
& \mbar & \mbar & \mbar & b \\
3 & \mbar & \mbar & \mbar & \green{H3:} & P b $\lor$ $\neg$Q a & assumption \\
\cline{5-7}
4 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H4:}} & P b & assumption \\
5 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\exists$i 4 \\
\cline{5-7}
6 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H5:}} & $\neg$Q a & assumption \\
7 & \mbar & \mbar & \mbar & \mbar & $\bot$ & $\neg$e 6,2 \\
8 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\bot$e 7 \\
\cline{5-7}
9 & \mbar & \mbar & \mbar && $\exists$x, P x & $\lor$e 3,4-5,6-8 \\
\cline{4-7}
10 & \mbar & \mbar &&& $\exists$x, P x & $\exists$e 1,3-9 \\
\cline{3-7}
11 & \mbar &&&& Q a $\to$ $\exists$x, P x & $\to$i 2-10 \\
\cline{2-7}
12 &&&&& $\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x & $\to$i 1-11
\end{tabular}}%
\hspace{-4.95em}\strut
\end{center}
\vss}
\adviplay{b1}
\adviplay{b4}
\adviplay{b5}
\adviplay{b6}
%\adviwait
%\adviplay[slideblue]{b3}%
\adviwait
\adviplay[white]{b1}
\adviplay[white]{b4}
\adviplay[white]{b5}
\adviplay[white]{b6}
\adviplay{b7}

\vfill
\end{slide}

\def\der#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle{\strut{#1}\over\strut\box0}\rlap{$\,#3$}\hss$}}
\def\xder#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle\white{{\strut{\black{#1}}\over\strut\black{\box0}}}\rlap{$\,#3$}\hss$}}
%\let\xder=\der
\def\leaf#1{\displaystyle{\strut\atop\strut #1}}
\def\lab#1{\green{\hspace{.5pt}\rlap{${\vrule height 7pt depth0pt width 0pt}^{\tt #1}$}}}
\def\third#1{\hbox{\vbox to 0pt{\vspace{.15em}\hbox{#1}\vss}}}

\begin{slide}
\slidetitle{natural deduction (Gentzen style)}
$$
\def\green#1{\textcolor{white}{#1}}
\hspace{-12em}
\white{\advirecord{c1}{
\der{
\der{
\der{
\leaf{[\exists x (P(x) \lor \neg Q(a))]\lab{H1}}\qquad\qquad\qquad\qquad\qquad\enskip
\der{
\leaf{[P(b) \lor \neg Q(a)]\lab{H3}}\qquad\enskip
\der{
\leaf{[P(b)]\lab{H4}}
}
{\exists x\,P(x)}{{\exists}\mbox{i}}\qquad\qquad\enskip
\der{
\der{
\leaf{[\neg Q(a)]\lab{H5}}\quad\enskip
\leaf{[Q(a)]\lab{H2}}
}
{\bot}{{\neg}\mbox{e}}
}
{\exists x\,P(x)}{{\bot}\mbox{e}}
}
{\exists x\,P(x)}{{\lor}\mbox{e}\,\green{\scriptstyle [{\tt H4},{\tt H5}]}}
}
{\exists x\,P(x)}{{\exists}\mbox{e}\,\green{\scriptstyle [{\tt H3}]}}
}
{Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H2}]}}
}
{\exists x (P(x) \lor \neg Q(a)) \to Q(a) \to \exists x\,P(x)}{{\to}\mbox{i}\,\green{\scriptstyle [{\tt H1}]}}
}}
$$
\adviplay{c1}
\adviwait
\adviplay[white]{c1}
\vspace{-13.8em}
\begin{center}\tt\footnotesize
\medskip
\strut\hspace{-4em}%
\begin{tabular}{ccclcl}
&&&& [$\neg$Q a]$^{\green{\tt H5}}\;$ [Q a]$^{\green{\tt H2}}$ & \third{$\neg$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
&& [P b]$^{\green{\tt H4}}$ & \third{$\exists$i} & $\bot$ & \third{$\bot$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{3-3}\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
& [P b $\lor$ $\neg$Q a]$^{\green{\tt H3}}$ & $\exists$x, P x && $\exists$x, P x & \third{$\lor$e\green{[H4,H5]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{2-5} \noalign{\vspace{.5\smallskipamount}} \strut[$\exists$x, (P x $\lor$ $\neg$Q a)]$^{\green{\tt H1}}$ && $\hspace{1.6em}${}$\exists$x, P x$\hspace{-1.6em}$ &&& \third{$\exists$e\green{[H3]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}${}$\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H2]}}\\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}$Q a $\to$ $\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H1]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{-2.5em}${}$\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x$\hspace{-8.5em}$ \\
\end{tabular}%
$\hspace{-7em}$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{user input}

\begingroup
\def\\{\char`\\}
\begin{alltt}\small
Require Import ProofWeb.\medskip
Variable P Q : D -> Prop.
Variable a : D.\medskip
Theorem example : \red{\advirecord{d1}{exi x, (P(x) \\/ ~Q(a)) -> Q(a) -> exi x, P(x)}}.
Proof.
\green{\advirecord{d2}{imp_i H1.
imp_i H2.
f_exi_e H1 b H3.
f_dis_e H3 H4 H5.
f_exi_i H4.
fls_e.
f_neg_e H5 H2.}}
Qed.
\end{alltt}
\endgroup
\adviplay[slidered]{d1}
\adviplay[white]{d2}
\adviwait
\adviplay[slidegreen]{d2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{exercise colors}
\begin{flushleft}
possibilities for an exercise$\,$:
\end{flushleft}
\medskip
\begin{itemize}
\item[$\bullet$]
\gray{\textsf{Not touched}}
\item[$\bullet$]
\red{\textsf{Incomplete}}
\item[$\bullet$]
\orange{\textsf{Correct}}
\item[$\bullet$]
\green{\textsf{Solved}}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{demo}}
\vspace{1.73em}
\begin{center}
\blue{\texttt{http://proofweb.cs.ru.nl/}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{trying ProofWeb}
\begin{flushleft}
\red{three possibilities$\,$:}
\end{flushleft}
\vspace{1em}
\begin{center}
\blue{\texttt{http://proofweb.cs.ru.nl/}}
\end{center}
\vspace{2em}
\begin{enumerate}
\item
\textbf{guest access} \green{(no registration needed)}
\medskip
\adviwait
\item
\textbf{host course in Nijmegen} \green{(free)}
\medskip
\adviwait
\item
download \green{(open source)} and \textbf{host course on your own system}
\end{enumerate}

\vfill
\end{slide}

\begin{slide}
\slidetitle{future plans}
\begin{itemize}
\item[$\bullet$]
\textbf{other proof display styles}
\medskip
\item[{$\bullet$}]
{\textbf{other logics}}
\smallskip
\begin{itemize}
\item
\green{modal logics}
\item
\green{temporal logics}
\item
\green{logic in Dijkstra style}
\end{itemize}
\medskip
\adviwait
\item[\red{$\bullet$}]
\textbf{\red{MathWiki}}
\end{itemize}

\vfill
\end{slide}

\end{document}